let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA
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 SCM+FSA;
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA
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 SCM+FSA; :: 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:105;
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 ) )
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then A5: Start-At (0,SCM+FSA) c= s by A4, XBOOLE_1:1;
A7: Directed I c= I ';' J by SCMFSA6A:55;
A8: Directed I c= P by A7, A3, XBOOLE_1:1;
then A9: P +* (Directed I) = P by FUNCT_4:104;
A11: P = P +* (I ';' J) by A3, FUNCT_4:104;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then B13: Start-At (0,SCM+FSA) c= s by A4, XBOOLE_1:1;
then A14: P +* I halts_on s by Th18, FUNCT_4:26;
hence A15: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by A5, Th37, A8; :: 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 (Initialized J)) implies (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁ )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁
then A18: x in (dom (Initialized J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A19: x in dom (Initialized J) by XBOOLE_0:def 4;
A20: x in Data-Locations SCM+FSA by A18, XBOOLE_0:def 4;

per cases ( x in dom J or x = intloc 0 or x = IC ) by A19, SCMFSA6A:44;

suppose A21: x in dom J ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁

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

end;

suppose A22: x = intloc 0 ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁

X9: Initialize ((intloc 0) .--> 1) c= Initialized I by FUNCT_4:26;
thus (DataPart (Initialized J)) . x = (Initialized J) . x by A20, FUNCT_1:72
.= 1 by A22, SCMFSA6A:46
.= (Initialized I) . x by A22, SCMFSA6A:46
.= (Initialize ((intloc 0) .--> 1)) . x by A22, X9, GRFUNC_1:8, SCMFSA6A:86
.= s . x by A22, A4, GRFUNC_1:8, SCMFSA6A:86
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . x by A22, Def4, B13, FUNCT_4:26
.= (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A20, FUNCT_1:72 ; :: thesis: verum

end;

suppose x = IC ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b₁

hence (DataPart (Initialized J)) . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A18, SCMFSA6A:37, XBOOLE_0:def 4; :: 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:26;
B24: dom (Initialized J) c= the carrier of SCM+FSA by RELAT_1:def 18;
J c= (P +* I) +* J by FUNCT_4:26;
then A25: (P +* I) +* J halts_on (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A23, Th19;
UU: DataPart (Initialized J) = (DataPart J) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:75
.= {} +* (DataPart (Initialize ((intloc 0) .--> 1))) by COMPOS_1:209
.= DataPart (Initialize ((intloc 0) .--> 1)) by FUNCT_4:21 ;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then B35: Start-At (0,SCM+FSA) c= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A23, XBOOLE_1:1;
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 B24, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:90;
then ( DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) ) by A17, UU, FUNCT_4:75, GRFUNC_1:8;
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:104;
s = s +* (Start-At (0,SCM+FSA)) by A5, FUNCT_4:104;
then NPP (Comput (P,s,(LifeSpan ((P +* I),s)))) = NPP (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by A11, Th40, A14;
then DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A26, COMPOS_1:138;
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 A5, A14, Th38, A8; :: 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:26;
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 ) )
X9: Initialize ((intloc 0) .--> 1) c= Initialized J by FUNCT_4:26;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A33: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:127, 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:72
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A33, FUNCT_1:72
.= (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:14, SCMFSA6A:86
.= (Initialized J) . (intloc 0) by X9, GRFUNC_1:8, SCMFSA6A:86
.= 1 by SCMFSA6A:46 ;
:: 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:5;
A36: J c= (P +* I) +* J by FUNCT_4:26;
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, B35;
then A37: CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A25, A34, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
hence A38: P halts_on s by EXTPRO_1:30; :: 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:8;
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, B35
.= halt SCM+FSA by A41, EXTPRO_1:5 ;
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 38, SCMFSA_2:124;
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:122;
hence contradiction by A25, A40, EXTPRO_1:def 14; :: 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:78;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A4, Th39, A43, A9, FUNCT_4:26; :: 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 13;
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 14;
A48: Initialize ((intloc 0) .--> 1) c= s by A4;
P +* I halts_on s by Th19, A48, FUNCT_4:26;
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 14; :: 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, B35;
assume A51: J is keeping_0 ; :: thesis: (Result (P,s)) . (intloc 0) = 1
X9: Initialize ((intloc 0) .--> 1) c= Initialized J by FUNCT_4:26;
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:5
.= (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:38
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A51, Def4, B35, FUNCT_4:26
.= (Initialize ((intloc 0) .--> 1)) . (intloc 0) by A23, GRFUNC_1:8, SCMFSA6A:86
.= (Initialized J) . (intloc 0) by X9, GRFUNC_1:8, SCMFSA6A:86
.= 1 by SCMFSA6A:46 ; :: thesis: verum

end;