let S be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialize S & I is_closed_on Initialize S & J is_closed_on IExec I,S holds
I ';' J is_closed_on Initialize S
let I, J be Program of SCM+FSA ; :: thesis: ( I is_halting_on Initialize S & I is_closed_on Initialize S & J is_closed_on IExec I,S implies I ';' J is_closed_on Initialize S )
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: I ';' J is_closed_on Initialize S
set IJ = I ';' J;
set IS = Initialize S;
set SAt = Start-At (insloc 0 );
set s = (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )));
A4: DataPart (Initialize S) = DataPart ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
A5: (I ';' J) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A6: (Initialize S) . (intloc 0 ) = 1 by SCMFSA6C:3;
set JAt = J +* (Start-At (insloc 0 ));
set s1 = ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (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 m1 = LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))));
set Ins = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) . (intloc 0 ) = 1 by A4, A6, SCMFSA6A:38;
then A7: ((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;
A8: I is_closed_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A2, A4, SCMFSA8B:6;
A9: I is_halting_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A1, A2, A4, SCMFSA8B:8;
then A10: ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
reconsider kk = DataPart (J +* (Start-At (insloc 0 ))) as Function ;
A11: 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;
DataPart (J +* (Start-At (insloc 0 ))) = {} by Th2;
then A12: 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 A11, LATTICE2:8, XBOOLE_1:2;
dom (I ';' J) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A13: I ';' J c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:33;
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);
A14: (I ';' J) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
(Directed I) +* (Start-At (insloc 0 )) c= (I ';' J) +* (Start-At (insloc 0 )) by PRE_CIRC:3, SCMFSA6A:55;
then (Directed I) +* (Start-At (insloc 0 )) c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A14, XBOOLE_1:1;
then A15: (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;
then A16: 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 A8, A9, SCMFSA8A:36;
A17: 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 A8, A9, A12, A15, SCMFSA8A:36;
A18: 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;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A19: dom (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
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, A2, A4, A6, 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 A19, 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 A7, A10, AMI_1:122 ;
then 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 SCMFSA8A:11;
then A20: 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 A3, SCMFSA8B:6;
A21: I ';' J c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A5, A13, XBOOLE_1:1;
set PPR = [(ProgramPart (Relocated J,(card I)))];
A22: [(ProgramPart (Relocated J,(card I)))] c= I ';' J by FUNCT_4:26;
then [(ProgramPart (Relocated J,(card I)))] c= (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A21, XBOOLE_1:1;
then A23: [(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;
let k be Element of NAT ; :: according to SCMFSA7B:def 7 :: thesis: IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J)

per cases ( k <= LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))) or (LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1 <= k ) by NAT_1:13;

suppose S: k <= LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))) ; :: thesis: IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J)

A24: IC (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) by A15, A8, A9, S, AMI_1:121, SCMFSA8A:35;
A25: IC (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),k) in dom I by A8, SCMFSA7B:def 7;
dom I c= dom (I ';' J) by SCMFSA6A:56;
hence IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J) by A24, A25; :: thesis: verum

end;

suppose (LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1 <= k ; :: thesis: IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J)

then consider i being Nat such that
A26: k = ((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))))) + 1) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A27: (IC (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 )))),i)) + (card I) = IC (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)),i) by A16, A17, A18, A20, A23, SCMFSA8C:42
.= 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) + i)) by AMI_1:51 ;
(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 ))) = ((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 )))) +* (J +* (Start-At (insloc 0 ))) by A18, FUNCT_4:79;
then A28: IC (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 )))),i) in dom J by A20, SCMFSA7B:def 7;
reconsider jloc = IC (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 )))),i) as Element of NAT by AMI_1:def 4;
A31: dom [(ProgramPart (Relocated J,(card I)))] = { (j + (card I)) where j is Element of NAT : j in dom (ProgramPart J) } by SCMFSA_5:3;
dom (ProgramPart J) = dom J by AMI_1:105;
then A32: insloc (jloc + (card I)) in dom [(ProgramPart (Relocated J,(card I)))] by A28, A31;
dom [(ProgramPart (Relocated J,(card I)))] c= dom (I ';' J) by A22, RELAT_1:25;
hence IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J) by A26, A27, A32; :: thesis: verum

end;

end;