A1: if=0 (a,I) =
((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))
by SCMFSA6A:25
.=
(a =0_goto 3) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a =0_goto 3) ";" (((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA))
by SCMFSA6A:25
;
A2: card (((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA)) =
(card ((Goto ((card I) + 1)) ";" I)) + 1
by Lm1, SCMFSA6A:21
.=
(card ((Goto ((card I) + 1)) ";" I)) + 1
.=
((card (Goto ((card I) + 1))) + (card I)) + 1
by SCMFSA6A:21
.=
(1 + (card I)) + 1
by SCMFSA8A:15
.=
(card I) + 2
;
0 + 1 <= card I
by NAT_1:13;
then A3:
1 + 2 <= (card I) + 2
by XREAL_1:7;
((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed
by Th26;
hence
if=0 (a,I) is really-closed
by A3, Th29, A1, A2; verum