let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

set A = NAT ;

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= p implies for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )

set s2 = s +* EP;

set p2 = p +* (Directed I);

set m = LifeSpan (p,s);

assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I c= p or for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )

assume A2: I c= p ; :: thesis: for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

then A3: p halts_on s by A1, Def1;

set lk = IC (Comput (p,s,k));

IC s = 0 by A1, MEMSTR_0:47;

then IC s in dom I by AFINSQ_1:65;

then A19: ( IC (Comput (p,s,k)) in dom I & dom I = dom (Directed I) ) by A2, AMISTD_1:21, FUNCT_4:99;

then A20: (Directed I) . (IC (Comput (p,s,k))) in rng (Directed I) by FUNCT_1:def 3;

assume k <= LifeSpan (p,s) ; :: thesis: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

then IC (Comput (p,s,k)) = IC (Comput ((p +* (Directed I)),(s +* EP),k)) by A4;

then A21: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),k))) = (p +* (Directed I)) . (IC (Comput (p,s,k))) by PBOOLE:143

.= (Directed I) . (IC (Comput (p,s,k))) by A19, FUNCT_4:13 ;

assume CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) = halt SCM+FSA ; :: thesis: contradiction

hence contradiction by A21, A20, SCMFSA6A:1; :: thesis: verum

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

set A = NAT ;

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= p implies for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )

set s2 = s +* EP;

set p2 = p +* (Directed I);

set m = LifeSpan (p,s);

assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I c= p or for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )

assume A2: I c= p ; :: thesis: for k being Nat st k <= LifeSpan (p,s) holds

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

then A3: p halts_on s by A1, Def1;

A4: now :: thesis: for k being Nat st k <= LifeSpan (p,s) holds

Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)

let k be Nat; :: thesis: ( k <= LifeSpan (p,s) implies CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)

set s1 = s +* EP;

set p1 = p +* (I ";" I);

let k be Nat; :: thesis: ( k <= LifeSpan (p,s) implies Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k) )

defpred S_{1}[ Nat] means ( $1 <= k implies Comput ((p +* (I ";" I)),(s +* EP),$1) = Comput ((p +* (Directed I)),(s +* EP),$1) );

assume A5: k <= LifeSpan (p,s) ; :: thesis: Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)

A6: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A18, A6);

then Comput ((p +* (I ";" I)),(s +* EP),k) = Comput ((p +* (Directed I)),(s +* EP),k) ;

hence Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k) by A1, A3, A5, Th8, A2; :: thesis: verum

end;set p1 = p +* (I ";" I);

let k be Nat; :: thesis: ( k <= LifeSpan (p,s) implies Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k) )

defpred S

assume A5: k <= LifeSpan (p,s) ; :: thesis: Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)

A6: for n being Nat st S

S

proof

A18:
S
A7:
Directed I c= I ";" I
by SCMFSA6A:16;

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

A8: dom I c= dom (I ";" I) by SCMFSA6A:17;

assume A9: ( n <= k implies Comput ((p +* (I ";" I)),(s +* EP),n) = Comput ((p +* (Directed I)),(s +* EP),n) ) ; :: thesis: S_{1}[n + 1]

A10: Comput ((p +* (Directed I)),(s +* EP),(n + 1)) = Following ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n))) by EXTPRO_1:3

.= Exec ((CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n)))),(Comput ((p +* (Directed I)),(s +* EP),n))) ;

A11: Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Following ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n))) by EXTPRO_1:3

.= Exec ((CurInstr ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n)))),(Comput ((p +* (I ";" I)),(s +* EP),n))) ;

A12: n <= n + 1 by NAT_1:12;

assume A13: n + 1 <= k ; :: thesis: Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1))

IC (s +* EP) = 0 by A1, MEMSTR_0:47;

then A14: IC (s +* EP) in dom I by AFINSQ_1:65;

n <= k by A13, A12, XXREAL_0:2;

then Comput (p,s,n) = Comput ((p +* (I ";" I)),(s +* EP),n) by A1, A3, Th8, A2, A5, XXREAL_0:2;

then A15: IC (Comput ((p +* (I ";" I)),(s +* EP),n)) in dom I by AMISTD_1:21, A2, A14;

then A16: IC (Comput ((p +* (Directed I)),(s +* EP),n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;

A17: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n))) = (p +* (Directed I)) . (IC (Comput ((p +* (Directed I)),(s +* EP),n))) by PBOOLE:143

.= (Directed I) . (IC (Comput ((p +* (Directed I)),(s +* EP),n))) by A16, FUNCT_4:13 ;

CurInstr ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n))) = (p +* (I ";" I)) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by PBOOLE:143

.= (I ";" I) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by A8, A15, FUNCT_4:13

.= (Directed I) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by A7, A13, A16, A9, A12, GRFUNC_1:2, XXREAL_0:2 ;

hence Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1)) by A9, A13, A12, A17, A11, A10, XXREAL_0:2; :: thesis: verum

end;let n be Nat; :: thesis: ( S

A8: dom I c= dom (I ";" I) by SCMFSA6A:17;

assume A9: ( n <= k implies Comput ((p +* (I ";" I)),(s +* EP),n) = Comput ((p +* (Directed I)),(s +* EP),n) ) ; :: thesis: S

A10: Comput ((p +* (Directed I)),(s +* EP),(n + 1)) = Following ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n))) by EXTPRO_1:3

.= Exec ((CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n)))),(Comput ((p +* (Directed I)),(s +* EP),n))) ;

A11: Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Following ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n))) by EXTPRO_1:3

.= Exec ((CurInstr ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n)))),(Comput ((p +* (I ";" I)),(s +* EP),n))) ;

A12: n <= n + 1 by NAT_1:12;

assume A13: n + 1 <= k ; :: thesis: Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1))

IC (s +* EP) = 0 by A1, MEMSTR_0:47;

then A14: IC (s +* EP) in dom I by AFINSQ_1:65;

n <= k by A13, A12, XXREAL_0:2;

then Comput (p,s,n) = Comput ((p +* (I ";" I)),(s +* EP),n) by A1, A3, Th8, A2, A5, XXREAL_0:2;

then A15: IC (Comput ((p +* (I ";" I)),(s +* EP),n)) in dom I by AMISTD_1:21, A2, A14;

then A16: IC (Comput ((p +* (Directed I)),(s +* EP),n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;

A17: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),n))) = (p +* (Directed I)) . (IC (Comput ((p +* (Directed I)),(s +* EP),n))) by PBOOLE:143

.= (Directed I) . (IC (Comput ((p +* (Directed I)),(s +* EP),n))) by A16, FUNCT_4:13 ;

CurInstr ((p +* (I ";" I)),(Comput ((p +* (I ";" I)),(s +* EP),n))) = (p +* (I ";" I)) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by PBOOLE:143

.= (I ";" I) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by A8, A15, FUNCT_4:13

.= (Directed I) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by A7, A13, A16, A9, A12, GRFUNC_1:2, XXREAL_0:2 ;

hence Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1)) by A9, A13, A12, A17, A11, A10, XXREAL_0:2; :: thesis: verum

for n being Nat holds S

then Comput ((p +* (I ";" I)),(s +* EP),k) = Comput ((p +* (Directed I)),(s +* EP),k) ;

hence Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k) by A1, A3, A5, Th8, A2; :: thesis: verum

set lk = IC (Comput (p,s,k));

IC s = 0 by A1, MEMSTR_0:47;

then IC s in dom I by AFINSQ_1:65;

then A19: ( IC (Comput (p,s,k)) in dom I & dom I = dom (Directed I) ) by A2, AMISTD_1:21, FUNCT_4:99;

then A20: (Directed I) . (IC (Comput (p,s,k))) in rng (Directed I) by FUNCT_1:def 3;

assume k <= LifeSpan (p,s) ; :: thesis: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

then IC (Comput (p,s,k)) = IC (Comput ((p +* (Directed I)),(s +* EP),k)) by A4;

then A21: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* EP),k))) = (p +* (Directed I)) . (IC (Comput (p,s,k))) by PBOOLE:143

.= (Directed I) . (IC (Comput (p,s,k))) by A19, FUNCT_4:13 ;

assume CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) = halt SCM+FSA ; :: thesis: contradiction

hence contradiction by A21, A20, SCMFSA6A:1; :: thesis: verum