let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed parahalting keeping_0 Program of
for J being really-closed parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
set D = Data-Locations ;
let I be really-closed parahalting keeping_0 Program of ; :: thesis: for J being really-closed parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let J be really-closed parahalting Program of ; :: thesis: for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; :: thesis: ( I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s implies ( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) ) )
set s3 = (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1));
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: dom (Directed I) = dom I by FUNCT_4:99;
assume that
A2: I ";" J c= P and
A3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A4: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then A5: Start-At (0,SCM+FSA) c= s by A3, XBOOLE_1:1;
A6: Directed I c= I ";" J by SCMFSA6A:16;
A7: P +* (Directed I) = P by A6, A2, FUNCT_4:98, XBOOLE_1:1;
A8: P = P +* (I ";" J) by A2, FUNCT_4:98;
A9: s is 0 -started State of SCM+FSA by A5, MEMSTR_0:29;
then A10: P +* I halts_on s by Th1, FUNCT_4:25;
hence A11: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th11, A6, A2, A9, XBOOLE_1:1; :: thesis: ( DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )

A12: now :: thesis: for x being object st x in dom (DataPart (Initialize ((intloc 0) .--> 1))) holds
(DataPart (Initialize ((intloc 0) .--> 1))) . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x

let x be object ; :: thesis: ( x in dom (DataPart (Initialize ((intloc 0) .--> 1))) implies (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁ )
A13: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (Initialize ((intloc 0) .--> 1)) by RELAT_1:60;
assume A14: x in dom (DataPart (Initialize ((intloc 0) .--> 1))) ; :: thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁
A15: x in Data-Locations by A14, RELAT_1:57;
A16: I c= P +* I by FUNCT_4:25;

per cases ( x = intloc 0 or x = IC ) by A14, A13, SCMFSA_M:11, TARSKI:def 2;

suppose A17: x = intloc 0 ; :: thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁

then A18: x in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
thus (DataPart (Initialize ((intloc 0) .--> 1))) . x = 1 by A17, A15, FUNCT_1:49, SCMFSA_M:12
.= s . x by A3, A18, A17, GRFUNC_1:2, SCMFSA_M:12
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . x by A17, Def2, A16, A9
.= (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A15, FUNCT_1:49 ; :: thesis: verum

end;

suppose x = IC ; :: thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁

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 A14, RELAT_1:57; :: thesis: verum

end;

end;

end;

set s4 = Comput (P,s,((LifeSpan ((P +* I),s)) + 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;
A19: Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
J c= (P +* I) +* J by FUNCT_4:25;
then A20: (P +* I) +* J halts_on (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A19, Th2;
A21: dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by RELAT_1:def 18;
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 A21, 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 dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:61;
then ( 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))) & DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) ) by A12, FUNCT_4:71, GRFUNC_1:2;
then A22: DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:98;
s = s +* (Start-At (0,SCM+FSA)) by A4, A3, FUNCT_4:98, XBOOLE_1:1;
then DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A22, A8, Th14, A10;
hence A23: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A10, Th12, A6, A2, A9, XBOOLE_1:1; :: thesis: ( Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
hence A24: Reloc (J,(card I)) c= P by A2, XBOOLE_1:1; :: thesis: ( (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
intloc 0 in Int-Locations by AMI_2:def 16;
then A25: 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 A23, FUNCT_1:49
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A25, FUNCT_1:49
.= 1 by FUNCT_4:13, SCMFSA_M:10, SCMFSA_M:12 ;
:: thesis: ( P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A26: 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;
A27: J c= (P +* I) +* J 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,(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 A11, A23, Th6, A24;
then A28: CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A20, A26, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A29: P halts_on s by EXTPRO_1:29; :: thesis: ( LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )

A30: now :: thesis: for k being Element of NAT st ((LifeSpan ((P +* I),s)) + 1) + k < m holds
not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA

let k be Element of NAT ; :: thesis: ( ((LifeSpan ((P +* I),s)) + 1) + k < m implies not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA )
assume ((LifeSpan ((P +* I),s)) + 1) + k < m ; :: thesis: not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA
then A31: k < LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) by XREAL_1:6;
assume A32: CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA ; :: thesis: contradiction
A33: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
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 A11, A23, Th6, A27, A24
.= halt SCM+FSA by A32, EXTPRO_1:4 ;
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 A33, 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 A20, A31, EXTPRO_1:def 15; :: thesis: verum

end;

now :: thesis: for k being Nat st k < m holds
CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA

let k be Nat; :: thesis: ( k < m implies CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA )
assume A34: k < m ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

per cases ( k <= LifeSpan ((P +* I),s) or LifeSpan ((P +* I),s) < k ) ;

suppose A35: k <= LifeSpan ((P +* I),s) ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

(P +* I) +* (Directed I) = P +* (Directed I) by A1, FUNCT_4:74;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A3, Th13, A35, A7, FUNCT_4:25; :: thesis: verum

end;

suppose LifeSpan ((P +* I),s) < k ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

then (LifeSpan ((P +* I),s)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A36: ((LifeSpan ((P +* I),s)) + 1) + kk = k by NAT_1:10;
kk in NAT by ORDINAL1:def 12;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A30, A34, A36; :: thesis: verum

end;

end;

end;

then A37: for k being Nat st CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA holds
m <= k ;
then A38: LifeSpan (P,s) = m by A28, A29, EXTPRO_1:def 15;
P +* I halts_on s by Th2, A3, FUNCT_4:25;
then Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Result ((P +* I),s) by 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 A37, A28, A29, EXTPRO_1:def 15; :: thesis: ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 )

hereby :: thesis: verum

A39: 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 A11, A23, Th6, A27, A24;
A40: J c= (P +* I) +* J by FUNCT_4:25;
assume A41: J is keeping_0 ; :: thesis: (Result (P,s)) . (intloc 0) = 1
thus (Result (P,s)) . (intloc 0) = (Comput (P,s,m)) . (intloc 0) by A29, A38, 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 A39, SCMFSA_M:2
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A41, A40
.= 1 by A19, GRFUNC_1:2, SCMFSA_M:10, SCMFSA_M:12 ; :: thesis: verum

end;