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 )
set Ins = NAT ;
set SAt = Start-At (insloc 0 );
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 IS = Initialize S;
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;
then A5: I is_closed_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A2, SCMFSA8B:6;
A6: I is_halting_on (Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 ))) by A1, A2, A4, SCMFSA8B:8;
then A7: ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
set s1 = ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )));
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 m1 = LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))));
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 (insloc 0 )))) | 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 (insloc 0 )))) . (intloc 0 ) = 1 by A4, SCMFSA6A:38;
then A10: ((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;
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, A9, 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 A8, 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 A10, A7, 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 A11: 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;
set PPR = [(ProgramPart (Relocated J,(card I)))];
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);
reconsider kk = DataPart (J +* (Start-At (insloc 0 ))) as Function ;
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 )))))) +* (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;
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)
A13: (Directed I) +* (Start-At (insloc 0 )) c= (I ';' J) +* (Start-At (insloc 0 )) by PRE_CIRC:3, SCMFSA6A:55;
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: 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;
(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 A13, XBOOLE_1:1;
then A16: (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 A17: 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 A5, A6, 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 A12, LATTICE2:8, XBOOLE_1:2;
then A18: 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 A5, A6, A16, SCMFSA8A:36;
A19: [(ProgramPart (Relocated J,(card I)))] c= I ';' J by FUNCT_4:26;
(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 A19, XBOOLE_1:1;
then A20: [(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;

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 A21: 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)

A22: dom I c= dom (I ';' J) by SCMFSA6A:56;
A23: IC (Computation (((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),k) in dom I by A5, SCMFSA7B:def 7;
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 A5, A6, A16, A21, AMI_1:121, SCMFSA8A:35;
hence IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J) by A23, A22; :: 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
A24: 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;
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;
(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 A15, FUNCT_4:79;
then A25: 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 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: insloc (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;
(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 A17, A18, A15, A11, A20, 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 ;
hence IC (Computation ((Initialize S) +* ((I ';' J) +* (Start-At (insloc 0 )))),k) in dom (I ';' J) by A24, A27, A28; :: thesis: verum

end;

end;