let S be State of ; :: thesis:
let I, J be Program of ; :: thesis:
set SAt = Start-At (insloc 0 );
assume that
A1: I is_halting_on Initialize S and
A2: J is_halting_on IExec I,S and
A3: I is_closed_on Initialize S and
A4: J is_closed_on IExec I,S ; :: thesis:
set s = (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )));
A5: DataPart (Initialize S) = DataPart ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
then A6: I is_halting_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A1, A3, SCMFSA8B:8;
then A7: ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))) halts_on ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) by SCMFSA7B:def 8;
set s1 = ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )));
A8: (Initialize S) . (intloc 0 ) = 1 by SCMFSA6C:3;
then ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) . (intloc 0 ) = 1 by A5, SCMFSA6A:38;
then A9: ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) = ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (Initialized I) by SCMFSA8C:18;
set JAt = J +* (Start-At (insloc 0 ));
set s3 = (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )));
set D = Int-Locations \/ FinSeq-Locations ;
set m3 = LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))));
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A10: dom (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A11: DataPart (IExec I,S) = DataPart (IExec I,(Initialize S)) by SCMFSA8C:17
.= DataPart (IExec I,((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))))) by A1, A3, A5, A8, SCMFSA8C:46
.= DataPart ((Result (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (Initialized I))) +* (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (Initialized I))) by A10, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) by A9, A7, AMI_1:122 ;
then J is_halting_on Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) by A2, A4, SCMFSA8B:8;
then A12: ProgramPart ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))) halts_on (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))) by SCMFSA7B:def 8;
DataPart (IExec I,S) = DataPart ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))) by A11, SCMFSA8A:11;
then A13: J is_closed_on (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))) by A4, SCMFSA8B:6;
dom (I ';' J) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A14: I ';' J c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:33;
A15: ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
set m1 = LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))));
set s4 = Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1);
A16: (Directed I) +* (Start-At (insloc 0 )) c= (I ';' J) +* (Start-At (insloc 0 )) by PRE_CIRC:3, SCMFSA6A:55;
(I ';' J) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then (Directed I) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A16, XBOOLE_1:1;
then A17: (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) = ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:79;
(I ';' J) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I ';' J c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A14, XBOOLE_1:1;
then ProgramPart (Relocated J,(card I)) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A15, XBOOLE_1:1;
then A18: [(ProgramPart (Relocated J,(card I)))] c= Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1) by AMI_1:81;
reconsider m = ((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1) + (LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))))) as Element of NAT ;
reconsider kk = DataPart (J +* (Start-At (insloc 0 ))) as Function ;
A19: DataPart ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))) = (DataPart (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))))) +* kk by FUNCT_4:75;
take m ; :: according to AMI_1:def 20,SCMFSA7B:def 8 :: thesis:
IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),m) in NAT by AMI_1:def 4;
hence IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),m) in dom (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))))) by AMI_1:143; :: thesis:
A20: J +* (Start-At (insloc 0 )) c= (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A21: I is_closed_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A3, A5, SCMFSA8B:6;
then A22: IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) by A6, A17, SCMFSA8A:36;
DataPart (J +* (Start-At (insloc 0 ))) = {} by Th2;
then DataPart (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) = DataPart ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))) by A19, LATTICE2:8, XBOOLE_1:2;
then DataPart (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))) by A21, A6, A17, SCMFSA8A:36;
then IncAddr (CurInstr (Computation ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))),(LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))))))),(card I) = CurInstr (Computation (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1)),(LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))))) by A22, A20, A13, A18, SCMFSA8C:42;
then IncAddr (CurInstr (Computation ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 )))),(LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))))))),(card I) = CurInstr (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1) + (LifeSpan ((Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))))) +* (J +* (Start-At (insloc 0 ))))))) by AMI_1:51;
then CurInstr (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),m) = IncAddr (halt SCM+FSA ),(card I) by A12, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
hence (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))))) . (IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),m)) = halt SCM+FSA by AMI_1:145; :: thesis: