set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (while>0 a,I) . (insloc 3) = goto (insloc ((card I) + 5))
let I be Program of SCM+FSA ; :: thesis: (while>0 a,I) . (insloc 3) = goto (insloc ((card I) + 5))
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 Mi = (Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA );
set G = Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1));
set J2 = (I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA );
set J1 = (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ));
A1: insloc 0 in dom (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) by SCMFSA8A:47;
A2: (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) . (insloc 0 ) = goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)) by SCMFSA8A:47
.= goto (insloc (((card I) + (card (Goto (insloc 0 )))) + 1)) by SCMFSA6A:61
.= goto (insloc (((card I) + 1) + 1)) by SCMFSA8A:29
.= goto (insloc ((card I) + (1 + 1))) ;
then A3: (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) . (insloc 0 ) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124;
dom ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))) = (dom (Directed (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),(card (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))))) by FUNCT_4:def 1
.= (dom (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),(card (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))))) by FUNCT_4:105 ;
then A4: insloc 0 in dom ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))) by A1, XBOOLE_0:def 3;
then (insloc 0 ) + 3 in { (il + 3) where il is Element of NAT : il in dom ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))) } ;
then A5: insloc 3 in dom (Shift ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3) by VALUED_1:def 12;
then A6: pi (Shift ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3),3 = (Shift ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3) . ((insloc 0 ) + 3) by AMI_1:def 47
.= ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))) . (insloc 0 ) by A4, VALUED_1:def 12
.= (Directed (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) . (insloc 0 ) by A1, SCMFSA8A:28
.= goto (insloc ((card I) + 2)) by A1, A2, A3, SCMFSA8A:30 ;
( dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} & 3 <> (card I) + 4 ) by FUNCOP_1:19, NAT_1:11;
then A7: not insloc 3 in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by TARSKI:def 1;
A8: card ((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) = (card (Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))))) + (card (Stop SCM+FSA )) by SCMFSA6A:61
.= 2 + 1 by SCMFSA7B:6, SCMFSA8A:17 ;
then A9: not insloc 3 in dom ((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
A10: ( insloc 3 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 Th37, FUNCT_4:def 1;
then A11: insloc 3 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A7, XBOOLE_0:def 3;
A12: 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
.= (((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 SCMFSA6A:67
.= ((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 ))) by SCMFSA6A:67
.= (Directed ((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA ))) +* (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3)) by A8 ;
then A13: 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 )))) \/ (dom (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3))) by 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 ))) \/ (dom (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3))) by FUNCT_4:105;
then A14: insloc 3 in dom (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3)) by A11, A9, XBOOLE_0:def 3;
thus (while>0 a,I) . (insloc 3) = ((Directed ((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA ))) +* (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3))) . (insloc 3) by A7, A10, A12, FUNCT_4:def 1
.= (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3)) . (insloc 3) by A11, A13, A14, FUNCT_4:def 1
.= (IncAddr [(Shift (ProgramPart ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )))),3)],3) . (insloc 3) by SCMFSA_5:2
.= (IncAddr (Shift ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3),3) . (insloc 3) by AMI_1:105
.= IncAddr (goto (insloc ((card I) + 2))),3 by A5, A6, SCMFSA_4:24
.= goto (insloc (((card I) + 2) + 3)) by SCMFSA_4:14
.= goto (insloc ((card I) + 5)) ; :: thesis: verum