set J1 = Stop SCM+FSA ;
set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of holds (while=0 a,I) . ((card I) + 5) = halt SCM+FSA
let I be Program of ; :: thesis: (while=0 a,I) . ((card I) + 5) = halt SCM+FSA
set I1 = I ';' (Goto (insloc 0 ));
set f = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set i = a =0_goto (insloc ((card (Stop SCM+FSA )) + 3));
set c5 = (card I) + 5;
set Lc5 = (card I) + 5;
set Mi = (((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )));
( dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} & (card I) + 5 <> insloc ((card I) + 4) ) by FUNCOP_1:19;
then A1: not (card I) + 5 in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by TARSKI:def 1;
(insloc 0 ) + ((card I) + 5) in { (il + ((card I) + 5)) where il is Element of NAT : il in dom (Stop SCM+FSA ) } by SCMFSA8A:15;
then A2: insloc ((card I) + 5) in dom (Shift (Stop SCM+FSA ),((card I) + 5)) by VALUED_1:def 12;
then A3: pi (Shift (Stop SCM+FSA ),((card I) + 5)),((card I) + 5) = (Shift (Stop SCM+FSA ),((card I) + 5)) . (0 + ((card I) + 5)) by AMI_1:def 47
.= halt SCM+FSA by SCMFSA8A:15, SCMFSA8A:16, 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 (insloc 0 ))),(Stop SCM+FSA ))) \/ (dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) ) by Th13, FUNCT_4:def 1;
then A5: (card I) + 5 in dom (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A1, XBOOLE_0:def 3;
A6: if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) = ((((a =0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) ';' (Stop SCM+FSA ) ;
then card (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (card ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 ))))) + (card (Stop SCM+FSA )) by SCMFSA6A:61;
then A7: card ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) = (card (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) - (card (Stop SCM+FSA ))
.= ((card I) + 6) - 1 by Th1, SCMFSA8A:17
.= (card I) + 5 ;
then A8: not (card I) + 5 in dom ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) by SCMFSA6A:15;
A9: dom (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom (Directed ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))))) \/ (dom (ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5)))) by A6, A7, FUNCT_4:def 1;
then dom (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom ((((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 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 (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 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
.= (IncAddr [(Shift (ProgramPart (Stop SCM+FSA )),((card I) + 5))],((card I) + 5)) . ((card I) + 5) by SCMFSA_5:2
.= (IncAddr (Shift (Stop SCM+FSA ),((card I) + 5)),((card I) + 5)) . ((card I) + 5) by AMI_1:105
.= IncAddr (halt SCM+FSA ),((card I) + 5) by A2, A3, SCMFSA_4:24
.= halt SCM+FSA by SCMFSA_4:8 ; :: thesis: verum