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