let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
set D = Data-Locations SCM+FSA;
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis:
let J be InitHalting Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
set s1 = s +* I;
set p1 = p +* I;
set s3 = (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J);
set p3 = (p +* I) +* J;
set m1 = LifeSpan ((p +* I),(s +* I));
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)));
A1: Initialize ((intloc 0) .--> 1) c= (I ';' J) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
A2: J c= (p +* I) +* J by FUNCT_4:26;
assume A3: Initialized (I ';' J) c= s ; :: thesis:
then A4: s = s +* (Initialized (I ';' J)) by FUNCT_4:79;
assume A5: I ';' J c= p ; :: thesis:
then A6: p +* (I ';' J) = p by FUNCT_4:79;
A7: I c= p +* I by FUNCT_4:26;
set s4 = Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1));
set p4 = p;
A8: ( Directed I c= I ';' J & I ';' J c= Initialized (I ';' J) ) by SCMFSA6A:26, SCMFSA6A:55;
then A9: Directed I c= p by A5, XBOOLE_1:1;
then A10: p = p +* (Directed I) by FUNCT_4:79;
reconsider m = ((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A11: dom (Directed I) = dom I by FUNCT_4:105;
A12: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A11, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A3, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A8, LATTICE2:8, XBOOLE_1:1
.= s by A3, LATTICE2:8 ;
then A13: Directed I c= s by FUNCT_4:26;
A14: (p +* I) +* (Directed I) = p +* (I +* (Directed I)) by FUNCT_4:15
.= p +* (Directed I) by A11, FUNCT_4:20
.= p by A10 ;
A15: Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by GRFUNC_1:8;
then A16: dom (Initialized J) c= the carrier of SCM+FSA by PARTFUN1:def 4;
A17: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
(I ';' J) +* (Initialize ((intloc 0) .--> 1)) c= s by A3, FUNCT_4:15;
then A18: Initialize ((intloc 0) .--> 1) c= s by A1, XBOOLE_1:1;
A19: Initialized I c= s +* I by A3, SCMFSA6A:52;
I c= p +* I by FUNCT_4:26;
then A20: p +* I halts_on s +* I by Th5, A19;
hence A21: IC (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = card I by A18, A12, Th21, FUNCT_4:26, A9; :: thesis:

A22: now

let x be set ; :: thesis:
assume x in dom (DataPart (Initialized J)) ; :: thesis:
then A23: x in (dom (Initialized J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A24: x in dom (Initialized J) by XBOOLE_0:def 4;
A25: x in Data-Locations SCM+FSA by A23, XBOOLE_0:def 4;

per cases by A24, SCMFSA6A:44;

suppose A26: x in dom J ; :: thesis:

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A26;
(DataPart (Initialized J)) . l = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . l by A25, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . x ; :: thesis:

end;

suppose A27: x = intloc 0 ; :: thesis:

thus (DataPart (Initialized J)) . x = (Initialized J) . x by A25, FUNCT_1:72
.= 1 by A27, SCMFSA6A:46
.= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) . x by A19, A27, Def3, A7
.= (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . x by A25, FUNCT_1:72 ; :: thesis:

end;

suppose x = IC ; :: thesis:

hence (DataPart (Initialized J)) . x = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . x by A23, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

A28: Initialize J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
A29: (p +* I) +* J halts_on (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by Th5, A2, A15;
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA) by A16, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) by RELAT_1:90;
then ( DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) ) by A22, FUNCT_4:75, GRFUNC_1:8;
then A30: DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by LATTICE2:8;
s +* I = (s +* (Initialize ((intloc 0) .--> 1))) +* I by A18, FUNCT_4:79
.= (s +* I) +* (Initialize ((intloc 0) .--> 1)) by Th19
.= s +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= s +* (Initialized I) by FUNCT_4:15 ;
then Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))), Comput (p,s,(LifeSpan ((p +* I),(s +* I)))) equal_outside NAT by A4, A20, Th24, A6;
then DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by A30, COMPOS_1:138;
hence A31: DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by A18, A13, Th22, A19, Th5, A7, A9; :: thesis:
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then I ';' J c= s by A3, XBOOLE_1:1;
then Reloc (J,(card I)) c= s by A17, XBOOLE_1:1;
hence A32: Reloc (J,(card I)) c= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) by AMI_1:81; :: thesis:
A33: Reloc (J,(card I)) c= p by A17, A5, XBOOLE_1:1;
A34: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A35: intloc 0 in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) . (intloc 0) = (DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))) . (intloc 0) by A31, FUNCT_1:72
.= ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A35, FUNCT_1:72
.= (Initialized J) . (intloc 0) by A34, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis:
A36: Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))))) by EXTPRO_1:5;
A37: Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
then IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))))) by A36, A21, A31, A32, Th12, A2, A33;
then A38: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A29, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
hence A39: p halts_on s by EXTPRO_1:30; :: thesis:

A40: now

let k be Element of NAT ; :: thesis:
assume ((LifeSpan ((p +* I),(s +* I))) + 1) + k < m ; :: thesis:
then A41: k < LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))) by XREAL_1:8;
assume A42: CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + k)))) = halt SCM+FSA ; :: thesis:
IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),k)))),(card I)) = CurInstr (p,(Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),k))) by A21, A31, A37, A32, Th12, A2, A33
.= halt SCM+FSA by A42, EXTPRO_1:5 ;
then InsCode (CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),k)))) = 0 by COMPOS_1:def 38, SCMFSA_2:124;
then CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),k))) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A29, A41, EXTPRO_1:def 14; :: thesis:

end;

let k be Element of NAT ; :: thesis:
assume A43: k < m ; :: thesis:

suppose k <= LifeSpan ((p +* I),(s +* I)) ; :: thesis:

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A19, A12, Th23, A7, A14; :: thesis:

end;

suppose LifeSpan ((p +* I),(s +* I)) < k ; :: thesis:

then (LifeSpan ((p +* I),(s +* I))) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A44: ((LifeSpan ((p +* I),(s +* I))) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
((LifeSpan ((p +* I),(s +* I))) + 1) + kk = k by A44;
hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A40, A43; :: thesis:

end;

end;

end;

then A45: for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A46: LifeSpan (p,s) = m by A38, A39, EXTPRO_1:def 14;
A47: s +* I = s +* (Initialized I) by A3, SCMFSA6A:51;
A48: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
I c= p +* I by FUNCT_4:26;
then A49: p +* I halts_on s +* I by Th5, A48, A47;
Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))) = Result ((p +* I),(s +* I)) by A49, EXTPRO_1:23;
hence LifeSpan (p,s) = ((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)))) by A45, A38, A39, EXTPRO_1:def 14; :: thesis:
A50: Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
A51: DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) = DataPart (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) by A21, A31, A37, A32, Th12, A2, A33;
assume A52: J is keeping_0 ; :: thesis:
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A39, A46, EXTPRO_1:23
.= (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by EXTPRO_1:5
.= (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by A51, SCMFSA6A:38
.= ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A28, A52, SCMFSA6B:def 4, A2
.= (Initialized J) . (intloc 0) by A34, A50, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: