let a be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA holds
( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )
let I, J be MacroInstruction of SCM+FSA ; :: thesis: ( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )
set i = a =0_goto ((card J) + 3);
A1: if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)
.= (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a =0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a =0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (Macro (a =0_goto ((card J) + 3))) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) ;
A2: dom (Macro (a =0_goto ((card J) + 3))) = {0,1} by COMPOS_1:61;
then 0 in dom (Macro (a =0_goto ((card J) + 3))) by TARSKI:def 2;
hence (if=0 (a,I,J)) . 0 = (Directed (Macro (a =0_goto ((card J) + 3)))) . 0 by A1, SCMFSA8A:14
.= a =0_goto ((card J) + 3) by SCMFSA7B:1 ;
:: thesis: ( (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )
1 in dom (Macro (a =0_goto ((card J) + 3))) by A2, TARSKI:def 2;
hence (if=0 (a,I,J)) . 1 = (Directed (Macro (a =0_goto ((card J) + 3)))) . 1 by A1, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ;
:: thesis: ( (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )
set i = a >0_goto ((card J) + 3);
A3: if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)
.= (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a >0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a >0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (Macro (a >0_goto ((card J) + 3))) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) ;
A4: dom (Macro (a >0_goto ((card J) + 3))) = {0,1} by COMPOS_1:61;
then 0 in dom (Macro (a >0_goto ((card J) + 3))) by TARSKI:def 2;
hence (if>0 (a,I,J)) . 0 = (Directed (Macro (a >0_goto ((card J) + 3)))) . 0 by A3, SCMFSA8A:14
.= a >0_goto ((card J) + 3) by SCMFSA7B:1 ;
:: thesis: (if>0 (a,I,J)) . 1 = goto 2
1 in dom (Macro (a >0_goto ((card J) + 3))) by A4, TARSKI:def 2;
hence (if>0 (a,I,J)) . 1 = (Directed (Macro (a >0_goto ((card J) + 3)))) . 1 by A3, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ;
:: thesis: verum