A4: 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
;
A5: card (((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA)) =
(card ((Goto ((card I) + 1)) ";" I)) + (card (Stop SCM+FSA))
by SCMFSA6A:21
.=
(card ((Goto ((card I) + 1)) ";" I)) + 1
by COMPOS_1:4
.=
((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 A6:
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 A6, Th30, A4, A5; verum