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
A3: Directed I c= p and
A4: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
P1: s = s +* {} by FUNCT_4:21;
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 A4, 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

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 A10: k <= LifeSpan ((p +* I),sISA0) ; :: thesis: Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)
A11: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A12: Directed I c= I ';' I by SCMFSA6A:16;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A13: dom I c= dom (I ';' I) by SCMFSA6A:17;
assume A14: ( n <= k implies Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n) ) ; :: thesis: S₁[n + 1]
A15: 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))) ;
A16: 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))) ;
A17: n <= n + 1 by NAT_1:12;
assume A18: 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 A18, A17, XXREAL_0:2;
then Comput ((p +* I),sISA0,n) = Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n) by A1, A5, Th18, A6, P1, A7, A10, XXREAL_0:2;
then A20: IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n)) in dom I by A5, Def1, A6;
then A21: IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) in dom (Directed I) by A18, A14, A17, FUNCT_4:99, XXREAL_0:2;
A22: 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 A21, 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 A13, A20, FUNCT_4:13
.= (Directed I) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n))) by A12, A18, A21, A14, A17, 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 A14, A18, A17, A22, A16, A15, XXREAL_0:2; :: thesis: verum

end;

( Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),0) = sISA0 +* EP & Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),0) = sISA0 +* EP ) by EXTPRO_1:2;
then A23: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A23, A11);
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, A10, Th18, A6, P1; :: thesis: verum

end;

then B25: Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))) ;
A26: 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, B25, FUNCT_4:99;
then A27: ((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 B25, FUNCT_4:13
.= goto (card I) by A8, A26, 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 B25, A27, PBOOLE:143 ;
then A28: ( ( 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 A3, FUNCT_4:98 ;
hence DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) by A7, A28, P1, SCMFSA6A:7; :: thesis: verum