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 ))) +* (I +* (Start-At 0 ,SCM+FSA ));
set JAt = J +* (Start-At 0 ,SCM+FSA );
set s3 = (Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
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 ))) +* (I +* (Start-At 0 ,SCM+FSA )) = ((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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 ((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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) = (DataPart (Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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= (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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 ((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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = DataPart ((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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= (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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )) = ((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 RELAT_1:209;
dom (ProgramPart (Relocated J,(card I))) = dom (Reloc (ProgramPart J),(card I)) by AMISTD_2:69
.= { (j + (card I)) where j is Element of NAT : j in dom (ProgramPart J) } by AMISTD_2:70 ;
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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by AMI_1:123;
(IC (Comput (ProgramPart ((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 ((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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))),(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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized 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 ((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 ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialized S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + i)) by T, AMI_1:51 ;
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;