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 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))))
;
then A1:
dom (Macro (a =0_goto ((card J) + 3))) c= dom (if=0 (a,I,J))
by SCMFSA6A:17;
A2:
dom (Macro (a =0_goto ((card J) + 3))) = {0,1}
by COMPOS_1:61;
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 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))))
;
then A4:
dom (Macro (a >0_goto ((card J) + 3))) c= dom (if>0 (a,I,J))
by SCMFSA6A:17;
A5:
dom (Macro (a >0_goto ((card J) + 3))) = {0,1}
by COMPOS_1:61;
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