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

for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds

for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds

for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on s,P implies for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA ) )

assume A1: I is_halting_on s,P ; :: thesis: for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;

A3: dom (P +* I) = NAT by PARTFUN1:def 2;

set s2 = Initialize s;

set s1 = Initialize s;

defpred S_{1}[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (Directed I)),(Initialize s),$1) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),$1))) <> halt SCM+FSA ) );

IC (Initialize s) = 0 by MEMSTR_0:47;

then A4: IC (Initialize s) in dom I by AFINSQ_1:65;

A5: I c= P +* I by FUNCT_4:25;

_{1}[k] holds

S_{1}[k + 1]
;

_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A24, A23); :: thesis: verum

for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds

for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds

for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on s,P implies for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA ) )

assume A1: I is_halting_on s,P ; :: thesis: for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;

A3: dom (P +* I) = NAT by PARTFUN1:def 2;

set s2 = Initialize s;

set s1 = Initialize s;

defpred S

IC (Initialize s) = 0 by MEMSTR_0:47;

then A4: IC (Initialize s) in dom I by AFINSQ_1:65;

A5: I c= P +* I by FUNCT_4:25;

A6: now :: thesis: for k being Element of NAT st Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) holds

not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA

not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA

let k be Element of NAT ; :: thesis: ( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) implies not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA )

dom (Directed I) = dom I by FUNCT_4:99;

then A7: IC (Comput ((P +* I),(Initialize s),k)) in dom (Directed I) by AMISTD_1:21, A4, A5;

A8: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A2, PARTFUN1:def 6;

A9: Directed I c= P +* (Directed I) by FUNCT_4:25;

assume Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ; :: thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA

then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A8

.= (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A7, A9, GRFUNC_1:2 ;

then A10: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) in rng (Directed I) by A7, FUNCT_1:def 3;

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

hence contradiction by A10, SCMFSA6A:1; :: thesis: verum

end;dom (Directed I) = dom I by FUNCT_4:99;

then A7: IC (Comput ((P +* I),(Initialize s),k)) in dom (Directed I) by AMISTD_1:21, A4, A5;

A8: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A2, PARTFUN1:def 6;

A9: Directed I c= P +* (Directed I) by FUNCT_4:25;

assume Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ; :: thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA

then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A8

.= (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A7, A9, GRFUNC_1:2 ;

then A10: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) in rng (Directed I) by A7, FUNCT_1:def 3;

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

hence contradiction by A10, SCMFSA6A:1; :: thesis: verum

now :: thesis: for k being Nat st ( k <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ) & k + 1 <= LifeSpan ((P +* I),(Initialize s)) holds

( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA )

then A23:
for k being Nat st S( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA )

A11:
P +* I halts_on Initialize s
by A1, SCMFSA7B:def 7;

A12: dom I c= dom (Directed I) by FUNCT_4:99;

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

assume A13: ( k <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ) ; :: thesis: ( k + 1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA ) )

A14: Comput ((P +* (Directed I)),(Initialize s),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k)))),(Comput ((P +* (Directed I)),(Initialize s),k))) ;

A15: IC (Comput ((P +* I),(Initialize s),k)) in dom I by AMISTD_1:21, A4, A5;

A16: I c= P +* I by FUNCT_4:25;

A17: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A3, PARTFUN1:def 6

.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A15, A16, GRFUNC_1:2 ;

A18: k + 0 < k + 1 by XREAL_1:6;

A19: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A2, PARTFUN1:def 6;

A20: Directed I c= P +* (Directed I) by FUNCT_4:25;

assume A21: k + 1 <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA )

then k < LifeSpan ((P +* I),(Initialize s)) by A18, XXREAL_0:2;

then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A17, A11, EXTPRO_1:def 15;

then A22: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A17, FUNCT_4:105

.= (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A15, A12, A20, GRFUNC_1:2

.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by A13, A21, A18, A19, XXREAL_0:2 ;

Comput ((P +* I),(Initialize s),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k))) ;

hence Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) by A13, A21, A18, A22, A14, XXREAL_0:2; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA

hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA by A6; :: thesis: verum

end;A12: dom I c= dom (Directed I) by FUNCT_4:99;

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

assume A13: ( k <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ) ; :: thesis: ( k + 1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA ) )

A14: Comput ((P +* (Directed I)),(Initialize s),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k)))),(Comput ((P +* (Directed I)),(Initialize s),k))) ;

A15: IC (Comput ((P +* I),(Initialize s),k)) in dom I by AMISTD_1:21, A4, A5;

A16: I c= P +* I by FUNCT_4:25;

A17: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A3, PARTFUN1:def 6

.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A15, A16, GRFUNC_1:2 ;

A18: k + 0 < k + 1 by XREAL_1:6;

A19: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A2, PARTFUN1:def 6;

A20: Directed I c= P +* (Directed I) by FUNCT_4:25;

assume A21: k + 1 <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA )

then k < LifeSpan ((P +* I),(Initialize s)) by A18, XXREAL_0:2;

then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A17, A11, EXTPRO_1:def 15;

then A22: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A17, FUNCT_4:105

.= (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A15, A12, A20, GRFUNC_1:2

.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by A13, A21, A18, A19, XXREAL_0:2 ;

Comput ((P +* I),(Initialize s),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k))) ;

hence Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) by A13, A21, A18, A22, A14, XXREAL_0:2; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA

hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA by A6; :: thesis: verum

S

now :: thesis: ( 0 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA ) )

then A24:
Sassume
0 <= LifeSpan ((P +* I),(Initialize s))
; :: thesis: ( Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA )

thus Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) ; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA

hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA by A6; :: thesis: verum

end;thus Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) ; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA

hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA by A6; :: thesis: verum

thus for k being Nat holds S