let a be Int-Location ; :: thesis: for I, J being Program 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 Program 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);
A2: if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) by SCMFSA8B:def 1
.= (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67
.= ((a =0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:67
.= (a =0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) by SCMFSA6A:71
.= (Macro (a =0_goto ((card J) + 3))) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) ;
A3: dom (Macro (a =0_goto ((card J) + 3))) = {0,1} by COMPOS_1:149;
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 A2, SCMFSA8A:28
.= a =0_goto ((card J) + 3) by SCMFSA7B:7 ;
:: 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 A3, TARSKI:def 2;
hence (if=0 (a,I,J)) . 1 = (Directed (Macro (a =0_goto ((card J) + 3)))) . 1 by A2, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ;
:: 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);
A5: if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) by SCMFSA8B:def 2
.= (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67
.= ((a >0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:67
.= (a >0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) by SCMFSA6A:71
.= (Macro (a >0_goto ((card J) + 3))) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) ;
A6: dom (Macro (a >0_goto ((card J) + 3))) = {0,1} by COMPOS_1:149;
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 A5, SCMFSA8A:28
.= a >0_goto ((card J) + 3) by SCMFSA7B:7 ;
:: thesis: (if>0 (a,I,J)) . 1 = goto 2
1 in dom (Macro (a >0_goto ((card J) + 3))) by A6, TARSKI:def 2;
hence (if>0 (a,I,J)) . 1 = (Directed (Macro (a >0_goto ((card J) + 3)))) . 1 by A5, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ;
:: thesis: verum