let a be Int-Location ; for I, J being Program of SCM+FSA holds
( 0 in dom (if=0 a,I,J) & 1 in dom (if=0 a,I,J) & 0 in dom (if>0 a,I,J) & 1 in dom (if>0 a,I,J) )
let I, J be Program of SCM+FSA ; ( 0 in dom (if=0 a,I,J) & 1 in dom (if=0 a,I,J) & 0 in dom (if>0 a,I,J) & 1 in dom (if>0 a,I,J) )
set i = a =0_goto ((card J) + 3);
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 ))))
;
then A1:
dom (Macro (a =0_goto ((card J) + 3))) c= dom (if=0 a,I,J)
by SCMFSA6A:56;
A2:
dom (Macro (a =0_goto ((card J) + 3))) = {0 ,1}
by SCMFSA7B:4;
then A3:
1 in dom (Macro (a =0_goto ((card J) + 3)))
by TARSKI:def 2;
0 in dom (Macro (a =0_goto ((card J) + 3)))
by A2, TARSKI:def 2;
hence
( 0 in dom (if=0 a,I,J) & 1 in dom (if=0 a,I,J) )
by A1, A3; ( 0 in dom (if>0 a,I,J) & 1 in dom (if>0 a,I,J) )
set i = a >0_goto ((card J) + 3);
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 ))))
;
then A4:
dom (Macro (a >0_goto ((card J) + 3))) c= dom (if>0 a,I,J)
by SCMFSA6A:56;
A5:
dom (Macro (a >0_goto ((card J) + 3))) = {0 ,1}
by SCMFSA7B:4;
then A6:
1 in dom (Macro (a >0_goto ((card J) + 3)))
by TARSKI:def 2;
0 in dom (Macro (a >0_goto ((card J) + 3)))
by A5, TARSKI:def 2;
hence
( 0 in dom (if>0 a,I,J) & 1 in dom (if>0 a,I,J) )
by A4, A6; verum