set J1 = Stop SCM+FSA;
set J = Stop SCM+FSA;
let a be Int-Location ; for I being Program of holds (while=0 (a,I)) . ((card I) + 5) = halt SCM+FSA
let I be Program of ; (while=0 (a,I)) . ((card I) + 5) = halt SCM+FSA
set I1 = I ';' (Goto 0);
set f = ((card I) + 4) .--> (goto 0);
set i = a =0_goto ((card (Stop SCM+FSA)) + 3);
set c5 = (card I) + 5;
set Lc5 = (card I) + 5;
set Mi = (((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0));
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & (card I) + 5 <> (card I) + 4 )
by FUNCOP_1:13;
then A1:
not (card I) + 5 in dom (((card I) + 4) .--> (goto 0))
by TARSKI:def 1;
0 + ((card I) + 5) in { (il + ((card I) + 5)) where il is Element of NAT : il in dom (Stop SCM+FSA) }
by Lm3;
then A2:
(card I) + 5 in dom (Shift ((Stop SCM+FSA),((card I) + 5)))
by VALUED_1:def 12;
then A3: (Shift ((Stop SCM+FSA),((card I) + 5))) /. ((card I) + 5) =
(Shift ((Stop SCM+FSA),((card I) + 5))) . (0 + ((card I) + 5))
by PARTFUN1:def 6
.=
halt SCM+FSA
by Lm2, Lm3, VALUED_1:def 12
;
A4:
( (card I) + 5 in dom (while=0 (a,I)) & dom (while=0 (a,I)) = (dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) )
by Th13, FUNCT_4:def 1;
then A5:
(card I) + 5 in dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))
by A1, XBOOLE_0:def 3;
A6: if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)) =
((((a =0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0))) ';' (Stop SCM+FSA)
by SCMFSA8B:def 1
.=
((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0))) ';' (Stop SCM+FSA)
;
then
card (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (card ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0)))) + (card (Stop SCM+FSA))
by SCMFSA6A:21;
then A7: card ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0))) =
(card (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) - (card (Stop SCM+FSA))
.=
((card I) + 6) - 1
by Th1, Lm1
.=
(card I) + 5
;
then A8:
not (card I) + 5 in dom ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0)))
;
A9:
dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (dom (Directed ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0))))) \/ (dom (Reloc ((Stop SCM+FSA),((card I) + 5))))
by A6, A7, FUNCT_4:def 1;
then
dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (dom ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0)))) \/ (dom (Reloc ((Stop SCM+FSA),((card I) + 5))))
by FUNCT_4:99;
then A10:
(card I) + 5 in dom (Reloc ((Stop SCM+FSA),((card I) + 5)))
by A5, A8, XBOOLE_0:def 3;
thus (while=0 (a,I)) . ((card I) + 5) =
((Directed ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0)))) +* (Reloc ((Stop SCM+FSA),((card I) + 5)))) . ((card I) + 5)
by A1, A4, A6, A7, FUNCT_4:def 1
.=
(Reloc ((Stop SCM+FSA),((card I) + 5))) . ((card I) + 5)
by A5, A9, A10, FUNCT_4:def 1
.=
IncAddr ((halt SCM+FSA),((card I) + 5))
by A2, A3, COMPOS_1:def 19
.=
halt SCM+FSA
by COMPOS_1:11
; verum