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 Initialized S and
A2: I is_closed_on Initialized S and
A3: J is_closed_on IExec (I,S) ; :: thesis:
set IS = Initialized S;
set s = (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)));
A4: DataPart (Initialized S) = DataPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A5: I is_closed_on (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A2, SCMFSA8B:6;
A6: I is_halting_on (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A1, A2, A4, SCMFSA8B:8;
then A7: ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA)))) halts_on ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
set s1 = ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I);
set JAt = J +* (Start-At (0,SCM+FSA));
set s3 = (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)));
set D = Int-Locations \/ FinSeq-Locations;
set m1 = LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)));
set IJ = I ';' J;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A8: dom (ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
A9: (Initialized S) . (intloc 0) = 1 by SCMFSA6C:3;
then ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) . (intloc 0) = 1 by A4, SCMFSA6A:38;
then A10: ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I) = ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I) by SCMFSA8C:18;
DataPart (IExec (I,S)) = DataPart (IExec (I,(Initialized S))) by SCMFSA8C:17
.= DataPart (IExec (I,((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))))) by A1, A2, A4, A9, SCMFSA8C:46
.= DataPart ((Result ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I)))) +* (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I)))) by A8, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) by A10, A7, EXTPRO_1:23 ;
then DataPart (IExec (I,S)) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A11: J is_closed_on (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) by A3, SCMFSA8B:6;
set PPR = ProgramPart (Relocated (J,(card I)));
set s4 = Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1));
reconsider kk = DataPart (J +* (Start-At (0,SCM+FSA))) as Function ;
A12: DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) = (DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))))))) +* 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 COMPOS_1:140;
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 (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
(I ';' J) +* (Start-At (0,SCM+FSA)) c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then (Directed I) +* (Start-At (0,SCM+FSA)) c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A13, XBOOLE_1:1;
then A16: (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* ((Directed I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
then A17: IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) = card I by A5, A6, SCMFSA8A:36;
DataPart (J +* (Start-At (0,SCM+FSA))) = {} by Th2;
then DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) by A12, LATTICE2:8, XBOOLE_1:2;
then A18: DataPart (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (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= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then I ';' J c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A14, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A19, XBOOLE_1:1;
then A20: ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1)) by AMI_1:81;

per cases by NAT_1:13;

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

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

end;

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

then consider i being Nat such that
A24: k = ((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
reconsider jloc = IC (Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),i)) as Element of NAT ;
(Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) = ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (J +* (Start-At (0,SCM+FSA))) by A15, FUNCT_4:79;
then A25: IC (Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),i)) in dom J by A11, SCMFSA7B:def 7;
A26: dom (ProgramPart J) = dom J by RELAT_1:209;
dom (ProgramPart (Relocated (J,(card I)))) = dom (Reloc ((ProgramPart J),(card I))) by COMPOS_1:116
.= { (j + (card I)) where j is Element of NAT : j in dom (ProgramPart J) } by COMPOS_1:117 ;
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 ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) by AMI_1:123;
(IC (Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),i))) + (card I) = IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))),i)) by A17, A18, A15, A11, A20, T, SCMFSA8C:42
.= IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1) + i))) by EXTPRO_1:5 ;
hence IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k)) in proj1 (I ';' J) by A24, A27, A28; :: thesis:

end;

end;