let a be Int-Location ; :: thesis: 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 ; :: thesis: (while>0 a,I) . ((card I) + 5) = halt SCM+FSA
set I1 = I ';' (Goto (insloc 0 ));
set J = Stop SCM+FSA ;
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;
A1: dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} by FUNCOP_1:19;
(card I) + 5 <> insloc ((card I) + 4) ;
then A2: not (card I) + 5 in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A1, TARSKI:def 1;
A3: (card I) + 5 in dom (while>0 a,I) by Th38;
A4: 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 FUNCT_4:def 1;
then A5: (card I) + 5 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A2, A3, XBOOLE_0:def 3;
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 )));
set J1 = Stop SCM+FSA ;
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 2
.= ((((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 Th2, 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;
A10: 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 A11: (card I) + 5 in dom (ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5))) by A5, A8, XBOOLE_0:def 3;
(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 A13: insloc ((card I) + 5) in dom (Shift (Stop SCM+FSA ),((card I) + 5)) by VALUED_1:def 12;
then A14: pi (Shift (Stop SCM+FSA ),((card I) + 5)),((card I) + 5) = (Shift (Stop SCM+FSA ),((card I) + 5)) . ((insloc 0 ) + ((card I) + 5)) by AMI_1:def 47
.= halt SCM+FSA by SCMFSA8A:15, SCMFSA8A:16, VALUED_1:def 12 ;
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 A2, A3, A4, A6, A7, FUNCT_4:def 1
.= (ProgramPart (Relocated (Stop SCM+FSA ),((card I) + 5))) . ((card I) + 5) by A5, A10, A11, 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 A13, A14, SCMFSA_4:24
.= halt SCM+FSA by SCMFSA_4:8 ; :: thesis: verum