let s be 0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let I be really-closed Program of ; :: thesis: ( P +* I halts_on s & Directed I c= P implies IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I )
assume that
A1: P +* I halts_on s and
A2: Directed I c= P ; :: thesis: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
A3: I c= P +* I by FUNCT_4:25;
set s2 = s;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
A4: I c= P +* I by FUNCT_4:25;
IC s = 0 by MEMSTR_0:def 11;
then IC s in dom I by AFINSQ_1:65;
then A5: IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I by A4, AMISTD_1:21;
set s1 = s;
A6: P +* (I ";" I) = P +* (I +* (I ";" I)) by SCMFSA6A:18
.= (P +* I) +* (I ";" I) by FUNCT_4:14 ;

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

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: ( n <= k implies Comput ((P +* (I ";" I)),s,n) = Comput ((P +* (Directed I)),s,n) ) ; :: thesis: S₁[n + 1]
A10: 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))) ;
A11: Comput ((P +* (I ";" I)),s,(n + 1)) = Following ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n)))),(Comput ((P +* (I ";" I)),s,n))) ;
A12: n <= n + 1 by NAT_1:12;
assume A13: n + 1 <= k ; :: thesis: Comput ((P +* (I ";" I)),s,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1))
IC s = 0 by MEMSTR_0:def 11;
then A14: IC s in dom I by AFINSQ_1:65;
n <= k by A13, A12, XXREAL_0:2;
then Comput ((P +* I),s,n) = Comput ((P +* (I ";" I)),s,n) by A3, Th10, A6, A1, A7, XXREAL_0:2;
then IC (Comput ((P +* (I ";" I)),s,n)) in dom I by A3, AMISTD_1:21, A14;
then A15: IC (Comput ((P +* (Directed I)),s,n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;
dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
then A16: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),s,n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),s,n))) by PARTFUN1:def 6;
A17: dom (P +* (I ";" I)) = NAT by PARTFUN1:def 2;
Directed I c= P +* (Directed I) by FUNCT_4:25;
then A18: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) = (Directed I) . (IC (Comput ((P +* (Directed I)),s,n))) by A15, A16, GRFUNC_1:2;
A19: ( dom I c= dom (I ";" I) & CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n))) = (P +* (I ";" I)) . (IC (Comput ((P +* (I ";" I)),s,n))) ) by A17, PARTFUN1:def 6, SCMFSA6A:17;
A20: Directed I c= I ";" I by SCMFSA6A:16;
I ";" I c= P +* (I ";" I) by FUNCT_4:25;
then Directed I c= P +* (I ";" I) by A20, XBOOLE_1:1;
hence Comput ((P +* (I ";" I)),s,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1)) by A9, A13, A12, A18, A11, A10, A15, A19, GRFUNC_1:2, XXREAL_0:2; :: thesis: verum

end;

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

end;

then A22: Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))) ;
A23: dom (P +* I) = NAT by PARTFUN1:def 2;
I c= P +* I by FUNCT_4:25;
then A24: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A5, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A23, PARTFUN1:def 6
.= halt SCM+FSA by A1, EXTPRO_1:def 15 ;
IC (Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))) in dom (Directed I) by A5, A22, FUNCT_4:99;
then A25: (P +* (Directed I)) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A22, FUNCT_4:13
.= goto (card I) by A5, A24, FUNCT_4:106 ;
A26: P +* (Directed I) = P by A2, FUNCT_4:98;
A27: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
Comput ((P +* (Directed I)),s,((LifeSpan ((P +* I),s)) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))))) by A27, A22, A25, PARTFUN1:def 6 ;
hence IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by A26, SCMFSA_2:69; :: thesis: verum