let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ';' J c= p 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 InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting Program of SCM+FSA
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ';' J c= p 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 InitHalting Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ';' J c= p 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: ( Initialize ((intloc 0) .--> 1) c= s & I ';' J c= p 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 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))));
A2: J c= (p +* I) +* J by FUNCT_4:25;
assume A3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I ';' J c= p or ( 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 ) ) )
then A4: s = Initialized s by FUNCT_4:98;
assume A5: I ';' J c= p ; :: 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 ) )
then A6: p +* (I ';' J) = p by FUNCT_4:98;
A7: I c= p +* I by FUNCT_4:25;
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
set p4 = p;
B9: Directed I c= I ';' J by SCMFSA6A:16;
then A9: Directed I c= p by A5, XBOOLE_1:1;
A10: p = p +* (Directed I) by A5, B9, 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 ;
A11: dom (Directed I) = dom I by FUNCT_4:99;
A14: (p +* I) +* (Directed I) = p +* (I +* (Directed I)) by FUNCT_4:14
.= p by A10, A11, FUNCT_4:19 ;
A15: 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 A16: dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by PARTFUN1:def 2;
A17: Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
JJ: I c= p +* I by FUNCT_4:25;
then A20: p +* I halts_on s by Def2, A3;
hence A21: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A3, Th21, A9; :: 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 ) )

A22: 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₁ )
assume 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₁
then A23: 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 B24: x in {(IC ),(intloc 0)} by diS, ENUMSET1:1;
A25: x in Data-Locations by A23, XBOOLE_0:def 4;

per cases ( x = intloc 0 or x = IC ) by B24, TARSKI:def 2;

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

thus (DataPart (Initialize ((intloc 0) .--> 1))) . x = 1 by A27, A25, FUNCT_1:49, SCMFSA6A:43
.= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . x by A27, Def3, A7, A3
.= (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x by A25, 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 A23, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A29: (p +* I) +* J halts_on (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by Def2, A2, A15;
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 A16, 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 BB: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by RELAT_1:61;
AA: 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;
CC: DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A22, BB, GRFUNC_1:2;
A30: DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by CC, AA, FUNCT_4:98;
KK: p +* I halts_on s by A3, Def2, JJ;
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A30, A4, A20, Th24, A6;
hence A31: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A3, Th22, A9, KK; :: 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 ) )
thus Reloc (J,(card I)) c= p by A5, A17, 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 ) )
A33: Reloc (J,(card I)) c= p by A17, A5, XBOOLE_1:1;
intloc 0 in Int-Locations by SCMFSA_2:2;
then A35: 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 A31, FUNCT_1:49
.= ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A35, 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 ) )
A36: 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;
A37: 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 A36, A21, A31, Th12, A2, A33;
then A38: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A29, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_1:11 ;
hence A39: 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 ) )

A40: 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 A41: k < LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) by XREAL_1:6;
assume A42: 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 A21, A31, A37, Th12, A2, A33
.= halt SCM+FSA by A42, 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 A29, A41, 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 A43: 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 k <= LifeSpan ((p +* I),s) ; :: thesis: CurInstr (p,(Comput (p,s,b₁))) <> halt SCM+FSA

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by Th23, A14, A3, 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;
reconsider kk = kk as Element of NAT by ORDINAL1:def 12;
((LifeSpan ((p +* I),s)) + 1) + kk = k by A44;
hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A40, A43; :: 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 A38, A39, EXTPRO_1:def 15;
I c= p +* I by FUNCT_4:25;
then A49: p +* I halts_on s by Def2, A3;
Comput ((p +* I),s,(LifeSpan ((p +* I),s))) = Result ((p +* I),s) by A49, 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, A38, A39, EXTPRO_1:def 15; :: thesis: ( J is keeping_0 implies (Result (p,s)) . (intloc 0) = 1 )
A50: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A51: 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 A21, A31, A37, Th12, A2, A33;
assume A52: J is keeping_0 ; :: thesis: (Result (p,s)) . (intloc 0) = 1
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)) + 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 A51, SCMFSA6A:7
.= ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A52, A2, SCMFSA6B:def 4
.= 1 by A50, GRFUNC_1:2, SCMFSA6A:41, SCMFSA6A:43 ; :: thesis: verum