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;
A1: (card I) + 4 =
((card I) + 1) + 3
.=
(card (I ';' (goto 0))) + 3
by COMPOS_2:11
;
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 A2:
(card I) + 4 in dom (Shift ((Stop SCM+FSA),((card I) + 4)))
by VALUED_1:def 12;
then A3: (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
;
A4:
( (card I) + 4 in dom (while=0 (a,I)) & dom (while=0 (a,I)) = dom (if=0 (a,(I ';' (goto 0)))) )
by Th6, 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 A5: 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 Th1, Lm1
.=
(card I) + 4
by A1
;
then A6:
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 A5, SCMFSA6A:39;
then A7:
(card I) + 4 in dom (Reloc ((Stop SCM+FSA),((card I) + 4)))
by A4, A6, XBOOLE_0:def 3;
A8:
Reloc ((Stop SCM+FSA),((card I) + 4)) = IncAddr ((Shift ((Stop SCM+FSA),((card I) + 4))),((card I) + 4))
by COMPOS_1:34;
A9:
(card I) + 4 <> (card I) + 2
;
thus (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, A9
.=
(Reloc ((Stop SCM+FSA),((card I) + 4))) . ((card I) + 4)
by A5, A7, SCMFSA6A:40
.=
IncAddr ((halt SCM+FSA),((card I) + 4))
by A2, A3, A8, COMPOS_1:def 21
.=
halt SCM+FSA
by COMPOS_0:4
; verum