let J be Program of SCM+FSA ; for a being Int-Location holds (if=0 a,(Goto 2),J) . ((card J) + 3) = goto ((card J) + 5)
let a be Int-Location ; (if=0 a,(Goto 2),J) . ((card J) + 3) = goto ((card J) + 5)
set JJ = (a =0_goto ((card J) + 3)) ';' J;
set J3 = ((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2);
set J4 = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2);
A1:
card (Goto 2) = 1
by SCMFSA8A:29;
card ((a =0_goto ((card J) + 3)) ';' J) =
(card (Macro (a =0_goto ((card J) + 3)))) + (card J)
by SCMFSA6A:61
.=
2 + (card J)
by SCMFSA7B:6
;
then A2: card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) =
((card J) + 2) + 1
by A1, SCMFSA6A:61
.=
(card J) + (2 + 1)
;
then
((card J) + 3) -' (card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2))) = 0
by XREAL_1:234;
then A3:
goto 2 = (Goto 2) . (((card J) + 3) -' (card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2))))
by SCMFSA8A:47;
card (Goto 2) = 1
by SCMFSA8A:29;
then
(card J) + 3 < (card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2))) + (card (Goto 2))
by A2, NAT_1:13;
then A4: ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2)) . ((card J) + 3) =
IncAddr (goto 2),(card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)))
by A2, A3, Th13
.=
goto (2 + ((card J) + 3))
by A2, SCMFSA_4:14
.=
goto ((card J) + (2 + 3))
;
card (Goto 2) = 1
by SCMFSA8A:29;
then A5:
if=0 a,(Goto 2),J = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto (1 + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA )
by SCMFSA8B:def 1;
A6:
InsCode (goto ((card J) + 5)) = 6
by SCMFSA_2:47;
card ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2)) =
((card J) + 3) + 1
by A1, A2, SCMFSA6A:61
.=
(card J) + (3 + 1)
;
then
card ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2)) = ((card J) + 3) + 1
;
then
(card J) + 3 < card ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2))
by NAT_1:13;
then A7:
(card J) + 3 in dom ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2))
by AFINSQ_1:70;
then (((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2)) ';' (Stop SCM+FSA )) . ((card J) + 3) =
(Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto 2)) ';' (Goto 2))) . ((card J) + 3)
by SCMFSA8A:28
.=
goto ((card J) + 5)
by A4, A6, A7, SCMFSA8A:30, SCMFSA_2:124
;
hence
(if=0 a,(Goto 2),J) . ((card J) + 3) = goto ((card J) + 5)
by A5; verum