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 J = Stop SCM+FSA ;
set f = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set i = a =0_goto (insloc ((card (Stop SCM+FSA )) + 3));
A1: dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} by FUNCOP_1:19;
3 <> (card I) + 4 by NAT_1:11;
then A2: not insloc 3 in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A1, TARSKI:def 1;
A3: insloc 3 in dom (while=0 a,I) by Th12;
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: insloc 3 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 );
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 ));
A6: 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 A7: not insloc 3 in dom ((Macro (a =0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
A8: 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
.= (((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 A6 ;
then 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 )))) \/ (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 A10: insloc 3 in dom (ProgramPart (Relocated ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),3)) by A5, A7, XBOOLE_0:def 3;
A11: insloc 0 in dom (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) by SCMFSA8A:47;
A12: (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 A13: (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 A15: insloc 0 in dom ((Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))) by A11, 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 A16: 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 A17: 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 A15, VALUED_1:def 12
.= (Directed (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) . (insloc 0 ) by A11, SCMFSA8A:28
.= goto (insloc ((card I) + 2)) by A11, A12, A13, SCMFSA8A:30 ;
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 A2, A3, A4, A8, 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 A5, A9, A10, 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 A16, A17, SCMFSA_4:24
.= goto ((insloc ((card I) + 2)) + 3) by SCMFSA_4:14
.= goto (insloc ((card I) + 5)) ; :: thesis: verum