let I, J be Program of SCM+FSA; for a being Int-Location holds (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5)
let a be Int-Location ; (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5)
set I1 = I ';' (SubFrom (a,(intloc 0)));
set J3 = ((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1));
set J4 = (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2);
A1:
card (Goto ((card (Goto 2)) + 1)) = 1
by SCMFSA8A:15;
card ((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) =
(card (Macro (a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)))) + (card (I ';' (SubFrom (a,(intloc 0)))))
by SCMFSA6A:21
.=
2 + (card (I ';' (SubFrom (a,(intloc 0)))))
by COMPOS_1:56
;
then A2: card (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) =
((card (I ';' (SubFrom (a,(intloc 0))))) + 2) + 1
by A1, SCMFSA6A:21
.=
(card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)
;
then
((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)) -' (card (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1)))) = 0
by XREAL_1:232;
then A3:
goto 2 = (Goto 2) . (((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)) -' (card (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1)))))
by SCMFSA8A:31;
A4:
card (Goto 2) = 1
by SCMFSA8A:15;
then
(card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1) < (card (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1)))) + (card (Goto 2))
by A2, NAT_1:13;
then A5: ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) . ((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)) =
IncAddr ((goto 2),(card (((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1)))))
by A2, A3, Th13
.=
goto (2 + ((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)))
by A2, SCMFSA_4:1
.=
goto ((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 3))
;
card ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) =
((card (I ';' (SubFrom (a,(intloc 0))))) + (2 + 1)) + 1
by A2, A4, SCMFSA6A:21
.=
(card (I ';' (SubFrom (a,(intloc 0))))) + ((2 + 1) + 1)
;
then
card ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) = ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) + 1
;
then
(card (I ';' (SubFrom (a,(intloc 0))))) + 3 < card ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))
by NAT_1:13;
then A6:
(card (I ';' (SubFrom (a,(intloc 0))))) + 3 in dom ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))
by AFINSQ_1:66;
then (((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA)) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) =
(Directed ((((a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) ';' (I ';' (SubFrom (a,(intloc 0))))) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)
by SCMFSA8A:14
.=
goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5)
by A5, A6, SCMFSA8A:16
;
hence
(if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5)
by SCMFSA8B:def 1; verum