let a be Int-Location; 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 ; ( (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
;
( (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
;
( (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
;
(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
;
verum