set J = Stop SCM+FSA;
let a be Int-Location; for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 4) = halt SCM+FSA
let I be MacroInstruction of SCM+FSA ; (while>0 (a,I)) . ((card I) + 4) = halt SCM+FSA
set I1 = I ';' (goto 0);
set i = a >0_goto 3;
set c5 = (card I) + 4;
set Mi = ((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0));
0 + ((card I) + 4) in { (il + ((card I) + 4)) where il is Nat : il in dom (Stop SCM+FSA) }
by Lm3;
then A1:
(card I) + 4 in dom (Shift ((Stop SCM+FSA),((card I) + 4)))
by VALUED_1:def 12;
then A2: (Shift ((Stop SCM+FSA),((card I) + 4))) /. ((card I) + 4) =
(Shift ((Stop SCM+FSA),((card I) + 4))) . (0 + ((card I) + 4))
by PARTFUN1:def 6
.=
halt SCM+FSA
by Lm2, Lm3, VALUED_1:def 12
;
A3:
( (card I) + 4 in dom (while>0 (a,I)) & dom (while>0 (a,I)) = dom (if>0 (a,(I ';' (goto 0)))) )
by Th8, FUNCT_7:30;
card (if>0 (a,(I ';' (goto 0)))) = (card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)))) + (card (Stop SCM+FSA))
by SCMFSA6A:21;
then A4: card (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0))) =
(card (if>0 (a,(I ';' (goto 0))))) - (card (Stop SCM+FSA))
.=
((card (I ';' (goto 0))) + 4) - 1
by Th2, Lm1
.=
(((card I) + 1) + 4) - 1
by COMPOS_2:11
.=
(card I) + 4
;
then A5:
not (card I) + 4 in dom (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)))
;
dom (if>0 (a,(I ';' (goto 0)))) = (dom (((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)))) \/ (dom (Reloc ((Stop SCM+FSA),((card I) + 4))))
by A4, SCMFSA6A:39;
then A6:
(card I) + 4 in dom (Reloc ((Stop SCM+FSA),((card I) + 4)))
by A3, A5, XBOOLE_0:def 3;
A7:
Reloc ((Stop SCM+FSA),((card I) + 4)) = IncAddr ((Shift ((Stop SCM+FSA),((card I) + 4))),((card I) + 4))
by COMPOS_1:34;
(card I) + 4 <> (card I) + 2
;
hence (while>0 (a,I)) . ((card I) + 4) =
((((Macro (a >0_goto 3)) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0))) ";" (Stop SCM+FSA)) . ((card I) + 4)
by FUNCT_7:32
.=
(Reloc ((Stop SCM+FSA),((card I) + 4))) . ((card I) + 4)
by A6, SCMFSA6A:40, A4
.=
IncAddr ((halt SCM+FSA),((card I) + 4))
by A1, A2, A7, COMPOS_1:def 21
.=
halt SCM+FSA
by COMPOS_0:4
;
verum