let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s 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 SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I
set A = NAT ;
let I be really-closed Program of SCM+FSA; :: thesis: ( p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s 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 and
A3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I
set sISA0 = s +* (Initialize ((intloc 0) .--> 1));
set pISA0 = p +* I;
set s1 = (s +* (Initialize ((intloc 0) .--> 1))) +* EP;
set p1 = (p +* I) +* (I ";" I);
A4: s +* (Initialize ((intloc 0) .--> 1)) = s by A3, FUNCT_4:98;
A5: I c= p +* I by FUNCT_4:25;
reconsider sISA0 = s +* (Initialize ((intloc 0) .--> 1)) as State of SCM+FSA ;
set m = LifeSpan ((p +* I),sISA0);
set l1 = IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))));
A6: I c= p +* I by FUNCT_4:25;
IC sISA0 = 0 by MEMSTR_0:def 11;
then IC sISA0 in dom I by AFINSQ_1:65;
then A7: IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) in dom I by AMISTD_1:21, A6;
set s2 = sISA0 +* EP;
set p2 = (p +* I) +* (Directed I);
A8: Directed I c= (p +* I) +* (Directed I) by FUNCT_4:25;

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

let k be Nat; :: thesis: ( k <= LifeSpan ((p +* I),sISA0) implies Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k) )
defpred S₁[ Nat] means ( $1 <= k implies Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),$1) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),$1) );
assume A9: k <= LifeSpan ((p +* I),sISA0) ; :: thesis: Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: ( n <= k implies Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n) ) ; :: thesis: S₁[n + 1]
A12: Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1)) = Following (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) by EXTPRO_1:3
.= Exec ((CurInstr (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)))),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) ;
A13: Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),(n + 1)) = Following (((p +* I) +* (I ";" I)),(Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) by EXTPRO_1:3
.= Exec ((CurInstr (((p +* I) +* (I ";" I)),(Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))),(Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) ;
A14: n <= n + 1 by NAT_1:12;
assume A15: n + 1 <= k ; :: thesis: Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),(n + 1)) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1))
A16: I c= p +* I by FUNCT_4:25;
IC ((s +* (Initialize ((intloc 0) .--> 1))) +* EP) = 0 by MEMSTR_0:def 11;
then A17: IC ((s +* (Initialize ((intloc 0) .--> 1))) +* EP) in dom I by AFINSQ_1:65;
n <= k by A15, A14, XXREAL_0:2;
then IC (Comput ((p +* I),sISA0,n)) = IC (Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)) by A1, A3, Th8, A5, A4, A9, XXREAL_0:2;
then A18: IC (Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)) in dom I by AMISTD_1:21, A16, A17;
then A19: IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) in dom (Directed I) by A15, A11, A14, FUNCT_4:99, XXREAL_0:2;
A20: CurInstr (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) = ((p +* I) +* (Directed I)) . (IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) by PBOOLE:143
.= (Directed I) . (IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) by A19, FUNCT_4:13 ;
( dom I c= dom (I ";" I) & CurInstr (((p +* I) +* (I ";" I)),(Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) = ((p +* I) +* (I ";" I)) . (IC (Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) ) by PBOOLE:143, SCMFSA6A:17;
then ( Directed I c= I ";" I & CurInstr (((p +* I) +* (I ";" I)),(Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) = (I ";" I) . (IC (Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) ) by A18, FUNCT_4:13, SCMFSA6A:16;
hence Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),(n + 1)) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1)) by A11, A15, A14, A20, A13, A12, 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, A10);
then Comput (((p +* I) +* (I ";" I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k) ;
hence Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k) by A1, A3, A9, Th8, A5, A4; :: thesis: verum

end;

then A22: Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))) ;
A23: I . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) = (p +* I) . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) by A7, A5, GRFUNC_1:2
.= CurInstr ((p +* I),(Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) by PBOOLE:143
.= halt SCM+FSA by A1, A4, EXTPRO_1:def 15 ;
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) in dom (Directed I) by A7, A22, FUNCT_4:99;
then A24: ((p +* I) +* (Directed I)) . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) = (Directed I) . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) by A22, A8, GRFUNC_1:2
.= goto (card I) by A7, A23, FUNCT_4:106 ;
A25: Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),((LifeSpan ((p +* I),sISA0)) + 1)) = Following (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))))) by A22, A24, PBOOLE:143 ;
set m = LifeSpan ((p +* I),sISA0);
dom (Directed I) = dom I by FUNCT_4:99;
then A26: (p +* I) +* (Directed I) = p +* (Directed I) by FUNCT_4:74
.= p by A2, FUNCT_4:98 ;
sISA0 +* EP = sISA0
.= s by A3, FUNCT_4:98 ;
hence IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),((LifeSpan ((p +* I),sISA0)) + 1))) by A26
.= card I by A25, SCMFSA_2:69 ;
:: thesis: verum