let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being 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 really-closed parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
let I be really-closed parahalting Program of ; :: thesis: ( I c= P & Initialize ((intloc 0) .--> 1) c= s implies for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA )
set m = LifeSpan (P,s);
assume that
A1: I c= P and
A2: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
A3: Start-At (0,SCM+FSA) c= s by A2, MEMSTR_0:50;
then s is 0 -started by MEMSTR_0:29;
then A4: P halts_on s by A1, AMISTD_1:def 11;
reconsider s1 = s as 0 -started State of SCM+FSA by A3, MEMSTR_0:29;
IC s1 = 0 by MEMSTR_0:def 11;
then A5: IC s in dom I by AFINSQ_1:65;

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

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

proof

A9: Directed I c= I ";" I by SCMFSA6A:16;
let n be 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)),s1,n) = Comput ((P +* (Directed I)),s,n) ) ; :: thesis: S₁[n + 1]
A12: Comput ((P +* (Directed I)),s,(n + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n)))),(Comput ((P +* (Directed I)),s,n))) ;
A13: Comput ((P +* (I ";" I)),s1,(n + 1)) = Following ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n)))),(Comput ((P +* (I ";" I)),s1,n))) ;
A14: n <= n + 1 by NAT_1:12;
assume A15: n + 1 <= k ; :: thesis: Comput ((P +* (I ";" I)),s1,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1))
n <= k by A15, A14, XXREAL_0:2;
then Comput (P,s,n) = Comput ((P +* (I ";" I)),s1,n) by A4, A1, Th10, A7, XXREAL_0:2;
then A16: IC (Comput ((P +* (I ";" I)),s1,n)) in dom I by A1, AMISTD_1:21, A5;
then A17: IC (Comput ((P +* (Directed I)),s,n)) in dom (Directed I) by A15, A11, A14, FUNCT_4:99, XXREAL_0:2;
dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
then A18: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),s,n))) by PARTFUN1:def 6
.= (Directed I) . (IC (Comput ((P +* (Directed I)),s,n))) by A17, FUNCT_4:13 ;
dom (P +* (I ";" I)) = NAT by PARTFUN1:def 2;
then CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n))) = (P +* (I ";" I)) . (IC (Comput ((P +* (I ";" I)),s1,n))) by PARTFUN1:def 6
.= (I ";" I) . (IC (Comput ((P +* (I ";" I)),s1,n))) by A10, A16, FUNCT_4:13
.= (Directed I) . (IC (Comput ((P +* (I ";" I)),s1,n))) by A9, A15, A11, A14, A17, GRFUNC_1:2, XXREAL_0:2 ;
hence Comput ((P +* (I ";" I)),s1,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1)) by A11, A15, A14, A18, A13, A12, XXREAL_0:2; :: thesis: verum

end;

A19: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A8);
then Comput ((P +* (I ";" I)),s1,k) = Comput ((P +* (Directed I)),s,k) ;
hence Comput (P,s,k) = Comput ((P +* (Directed I)),s,k) by A4, A7, Th10, A1; :: thesis: verum

end;

let k be 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: dom I = dom (Directed I) by FUNCT_4:99;
A21: IC (Comput (P,s1,k)) in dom I by A1, AMISTD_1:21, A5;
then A22: (Directed I) . (IC (Comput (P,s,k))) in rng (Directed I) by A20, FUNCT_1:def 3;
A23: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
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,k)) by A6;
then A24: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) = (P +* (Directed I)) . (IC (Comput (P,s,k))) by A23, PARTFUN1:def 6
.= (Directed I) . (IC (Comput (P,s,k))) by A20, A21, FUNCT_4:13 ;
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA by A24, A22, SCMFSA6A:1; :: thesis: verum