let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting Program of SCM+FSA st I c= P & Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting Program of SCM+FSA st I c= P & Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
set A = NAT ;
let I be parahalting Program of SCM+FSA; :: thesis: ( I c= P & Initialized I c= s implies for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA )
set s2 = s +* (Directed I);
set m = LifeSpan (P,s);
assume that
A1: I c= P and
A2: Initialized I c= s ; :: thesis: for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
A3: Initialize I c= s by Th8, A2;
A4: ProgramPart (Initialize I) = I by COMPOS_1:144;
Initialize I is halting by Def3;
then A5: P halts_on s by EXTPRO_1:def 10, A1, A3, A4;
set s1 = s +* (I ';' I);

A6: now

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (P,s) implies Comput (P,s,k), Comput ((P +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT )
defpred S₁[ Nat] means ( $1 <= k implies Comput ((P +* (I ';' I)),(s +* (I ';' I)),$1), Comput ((P +* (Directed I)),(s +* (Directed I)),$1) equal_outside NAT );
assume A7: k <= LifeSpan (P,s) ; :: thesis: Comput (P,s,k), Comput ((P +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT
A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A9: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A10: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A11: ( n <= k implies Comput ((P +* (I ';' I)),(s +* (I ';' I)),n), Comput ((P +* (Directed I)),(s +* (Directed I)),n) equal_outside NAT ) ; :: thesis: S₁[n + 1]
A12: Comput ((P +* (Directed I)),(s +* (Directed I)),(n + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),n)))),(Comput ((P +* (Directed I)),(s +* (Directed I)),n))) ;
A13: Comput ((P +* (I ';' I)),(s +* (I ';' I)),(n + 1)) = Following ((P +* (I ';' I)),(Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (I ';' I)),(Comput ((P +* (I ';' I)),(s +* (I ';' I)),n)))),(Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) ;
A14: n <= n + 1 by NAT_1:12;
assume A15: n + 1 <= k ; :: thesis: Comput ((P +* (I ';' I)),(s +* (I ';' I)),(n + 1)), Comput ((P +* (Directed I)),(s +* (Directed I)),(n + 1)) equal_outside NAT
then A16: IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n)) = IC (Comput ((P +* (Directed I)),(s +* (Directed I)),n)) by A11, A14, COMPOS_1:24, XXREAL_0:2;
n <= k by A15, A14, XXREAL_0:2;
then n <= LifeSpan (P,s) by A7, XXREAL_0:2;
then Comput (P,s,n), Comput ((P +* (I ';' I)),(s +* (I ';' I)),n) equal_outside NAT by A5, A3, A1, Th36;
then IC (Comput (P,s,n)) = IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n)) by COMPOS_1:24;
then A17: IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n)) in dom I by A3, Def2, A1;
then A18: IC (Comput ((P +* (Directed I)),(s +* (Directed I)),n)) in dom (Directed I) by A16, FUNCT_4:105;
dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
then A19: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Directed I)),n))) by PARTFUN1:def 8
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(s +* (Directed I)),n))) by A18, FUNCT_4:14 ;
dom (P +* (I ';' I)) = NAT by PARTFUN1:def 4;
then CurInstr ((P +* (I ';' I)),(Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) = (P +* (I ';' I)) . (IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) by PARTFUN1:def 8
.= (I ';' I) . (IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) by A10, A17, FUNCT_4:14
.= (Directed I) . (IC (Comput ((P +* (I ';' I)),(s +* (I ';' I)),n))) by A9, A16, A18, GRFUNC_1:8 ;
hence Comput ((P +* (I ';' I)),(s +* (I ';' I)),(n + 1)), Comput ((P +* (Directed I)),(s +* (Directed I)),(n + 1)) equal_outside NAT by A11, A15, A14, A16, A19, A13, A12, AMISTD_2:def 20, XXREAL_0:2; :: thesis: verum

end;

( Comput ((P +* (I ';' I)),(s +* (I ';' I)),0) = s +* (I ';' I) & Comput ((P +* (Directed I)),(s +* (Directed I)),0) = s +* (Directed I) ) by EXTPRO_1:3;
then Comput ((P +* (Directed I)),(s +* (Directed I)),0), Comput ((P +* (I ';' I)),(s +* (I ';' I)),0) equal_outside NAT by FUNCT_7:107, FUNCT_7:133;
then A20: S₁[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A20, A8);
then A21: Comput ((P +* (I ';' I)),(s +* (I ';' I)),k), Comput ((P +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT ;
Comput (P,s,k), Comput ((P +* (I ';' I)),(s +* (I ';' I)),k) equal_outside NAT by A5, A3, A7, Th36, A1;
hence Comput (P,s,k), Comput ((P +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT by A21, FUNCT_7:29; :: thesis: verum

end;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (P,s) implies not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) = halt SCM+FSA )
set lk = IC (Comput (P,s,k));
A22: dom I = dom (Directed I) by FUNCT_4:105;
IC (Comput (P,s,k)) in dom I by A3, Def2, A1;
then A23: (Directed I) . (IC (Comput (P,s,k))) in rng (Directed I) by FUNCT_1:def 5, A22;
A24: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
assume k <= LifeSpan (P,s) ; :: thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) = halt SCM+FSA
then IC (Comput (P,s,k)) = IC (Comput ((P +* (Directed I)),(s +* (Directed I)),k)) by A6, COMPOS_1:24;
then A25: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) = (P +* (Directed I)) . (IC (Comput (P,s,k))) by A24, PARTFUN1:def 8
.= (Directed I) . (IC (Comput (P,s,k))) by A22, FUNCT_4:14, A3, Def2, A1 ;
assume CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Directed I)),k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A25, A23, SCMFSA6A:18; :: thesis: verum

end;