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