set J = Stop SCM+FSA;
let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds
( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )

let I be MacroInstruction of SCM+FSA ; :: thesis: ( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )
set I1 = I ';' ();
set i = a =0_goto 3;
A1: dom (Macro (a =0_goto 3)) = {0,1} by COMPOS_1:61;
then A2: 0 in dom (Macro (a =0_goto 3)) by TARSKI:def 2;
A3: 1 in dom (Macro (a =0_goto 3)) by ;
A4: if=0 (a,(I ';' ())) = ((a =0_goto 3) ";" (Goto ((card (I ';' ())) + 1))) ";" ((I ';' ()) ";" ()) by SCMFSA6A:25
.= (Macro (a =0_goto 3)) ";" ((Goto ((card (I ';' ())) + 1)) ";" ((I ';' ()) ";" ())) by SCMFSA6A:25 ;
A5: 1 <> (card I) + 2 by NAT_1:11;
thus (while=0 (a,I)) . 0 = (if=0 (a,(I ';' ()))) . 0 by FUNCT_7:32
.= (Directed (Macro (a =0_goto 3))) . 0 by
.= a =0_goto 3 by SCMFSA7B:1 ; :: thesis: ( (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )
thus (while=0 (a,I)) . 1 = (if=0 (a,(I ';' ()))) . 1 by
.= (Directed (Macro (a =0_goto 3))) . 1 by
.= goto 2 by SCMFSA7B:2 ; :: thesis: ( (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )
set i = a >0_goto 3;
A6: if>0 (a,(I ';' ())) = ((a >0_goto 3) ";" (Goto ((card (I ';' ())) + 1))) ";" ((I ';' ()) ";" ()) by SCMFSA6A:25
.= (Macro (a >0_goto 3)) ";" ((Goto ((card (I ';' ())) + 1)) ";" ((I ';' ()) ";" ())) by SCMFSA6A:25 ;
A7: dom (Macro (a >0_goto 3)) = {0,1} by COMPOS_1:61;
then A8: 0 in dom (Macro (a >0_goto 3)) by TARSKI:def 2;
A9: 1 in dom (Macro (a >0_goto 3)) by ;
thus (while>0 (a,I)) . 0 = (if>0 (a,(I ';' ()))) . 0 by FUNCT_7:32
.= (Directed (Macro (a >0_goto 3))) . 0 by
.= a >0_goto 3 by SCMFSA7B:1 ; :: thesis: (while>0 (a,I)) . 1 = goto 2
thus (while>0 (a,I)) . 1 = (if>0 (a,(I ';' ()))) . 1 by
.= (Directed (Macro (a >0_goto 3))) . 1 by
.= goto 2 by SCMFSA7B:2 ; :: thesis: verum