let s be State of SCM+FSA; 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
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; 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
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
set A = NAT ;
let I be really-closed Program of SCM+FSA; ( 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
; DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))
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);
A4:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:25;
A5:
I c= p +* I
by FUNCT_4:25;
A6:
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))));
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, A5;
set s2 = sISA0 +* EP;
set p2 = (p +* I) +* (Directed I);
now for k being 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
Nat;
( k <= LifeSpan ((p +* I),sISA0) implies Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k) )defpred S1[
Nat]
means ( $1
<= k implies
Comput (
((p +* I) +* (I ";" I)),
(sISA0 +* EP),$1)
= Comput (
((p +* I) +* (Directed I)),
(sISA0 +* EP),$1) );
assume A8:
k <= LifeSpan (
(p +* I),
sISA0)
;
Comput ((p +* I),sISA0,k) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k)A9:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
A10:
Directed I c= I ";" I
by SCMFSA6A:16;
let n be
Nat;
( S1[n] implies S1[n + 1] )
A11:
dom I c= dom (I ";" I)
by SCMFSA6A:17;
assume A12:
(
n <= k implies
Comput (
((p +* I) +* (I ";" I)),
(sISA0 +* EP),
n)
= Comput (
((p +* I) +* (Directed I)),
(sISA0 +* EP),
n) )
;
S1[n + 1]
A13:
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)))
;
A14:
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)))
;
A15:
n <= n + 1
by NAT_1:12;
assume A16:
n + 1
<= k
;
Comput (((p +* I) +* (I ";" I)),(sISA0 +* EP),(n + 1)) = Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1))
IC (sISA0 +* EP) = 0
by MEMSTR_0:def 11;
then A17:
IC (sISA0 +* EP) in dom I
by AFINSQ_1:65;
n <= k
by A16, A15, XXREAL_0:2;
then
Comput (
(p +* I),
sISA0,
n)
= Comput (
((p +* I) +* (I ";" I)),
(sISA0 +* EP),
n)
by A1, A4, Th8, A5, A6, A8, XXREAL_0:2;
then A18:
IC (Comput (((p +* I) +* (I ";" I)),(sISA0 +* EP),n)) in dom I
by AMISTD_1:21, A5, A17;
then A19:
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) in dom (Directed I)
by A16, A12, A15, 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 A11, A18, FUNCT_4:13
.=
(Directed I) . (IC (Comput (((p +* I) +* (I ";" I)),(sISA0 +* EP),n)))
by A10, A16, A19, A12, A15, 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 A12, A16, A15, A20, A14, A13, XXREAL_0:2;
verum
end; A21:
S1[
0 ]
;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A21, A9);
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, A4, A6, A8, Th8, A5;
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, A6, 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, FUNCT_4:13
.=
goto (card I)
by A7, 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 A6, A25, SCMFSA_M:2; verum