let p be Instruction-Sequence of SCM+FSA; :: thesis:
set D = Data-Locations ;
let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; :: thesis:
let J be really-closed InitHalting Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
set s1 = s +* EP;
set p1 = p +* I;
set s3 = (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1));
set p3 = (p +* I) +* J;
set m1 = LifeSpan ((p +* I),s);
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))));
A1: J c= (p +* I) +* J by FUNCT_4:25;
assume A2: Initialize ((intloc 0) .--> 1) c= s ; :: thesis:
then A3: s = Initialized s by FUNCT_4:98;
assume A4: I ";" J c= p ; :: thesis:
then A5: p +* (I ";" J) = p by FUNCT_4:98;
A6: I c= p +* I by FUNCT_4:25;
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
set p4 = p;
A7: Directed I c= I ";" J by SCMFSA6A:16;
then A8: Directed I c= p by A4, XBOOLE_1:1;
A9: p = p +* (Directed I) by A4, A7, FUNCT_4:98, XBOOLE_1:1;
reconsider m = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))) as Element of NAT by ORDINAL1:def 12;
A10: dom (Directed I) = dom I by FUNCT_4:99;
A11: (p +* I) +* (Directed I) = p +* (I +* (Directed I)) by FUNCT_4:14
.= p by A9, A10, FUNCT_4:19 ;
A12: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then dom (Initialize ((intloc 0) .--> 1)) c= dom ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by GRFUNC_1:2;
then A13: dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by PARTFUN1:def 2;
A14: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
A15: I c= p +* I by FUNCT_4:25;
then A16: p +* I halts_on s by Def1, A2;
hence A17: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A2, Th9, A8; :: thesis:

A18: now :: thesis:

let x be object ; :: thesis:
assume x in dom (DataPart (Initialize ((intloc 0) .--> 1))) ; :: thesis:
then A19: x in (dom (Initialize ((intloc 0) .--> 1))) /\ (Data-Locations ) by RELAT_1:61;
then x in dom (Initialize ((intloc 0) .--> 1)) by XBOOLE_0:def 4;
then A20: x in {(IC ),(intloc 0)} by Lm2, ENUMSET1:1;
A21: x in Data-Locations by A19, XBOOLE_0:def 4;

per cases by A20, TARSKI:def 2;

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

thus (DataPart (Initialize ((intloc 0) .--> 1))) . x = 1 by A22, A21, FUNCT_1:49, SCMFSA_M:12
.= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . x by A22, Def2, A6, A2
.= (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x by A21, FUNCT_1:49 ; :: thesis:

end;

suppose x = IC ; :: thesis:

then not x in Data-Locations by STRUCT_0:3;
hence (DataPart (Initialize ((intloc 0) .--> 1))) . x = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x by A19, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

A23: (p +* I) +* J halts_on (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by Def1, A1, A12;
dom (DataPart (Initialize ((intloc 0) .--> 1))) = (dom (Initialize ((intloc 0) .--> 1))) /\ (Data-Locations ) by RELAT_1:61;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= the carrier of SCM+FSA /\ (Data-Locations ) by A13, XBOOLE_1:26;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= (dom (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) /\ (Data-Locations ) by PARTFUN1:def 2;
then A24: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by RELAT_1:61;
A25: DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71;
A26: DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A18, A24, GRFUNC_1:2;
A27: DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A26, A25, FUNCT_4:98;
A28: p +* I halts_on s by A2, Def1, A15;
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A27, A3, A16, Th12, A5;
hence A29: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A2, Th10, A8, A28; :: thesis:
thus Reloc (J,(card I)) c= p by A4, A14, XBOOLE_1:1; :: thesis:
A30: Reloc (J,(card I)) c= p by A14, A4, XBOOLE_1:1;
intloc 0 in Int-Locations by AMI_2:def 16;
then A31: intloc 0 in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = (DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) . (intloc 0) by A29, FUNCT_1:49
.= ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A31, FUNCT_1:49
.= 1 by FUNCT_4:13, SCMFSA_M:10, SCMFSA_M:12 ;
:: thesis:
A32: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))))) by EXTPRO_1:4;
A33: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))) by A32, A17, A29, Th4, A1, A30;
then A34: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A23, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A35: p halts_on s by EXTPRO_1:29; :: thesis:

A36: now :: thesis:

let k be Nat; :: thesis:
assume ((LifeSpan ((p +* I),s)) + 1) + k < m ; :: thesis:
then A37: k < LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) by XREAL_1:6;
assume A38: CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA ; :: thesis:
A39: IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I)) = CurInstr (p,(Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),k))) by A17, A29, A33, Th4, A1, A30
.= halt SCM+FSA by A38, EXTPRO_1:4 ;
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
then InsCode (CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k)))) = 0 by A39, COMPOS_0:def 9;
then CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA by SCMFSA_2:95;
hence contradiction by A23, A37, EXTPRO_1:def 15; :: thesis:

end;

now :: thesis:

let k be Nat; :: thesis:
assume A40: k < m ; :: thesis:

per cases ;

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

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by Th11, A11, A2, FUNCT_4:25; :: thesis:

end;

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

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

end;

end;

end;

then A42: for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A43: LifeSpan (p,s) = m by A34, A35, EXTPRO_1:def 15;
I c= p +* I by FUNCT_4:25;
then A44: p +* I halts_on s by Def1, A2;
Comput ((p +* I),s,(LifeSpan ((p +* I),s))) = Result ((p +* I),s) by A44, EXTPRO_1:23;
hence LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) by A42, A34, A35, EXTPRO_1:def 15; :: thesis:
A45: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A46: DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) by A17, A29, A33, Th4, A1, A30;
assume A47: J is keeping_0 ; :: thesis:
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A35, A43, EXTPRO_1:23
.= (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) by EXTPRO_1:4
.= (Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) by A46, SCMFSA_M:2
.= ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A47, A1, SCMFSA6B:def 4
.= 1 by A45, GRFUNC_1:2, SCMFSA_M:10, SCMFSA_M:12 ; :: thesis: