let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being parahalting keeping_0 Program of
for J being 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 parahalting keeping_0 Program of ; :: thesis: for J being 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 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
A3: I ';' J c= P and
A4: 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 ) )
B5: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then A5: Start-At (0,SCM+FSA) c= s by A4, XBOOLE_1:1;
A7: Directed I c= I ';' J by SCMFSA6A:16;
A9: P +* (Directed I) = P by A7, A3, FUNCT_4:98, XBOOLE_1:1;
A11: P = P +* (I ';' J) by A3, FUNCT_4:98;
C13: s is 0 -started State of SCM+FSA by A5, MEMSTR_0:29;
then A14: P +* I halts_on s by Th18, FUNCT_4:25;
hence A15: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th37, A7, A3, C13, 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 ) )

A17: now

let x be set ; :: 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₁ )
DD: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (Initialize ((intloc 0) .--> 1)) by RELAT_1:60;
assume Z: 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₁
A20: x in Data-Locations by Z, RELAT_1:57;
II: I c= P +* I by FUNCT_4:25;

per cases ( x = intloc 0 or x = IC ) by Z, DD, SCMFSA6A:42, TARSKI:def 2;

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

then B22: x in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:42, TARSKI:def 2;
thus (DataPart (Initialize ((intloc 0) .--> 1))) . x = 1 by A22, A20, FUNCT_1:49, SCMFSA6A:43
.= s . x by A4, B22, A22, GRFUNC_1:2, SCMFSA6A:43
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . x by A22, Def4, II, C13
.= (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A20, 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 Z, 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 ;
A23: 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 A25: (P +* I) +* J halts_on (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A23, Th19;
B24: 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 B24, 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 A17, FUNCT_4:71, GRFUNC_1:2;
then A26: 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 B5, A4, 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 A26, A11, Th40, A14;
hence A28: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A14, Th38, A7, A3, C13, 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 FUNCT_4:25;
hence A31: Reloc (J,(card I)) c= P by A3, 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 SCMFSA_2:2;
then A33: 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 A28, FUNCT_1:49
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A33, FUNCT_1:49
.= 1 by FUNCT_4:13, SCMFSA6A:41, SCMFSA6A:43 ;
:: 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 ) )
A34: 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;
A36: 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 A15, A28, Th27, A31;
then A37: CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A25, A34, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_1:11 ;
hence A38: 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 ) )

A39: now

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 A40: k < LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) by XREAL_1:6;
assume A41: CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA ; :: thesis: contradiction
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 A15, A28, Th27, A36, A31
.= halt SCM+FSA by A41, 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 COMPOS_1:def 17, SCMFSA_2:97;
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 A25, A40, EXTPRO_1:def 15; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA )
assume A42: 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 A43: 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 A4, Th39, A43, A9, 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
A44: ((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 A39, A42, A44; :: thesis: verum

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 A37, A38, EXTPRO_1:def 15;
P +* I halts_on s by Th19, A4, 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 A45, A37, A38, EXTPRO_1:def 15; :: thesis: ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 )

hereby :: thesis: verum

A50: 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 A15, A28, Th27, A36, A31;
IJ: J c= (P +* I) +* J by FUNCT_4:25;
assume A51: J is keeping_0 ; :: thesis: (Result (P,s)) . (intloc 0) = 1
thus (Result (P,s)) . (intloc 0) = (Comput (P,s,m)) . (intloc 0) by A38, A46, 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 A50, SCMFSA6A:7
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A51, Def4, IJ
.= 1 by A23, GRFUNC_1:2, SCMFSA6A:41, SCMFSA6A:43 ; :: thesis: verum

end;