let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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:22;
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:26;
A6: I c= p +* I by FUNCT_4:26;
set IAt = Initialize I;
A7: s +* (Initialize ((intloc 0) .--> 1)) = s by A4, FUNCT_4:104;
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 NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)) )
defpred S1[ Nat] means ( $1 <= k implies NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),$1)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),$1)) );
assume A10: k <= LifeSpan ((p +* I),sISA0) ; :: thesis: NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k))
A11: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
A12: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
A13: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A14: ( n <= k implies NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) ) ; :: thesis: S1[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:4
.= 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:4
.= 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: NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),(n + 1))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1)))
then A19: IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n)) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) by A14, A17, COMPOS_1:230, XXREAL_0:2;
n <= k by A18, A17, XXREAL_0:2;
then n <= LifeSpan ((p +* I),sISA0) by A10, XXREAL_0:2;
then NPP (Comput ((p +* I),sISA0,n)) = NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n)) by A1, A5, Th18, A6, P1, A7;
then IC (Comput ((p +* I),sISA0,n)) = IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n)) by COMPOS_1:230;
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 A19, FUNCT_4:105;
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:158
.= (Directed I) . (IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))) by A21, FUNCT_4:14 ;
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:158
.= (I ';' I) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n))) by A13, A20, FUNCT_4:14
.= (Directed I) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),n))) by A12, A19, A21, GRFUNC_1:8 ;
hence NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),(n + 1))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1))) by A14, A18, A17, A19, A22, A16, A15, AMISTD_2:def 20, 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:3;
then NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),0)) = NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),0)) ;
then A23: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A23, A11);
then A24: NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)) ;
NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (I ';' I)),(sISA0 +* EP),k)) by A1, A5, A7, A10, Th18, A6, P1;
hence NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)) by A24; :: thesis: verum
end;
then B25: NPP (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) ;
then A25: IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) by COMPOS_1:230;
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:8
.= CurInstr ((p +* I),(Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) by PBOOLE:158
.= halt SCM+FSA by A1, A7, EXTPRO_1:def 14 ;
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) in dom I by A8, B25, COMPOS_1:230;
then IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) in dom (Directed I) by FUNCT_4:105;
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 A25, FUNCT_4:14
.= goto (card I) by A8, A26, FUNCT_4:112 ;
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:4
.= Exec ((goto (card I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))))) by A25, A27, PBOOLE:158 ;
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:95;
dom (Directed I) = dom I by FUNCT_4:105;
then (p +* I) +* (Directed I) = p +* (Directed I) by FUNCT_4:78
.= p by A3, FUNCT_4:103, FUNCT_4:104 ;
hence DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) by A7, A28, P1, SCMFSA6A:38; :: thesis: verum