let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds (if>0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)
let I be MacroInstruction of SCM+FSA ; :: thesis: (if>0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)
set I1 = I ';' (goto 0);
set i = a >0_goto 3;
set c4 = (card (I ';' (goto 0))) + 1;
set Mi = ((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I;
A1: card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) = card (((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)
.= (card ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1)))) + (card I) by SCMFSA6A:21
.= ((card (Goto ((card (I ';' (goto 0))) + 1))) + 2) + (card I) by SCMFSA6A:33
.= (1 + 2) + (card I) by SCMFSA8A:15
.= (card I) + 3 ;
A2: ((card (I ';' (goto 0))) + 1) + 0 = ((card I) + 1) + 1 by COMPOS_2:11
.= ((card I) + 3) - 1
.= LastLoc (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) by AFINSQ_1:91, A1 ;
then A3: (card (I ';' (goto 0))) + 1 = (card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)) -' 1 by AFINSQ_1:70;
LastLoc ((((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) = (LastLoc (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)) + (LastLoc (Macro (goto 0))) by COMPOS_2:43
.= (LastLoc (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)) + 1 by COMPOS_2:30 ;
then A4: (card (I ';' (goto 0))) + 1 < LastLoc ((((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) by A2, NAT_1:13;
A5: 0 in dom (Macro (goto 0)) by AFINSQ_1:65;
then A6: (Macro (goto 0)) /. 0 = (Macro (goto 0)) . 0 by PARTFUN1:def 6
.= goto 0 by COMPOS_1:58 ;
thus (if>0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = (((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)) . ((card (I ';' (goto 0))) + 1) by SCMFSA_X:36
.= ((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) . ((card (I ';' (goto 0))) + 1) by A4, SCMFSA6A:41
.= (IncAddr ((Macro (goto 0)),((card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)) -' 1))) . 0 by A2, COMPOS_1:23
.= IncAddr (((Macro (goto 0)) /. 0),((card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I)) -' 1)) by A5, COMPOS_1:def 21
.= IncAddr ((goto 0),((card (I ';' (goto 0))) + 1)) by A6, A3
.= goto (0 + ((card (I ';' (goto 0))) + 1)) by SCMFSA_4:1
.= goto ((card (I ';' (goto 0))) + 1) ; :: thesis: verum