let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being InitClosed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being InitClosed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
set A = NAT ;
let I be InitClosed Program of SCM+FSA; :: thesis: ( p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s implies DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) )
assume that
A1: p +* I halts_on s and
A2: Directed I c= p and
A3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
A4: s = s +* {} ;
set sISA0 = s +* (Initialize ((intloc 0) .--> 1));
set pISA0 = p +* I;
set s2 = (s +* (Initialize ((intloc 0) .--> 1))) +* EP;
set p2 = (p +* I) +* (Directed I);
A5: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A6: I c= p +* I by FUNCT_4:25;
A7: s +* (Initialize ((intloc 0) .--> 1)) = s by A3, FUNCT_4:98;
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))));
A8: IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) in dom I by A5, Def1, A6;
set s2 = sISA0 +* EP;
set p2 = (p +* I) +* (Directed I);

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

set s1 = sISA0 +* EP;
set p1 = (p +* I) +* (I ";" I);
let k be Element of 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)),(sISA0 +* 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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

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

end;

A21: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A21, A10);
then Comput (((p +* I) +* (I ";" I)),(sISA0 +* 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, A5, A7, A9, Th10, A6, 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 A8, A6, GRFUNC_1:2
.= CurInstr ((p +* I),(Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) by PBOOLE:143
.= halt SCM+FSA by A1, A7, EXTPRO_1:def 15 ;
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) in dom (Directed I) by A8, 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, FUNCT_4:13
.= goto (card I) by A8, A23, FUNCT_4:106 ;
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 ;
then A25: ( ( for a being Int-Location holds (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),((LifeSpan ((p +* I),sISA0)) + 1))) . a = (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) . a ) & ( for f being FinSeq-Location holds (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),((LifeSpan ((p +* I),sISA0)) + 1))) . f = (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) . f ) ) by SCMFSA_2:69;
dom (Directed I) = dom I by FUNCT_4:99;
then (p +* I) +* (Directed I) = p +* (Directed I) by FUNCT_4:74
.= p by A2, FUNCT_4:98 ;
hence DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) by A7, A25, A4, SCMFSA_M:2; :: thesis: verum