let s be State of SCM+FSA; :: thesis:
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let I be Program of SCM+FSA; :: thesis:
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis:
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
A4: dom (P +* I) = NAT by PARTFUN1:def 4;
A5: ProgramPart I = I by RELAT_1:209;
set s2 = s +* (Initialize (Directed I));
set s1 = s +* (Initialize I);
defpred S₁[ Nat] means ( $1 <= LifeSpan ((P +* I),(s +* (Initialize I))) implies ( Comput ((P +* I),(s +* (Initialize I)),$1), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),$1) equal_outside NAT & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),$1))) <> halt SCM+FSA ) );

A6: now

let k be Element of NAT ; :: thesis:
dom (Directed I) = dom I by FUNCT_4:105;
then A7: IC (Comput ((P +* I),(s +* (Initialize I)),k)) in dom (Directed I) by A1, SCMFSA7B:def 7, A5;
A8: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A3, PARTFUN1:def 8;
A9: Directed I c= P +* (Directed I) by FUNCT_4:26;
assume Comput ((P +* I),(s +* (Initialize I)),k), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k) equal_outside NAT ; :: thesis:
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A8, COMPOS_1:24
.= (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A7, GRFUNC_1:8, A9 ;
then A10: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) in rng (Directed I) by A7, FUNCT_1:def 5;
assume CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = halt SCM+FSA ; :: thesis:
hence contradiction by A10, SCMFSA6A:18; :: thesis:

end;

A11: P +* I halts_on s +* (Initialize I) by A2, SCMFSA7B:def 8, A5;
A12: dom I c= dom (Directed I) by FUNCT_4:105;
let k be Element of NAT ; :: thesis:
assume A13: ( k <= LifeSpan ((P +* I),(s +* (Initialize I))) implies Comput ((P +* I),(s +* (Initialize I)),k), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k) equal_outside NAT ) ; :: thesis:
A14: Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)))),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) ;
A15: IC (Comput ((P +* I),(s +* (Initialize I)),k)) in dom I by A1, SCMFSA7B:def 7, A5;
A16: I c= P +* I by FUNCT_4:26;
A17: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),k))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A4, PARTFUN1:def 8
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A15, GRFUNC_1:8, A16 ;
A18: k + 0 < k + 1 by XREAL_1:8;
A19: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A3, PARTFUN1:def 8;
A20: Directed I c= P +* (Directed I) by FUNCT_4:26;
assume A21: k + 1 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
then k < LifeSpan ((P +* I),(s +* (Initialize I))) by A18, XXREAL_0:2;
then I . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) <> halt SCM+FSA by A17, A11, EXTPRO_1:def 14;
then A22: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),k))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A17, FUNCT_4:111
.= (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),k))) by A15, A12, GRFUNC_1:8, A20
.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A13, A21, A18, A19, COMPOS_1:24, XXREAL_0:2 ;
Comput ((P +* I),(s +* (Initialize I)),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),k)))),(Comput ((P +* I),(s +* (Initialize I)),k))) ;
hence Comput ((P +* I),(s +* (Initialize I)),(k + 1)), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(k + 1)) equal_outside NAT by A13, A21, A18, A22, A14, AMISTD_2:def 20, XXREAL_0:2; :: thesis:
hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(k + 1)))) <> halt SCM+FSA by A6; :: thesis:

end;

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

assume 0 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
A24: ( Comput ((P +* I),(s +* (Initialize I)),0) = s +* (Initialize I) & Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),0) = s +* (Initialize (Directed I)) ) by EXTPRO_1:3;
hence Comput ((P +* I),(s +* (Initialize I)),0), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),0) equal_outside NAT by Th14; :: thesis:
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),0))) <> halt SCM+FSA by A6, A24, Th14; :: thesis:

end;

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