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
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 really-closed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let I be really-closed Program of ; :: thesis: ( P +* I halts_on s & Directed I c= P 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 ; :: thesis: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
A3: I c= P +* I by FUNCT_4:25;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
IC s = 0 by MEMSTR_0:def 11;
then IC s in dom I by AFINSQ_1:65;
then A4: IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I by A3, AMISTD_1:21;
now :: thesis: for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput (P,s,k)
let k be Nat; :: thesis: ( k <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,k) = Comput (P,s,k) )
defpred S1[ Nat] means ( $1 <= k implies Comput (((P +* I) +* (I ";" I)),s,$1) = Comput (P,s,$1) );
assume A5: k <= LifeSpan ((P +* I),s) ; :: thesis: Comput ((P +* I),s,k) = Comput (P,s,k)
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
A7: Directed I c= I ";" I by SCMFSA6A:16;
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A8: dom I c= dom (I ";" I) by SCMFSA6A:17;
assume A9: ( n <= k implies Comput (((P +* I) +* (I ";" I)),s,n) = Comput (P,s,n) ) ; :: thesis: S1[n + 1]
A10: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s,n)))),(Comput (P,s,n))) ;
A11: Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Following (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n)))),(Comput (((P +* I) +* (I ";" I)),s,n))) ;
A12: n <= n + 1 by NAT_1:12;
assume A13: n + 1 <= k ; :: thesis: Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Comput (P,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 ";" I)),s,n) by Th10, A5, A3, A1, XXREAL_0:2;
then A15: IC (Comput (((P +* I) +* (I ";" I)),s,n)) in dom I by A3, AMISTD_1:21, A14;
then A16: IC (Comput (P,s,n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;
A17: dom P = NAT by PARTFUN1:def 2;
A18: CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A17, PARTFUN1:def 6
.= (Directed I) . (IC (Comput (P,s,n))) by A16, A2, GRFUNC_1:2 ;
A19: dom ((P +* I) +* (I ";" I)) = NAT by PARTFUN1:def 2;
CurInstr (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n))) = ((P +* I) +* (I ";" I)) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A19, PARTFUN1:def 6
.= (I ";" I) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A8, A15, FUNCT_4:13
.= (Directed I) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A7, A13, A16, A9, A12, GRFUNC_1:2, XXREAL_0:2 ;
hence Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Comput (P,s,(n + 1)) by A9, A13, A12, A18, A11, A10, XXREAL_0:2; :: thesis: verum
end;
A20: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A20, A6);
then Comput (((P +* I) +* (I ";" I)),s,k) = Comput (P,s,k) ;
hence Comput ((P +* I),s,k) = Comput (P,s,k) by A5, A1, Th10, FUNCT_4:25; :: thesis: verum
end;
then A21: Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput (P,s,(LifeSpan ((P +* I),s))) ;
A22: dom (P +* I) = NAT by PARTFUN1:def 2;
I c= P +* I by FUNCT_4:25;
then A23: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A4, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A22, PARTFUN1:def 6
.= halt SCM+FSA by A1, EXTPRO_1:def 15 ;
IC (Comput (P,s,(LifeSpan ((P +* I),s)))) in dom (Directed I) by A4, A21, FUNCT_4:99;
then A24: P . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A21, A2, GRFUNC_1:2
.= goto (card I) by A4, A23, FUNCT_4:106 ;
A25: dom P = NAT by PARTFUN1:def 2;
Comput (P,s,((LifeSpan ((P +* I),s)) + 1)) = Following (P,(Comput (P,s,(LifeSpan ((P +* I),s))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput (P,s,(LifeSpan ((P +* I),s))))) by A21, A24, A25, PARTFUN1:def 6 ;
then ( ( for a being Int-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . a = (Comput (P,s,(LifeSpan ((P +* I),s)))) . a ) & ( for f being FinSeq-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . f = (Comput (P,s,(LifeSpan ((P +* I),s)))) . f ) ) by SCMFSA_2:69;
hence DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by SCMFSA_M:2; :: thesis: verum