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);
A6: I ';' J c= P +* (I ';' J) by FUNCT_4:25;
A7: 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 A7, XBOOLE_1:1;
then A8: (P +* (I ';' J)) +* (Directed I) = P +* (I ';' J) by FUNCT_4:98;
A9: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A10: I is_closed_on Initialize (Initialized S),P +* (I ';' J) by A2, SCMFSA8B:3;
A11: I is_halting_on Initialize (Initialized S),P +* (I ';' J) by A1, A2, A9, SCMFSA8B:5;
then A12: (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;
A13: 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;
A15: (Initialized S) . (intloc 0) = 1 by SCMFSA6A:38;
then (Initialize (Initialized S)) . (intloc 0) = 1 by A9, SCMFSA6A:7;
then A16: Initialized (Initialize (Initialize (Initialized S))) = Initialize (Initialized S) by SCMFSA8C:4;
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, A9, A15, 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 A16, A12, 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 A17: 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 ;
A18: 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 A10, A11, SCMFSA8A:22;
then A22: IC (Comput ((P +* (I ';' J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ';' J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A8;
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 A18, FUNCT_4:98, XBOOLE_1:2;
then A23: 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 A10, A11, A8, SCMFSA8A:22;
A24: Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
A25: Reloc (J,(card I)) c= P +* (I ';' J) by A6, A24, XBOOLE_1:1;

per cases by NAT_1:13;

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

A27: dom I c= dom (I ';' J) by SCMFSA6A:17;
A28: IC (Comput (((P +* (I ';' J)) +* I),(Initialize (Initialize (Initialized S))),k)) in dom I by A10, SCMFSA7B:def 6;
Comput (((P +* (I ';' J)) +* I),(Initialize (Initialize (Initialized S))),k) = Comput ((P +* (I ';' J)),(Initialize (Initialized S)),k) by A10, A11, A26, A8, 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 K376((I ';' J)) by A28, A27; :: thesis:

end;

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

then consider i being Nat such that
A29: 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 ;
A30: 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 by FUNCT_4:93;
then A31: 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 A17, A30, 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 A32: jloc + (card I) in dom (Reloc (J,(card I))) by A31;
A33: dom (Reloc (J,(card I))) c= dom (I ';' J) by A24, 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 A22, A23, A17, A13, A25, 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 K376((I ';' J)) by A29, A32, A33; :: thesis:

end;

end;