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

per cases by NAT_1:13;

suppose A21: k <= LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis:

A22: dom I c= dom (I ';' J) by SCMFSA6A:56;
A23: IC (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by A5, SCMFSA7B:def 7;
IC (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k) by A5, A6, A16, A21, AMI_1:121, SCMFSA8A:35;
hence IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k) in proj1 (I ';' J) by A23, A22; :: thesis:

end;

suppose (LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 <= k ; :: thesis:

then consider i being Nat such that
A24: k = ((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
reconsider jloc = IC (Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),i) as Element of NAT ;
(Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )) = ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) +* (J +* (Start-At 0 ,SCM+FSA )) by A15, FUNCT_4:79;
then A25: IC (Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),i) in dom J by A11, SCMFSA7B:def 7;
A26: dom (ProgramPart J) = dom J by AMI_1:105;
dom (ProgramPart (Relocated J,(card I))) = { (j + (card I)) where j is Element of NAT : j in dom (ProgramPart J) } by SCMFSA_5:3;
then A27: jloc + (card I) in dom (ProgramPart (Relocated J,(card I))) by A25, A26;
A28: dom (ProgramPart (Relocated J,(card I))) c= dom (I ';' J) by A19, RELAT_1:25;
T: ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by AMI_1:144;
(IC (Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),i)) + (card I) = IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)),i) by A17, A18, A15, A11, A20, SCMFSA8C:42
.= IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),(((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + i)) by AMI_1:51, T ;
hence IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k) in proj1 (I ';' J) by A24, A27, A28; :: thesis:

end;

end;