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 ';' (goto 0);
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 A1, TARSKI:def 2;
A4: if=0 (a,(I ';' (goto 0))) = ((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= (Macro (a =0_goto 3)) ";" ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) by SCMFSA6A:25 ;
A5: 1 <> (card I) + 2 by NAT_1:11;
thus (while=0 (a,I)) . 0 = (if=0 (a,(I ';' (goto 0)))) . 0 by FUNCT_7:32
.= (Directed (Macro (a =0_goto 3))) . 0 by A4, A2, SCMFSA8A:14
.= 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 ';' (goto 0)))) . 1 by FUNCT_7:32, A5
.= (Directed (Macro (a =0_goto 3))) . 1 by A4, A3, SCMFSA8A:14
.= 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 ';' (goto 0))) = ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= (Macro (a >0_goto 3)) ";" ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) 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 A7, TARSKI:def 2;
thus (while>0 (a,I)) . 0 = (if>0 (a,(I ';' (goto 0)))) . 0 by FUNCT_7:32
.= (Directed (Macro (a >0_goto 3))) . 0 by A6, A8, SCMFSA8A:14
.= 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 ';' (goto 0)))) . 1 by FUNCT_7:32, A5
.= (Directed (Macro (a >0_goto 3))) . 1 by A6, A9, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ; :: thesis: verum