let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of 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 Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of 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 Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies for k being Element of 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 that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: for k being Element of 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 )
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
A4: dom (P +* I) = NAT by PARTFUN1:def 2;
set s2 = Initialize s;
set s1 = Initialize s;
defpred S₁[ 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 ) );

A5: 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

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 A6: IC (Comput ((P +* I),(Initialize s),k)) in dom (Directed I) by A1, SCMFSA7B:def 6;
A7: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A3, PARTFUN1:def 6;
A8: 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 A7
.= (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A6, A8, GRFUNC_1:2 ;
then A9: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) in rng (Directed I) by A6, FUNCT_1:def 3;
assume CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A9, SCMFSA6A:1; :: thesis: verum

end;

now :: thesis: for k being Element of 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 )

A10: P +* I halts_on Initialize s by A2, SCMFSA7B:def 7;
A11: dom I c= dom (Directed I) by FUNCT_4:99;
let k be Element of 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 A12: ( 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 ) )
A13: 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))) ;
A14: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, SCMFSA7B:def 6;
A15: I c= P +* I by FUNCT_4:25;
A16: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A4, PARTFUN1:def 6
.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A14, A15, GRFUNC_1:2 ;
A17: k + 0 < k + 1 by XREAL_1:6;
A18: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A3, PARTFUN1:def 6;
A19: Directed I c= P +* (Directed I) by FUNCT_4:25;
assume A20: 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 A17, XXREAL_0:2;
then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A16, A10, EXTPRO_1:def 15;
then A21: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A16, FUNCT_4:105
.= (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A14, A11, A19, GRFUNC_1:2
.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by A12, A20, A17, A18, 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 A12, A20, A17, A21, A13, 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 A5; :: thesis: verum

end;

then A22: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;

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 ) )

assume 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 A5; :: thesis: verum

end;

then A23: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A22); :: thesis: verum