set J1 = Stop SCM+FSA ;
set J = Stop SCM+FSA ;
let a be Int-Location ; for I being Program of SCM+FSA holds (while>0 a,I) . ((card I) + 5) = halt SCM+FSA
let I be Program of SCM+FSA ; (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:19;
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 JJ;
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 8
.=
halt SCM+FSA
by KK, JJ, 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 Th38, 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 2
.=
((((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:61;
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 Th2, LL
.=
(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 (ProgramPart (Relocated (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 (ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5))))
by FUNCT_4:105;
then A10:
(card I) + 5 in dom (ProgramPart (Relocated (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 )))) +* (ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5)))) . ((card I) + 5)
by A1, A4, A6, A7, FUNCT_4:def 1
.=
(ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5))) . ((card I) + 5)
by A5, A9, A10, FUNCT_4:def 1
.=
(Reloc (ProgramPart (Stop SCM+FSA )),((card I) + 5)) . ((card I) + 5)
by AMISTD_2:69
.=
(Reloc (Stop SCM+FSA ),((card I) + 5)) . ((card I) + 5)
by RELAT_1:209
.=
IncAddr (halt SCM+FSA ),((card I) + 5)
by A2, A3, SCMFSA_4:24
.=
halt SCM+FSA
by SCMFSA_4:8
; verum