let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds
for k being Element of 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 InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds
for k being Element of 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 InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= p implies for k being Element of 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);
A1: s +* EP = s by FUNCT_4:21;
assume A2: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I c= p or for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )
assume A3: I c= p ; :: thesis: for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA
then A4: p halts_on s by A2, Def2;

A5: now :: thesis: for k being Element of NAT st k <= LifeSpan (p,s) holds
Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)

set s1 = s +* EP;
set p1 = p +* (I ";" I);
A6: s = s +* EP by FUNCT_4:21;
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (p,s) implies Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k) )
defpred S₁[ Nat] means ( $1 <= k implies Comput ((p +* (I ";" I)),(s +* EP),$1) = Comput ((p +* (Directed I)),(s +* EP),$1) );
assume A7: k <= LifeSpan (p,s) ; :: thesis: Comput (p,s,k) = Comput ((p +* (Directed I)),(s +* EP),k)
A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A9: Directed I c= I ";" I by SCMFSA6A:16;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A10: dom I c= dom (I ";" I) by SCMFSA6A:17;
assume A11: ( n <= k implies Comput ((p +* (I ";" I)),(s +* EP),n) = Comput ((p +* (Directed I)),(s +* EP),n) ) ; :: thesis: S₁[n + 1]
A12: 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))) ;
A13: 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))) ;
A14: n <= n + 1 by NAT_1:12;
assume A15: n + 1 <= k ; :: thesis: Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1))
n <= k by A15, A14, XXREAL_0:2;
then Comput (p,s,n) = Comput ((p +* (I ";" I)),(s +* EP),n) by A2, A4, Th10, A3, A6, A7, XXREAL_0:2;
then A16: IC (Comput ((p +* (I ";" I)),(s +* EP),n)) in dom I by A2, Def1, A3;
then A17: IC (Comput ((p +* (Directed I)),(s +* EP),n)) in dom (Directed I) by A15, A11, A14, FUNCT_4:99, XXREAL_0:2;
A18: 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 A17, 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 A10, A16, FUNCT_4:13
.= (Directed I) . (IC (Comput ((p +* (I ";" I)),(s +* EP),n))) by A9, A15, A17, A11, A14, GRFUNC_1:2, XXREAL_0:2 ;
hence Comput ((p +* (I ";" I)),(s +* EP),(n + 1)) = Comput ((p +* (Directed I)),(s +* EP),(n + 1)) by A11, A15, A14, A18, A13, A12, XXREAL_0:2; :: thesis: verum

end;

A19: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A19, A8);
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 A2, A4, A7, Th10, A3, A6; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (p,s) implies CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA )
set lk = IC (Comput (p,s,k));
A20: ( IC (Comput (p,s,k)) in dom I & dom I = dom (Directed I) ) by A2, A3, Def1, FUNCT_4:99;
then A21: (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 A5;
then A22: 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 A20, FUNCT_4:13 ;
assume CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A22, A21, A1, SCMFSA6A:1; :: thesis: verum