let P be Instruction-Sequence of SCM+FSA; :: thesis:
let S be State of SCM+FSA; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
assume that
A1: I is_halting_on Initialized S,P and
A2: I is_closed_on Initialized S,P and
A3: J is_closed_on IExec (I,P,S),P ; :: thesis:
set IS = Initialized S;
set PS = P;
set s = Initialize (Initialized S);
set p = P +* (I ";" J);
A4: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A5: Directed I c= I ";" J by SCMFSA6A:16;
I ";" J c= P +* (I ";" J) by FUNCT_4:25;
then Directed I c= P +* (I ";" J) by A5, XBOOLE_1:1;
then A6: (P +* (I ";" J)) +* (Directed I) = P +* (I ";" J) by FUNCT_4:98;
A7: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A8: I is_closed_on Initialize (Initialized S),P +* (I ";" J) by A2, SCMFSA8B:3;
A9: I is_halting_on Initialize (Initialized S),P +* (I ";" J) by A1, A2, A7, SCMFSA8B:5;
then A10: (P +* (I ";" J)) +* I halts_on Initialize (Initialize (Initialized S)) by SCMFSA7B:def 7;
set s1 = Initialize (Initialize (Initialized S));
set p1 = (P +* (I ";" J)) +* I;
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))));
set p3 = ((P +* (I ";" J)) +* I) +* J;
A11: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
set m1 = LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))));
set IJ = I ";" J;
A12: (Initialized S) . (intloc 0) = 1 by SCMFSA_M:9;
then (Initialize (Initialized S)) . (intloc 0) = 1 by A7, SCMFSA_M:2;
then A13: Initialized (Initialize (Initialize (Initialized S))) = Initialize (Initialized S) by SCMFSA_M:18;
DataPart (IExec (I,P,S)) = DataPart (IExec (I,P,(Initialized S))) by SCMFSA8C:3
.= DataPart (IExec (I,(P +* (I ";" J)),(Initialize (Initialized S)))) by A1, A2, A7, A12, SCMFSA8C:20
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S))))) by SCMFSA6B:def 1
.= DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) by A13, A10, EXTPRO_1:23 ;
then DataPart (IExec (I,P,S)) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by MEMSTR_0:79;
then A14: J is_closed_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))),((P +* (I ";" J)) +* I) +* J by A3, SCMFSA8B:3;
set PPR = Reloc (J,(card I));
set s4 = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1));
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A15: DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) = (DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) +* kk by FUNCT_4:71;
let k be Element of NAT ; :: according to SCMFSA7B:def 6 :: thesis:
IC (Comput (((P +* (I ";" J)) +* (Directed I)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A8, A9, SCMFSA8A:22;
then A16: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A6;
DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
then DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A15, FUNCT_4:98, XBOOLE_1:2;
then A17: DataPart (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A8, A9, A6, SCMFSA8A:22;
A18: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
A19: Reloc (J,(card I)) c= P +* (I ";" J) by A4, A18, XBOOLE_1:1;

per cases by NAT_1:13;

suppose A20: k <= LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))) ; :: thesis:

A21: dom I c= dom (I ";" J) by SCMFSA6A:17;
A22: IC (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k)) in dom I by A8, SCMFSA7B:def 6;
Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k) = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k) by A8, A9, A20, A6, SCMFSA8A:21;
then IC (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k)) = IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) ;
hence IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J)) by A22, A21; :: thesis:

end;

suppose (LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1 <= k ; :: thesis:

then consider i being Nat such that
A23: k = ((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
reconsider jloc = IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i)) as Element of NAT ;
A24: Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = Initialize (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) ;
(((P +* (I ";" J)) +* I) +* J) +* J = ((P +* (I ";" J)) +* I) +* J ;
then A25: IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i)) in dom J by A14, A24, SCMFSA7B:def 6;
dom (Reloc (J,(card I))) = { (j + (card I)) where j is Element of NAT : j in dom J } by COMPOS_1:33;
then A26: jloc + (card I) in dom (Reloc (J,(card I))) by A25;
A27: dom (Reloc (J,(card I))) c= dom (I ";" J) by A18, RELAT_1:11;
(IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i))) + (card I) = IC (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),i)) by A16, A17, A14, A11, A19, SCMFSA8C:16
.= IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + i))) by EXTPRO_1:4 ;
hence IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J)) by A23, A26, A27; :: thesis:

end;

end;