A4: if>0 (a,I,J) =
((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)
.=
(((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))
by SCMFSA6A:25
.=
((a >0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a >0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))))
by SCMFSA6A:25
.=
(a >0_goto ((card J) + 3)) ";" ((J ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a >0_goto ((card J) + 3)) ";" (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))
by SCMFSA6A:25
;
A5: card (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)) =
(card ((J ";" (Goto ((card I) + 1))) ";" I)) + (card (Stop SCM+FSA))
by SCMFSA6A:21
.=
(card ((J ";" (Goto ((card I) + 1))) ";" I)) + 1
by COMPOS_1:4
.=
((card (J ";" (Goto ((card I) + 1)))) + (card I)) + 1
by SCMFSA6A:21
.=
(((card J) + (card (Goto ((card I) + 1)))) + (card I)) + 1
by SCMFSA6A:21
.=
(((card J) + 1) + (card I)) + 1
by SCMFSA8A:15
.=
((card I) + (card J)) + 2
;
0 + 1 <= card I
by NAT_1:13;
then
1 + (card J) <= (card I) + (card J)
by XREAL_1:7;
then A6:
(1 + (card J)) + 2 <= ((card I) + (card J)) + 2
by XREAL_1:7;
((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is really-closed
by Lm3;
hence
if>0 (a,I,J) is really-closed
by A6, SCMFSA_X:32, A4, A5; verum