let s be State of SCM+FSA; 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 +* I & Directed I c= s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)))
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for I being InitClosed Program of SCM+FSA st p +* I halts_on s +* I & Directed I c= s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)))
set A = NAT ;
let I be InitClosed Program of SCM+FSA; ( p +* I halts_on s +* I & Directed I c= s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s implies DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) )
assume that
A1:
p +* I halts_on s +* I
and
A2:
Directed I c= s
and
A3:
Directed I c= p
and
A4:
Initialize ((intloc 0) .--> 1) c= s
; DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)))
set sISA0 = s +* (I +* (Initialize ((intloc 0) .--> 1)));
set pISA0 = p +* I;
A5:
Initialized I c= s +* (I +* (Initialize ((intloc 0) .--> 1)))
by A4, Th20;
A6:
I c= p +* I
by FUNCT_4:26;
set IAt = Initialize I;
A7:
s +* (I +* (Initialize ((intloc 0) .--> 1))) = s +* I
by A4, Th20;
reconsider sISA0 = s +* (I +* (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 +* (Directed I);
set p2 = (p +* I) +* (Directed I);
A9:
now set s1 =
sISA0 +* (I ';' I);
set p1 =
(p +* I) +* (I ';' I);
let k be
Element of
NAT ;
( k <= LifeSpan ((p +* I),sISA0) implies Comput ((p +* I),sISA0,k), Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),k) equal_outside NAT )defpred S1[
Nat]
means ( $1
<= k implies
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),$1),
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),$1)
equal_outside NAT );
assume A10:
k <= LifeSpan (
(p +* I),
sISA0)
;
Comput ((p +* I),sISA0,k), Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),k) equal_outside NAT 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 ;
( S1[n] implies S1[n + 1] )
A13:
dom I c= dom (I ';' I)
by SCMFSA6A:56;
assume A14:
(
n <= k implies
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
n),
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
n)
equal_outside NAT )
;
S1[n + 1]
A15:
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
(n + 1)) =
Following (
((p +* I) +* (Directed I)),
(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)))
by EXTPRO_1:4
.=
Exec (
(CurInstr (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)))),
(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)))
;
A16:
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
(n + 1)) =
Following (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))
by EXTPRO_1:4
.=
Exec (
(CurInstr (((p +* I) +* (I ';' I)),(Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))),
(Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))
;
A17:
n <= n + 1
by NAT_1:12;
assume A18:
n + 1
<= k
;
Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),(n + 1)), Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(n + 1)) equal_outside NAT
then A19:
IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n))
by A14, A17, COMPOS_1:24, XXREAL_0:2;
n <= k
by A18, A17, XXREAL_0:2;
then
n <= LifeSpan (
(p +* I),
sISA0)
by A10, XXREAL_0:2;
then
IC (Comput ((p +* I),sISA0,n)) = IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n))
by A1, A5, A7, Th18, COMPOS_1:24, A6;
then A20:
IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)) in dom I
by A5, Def1, A6;
then A21:
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)) in dom (Directed I)
by A19, FUNCT_4:105;
A22:
CurInstr (
((p +* I) +* (Directed I)),
(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n))) =
((p +* I) +* (Directed I)) . (IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)))
by PBOOLE:158
.=
(Directed I) . (IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),n)))
by A21, FUNCT_4:14
;
CurInstr (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n))) =
((p +* I) +* (I ';' I)) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))
by PBOOLE:158
.=
(I ';' I) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))
by A13, A20, FUNCT_4:14
.=
(Directed I) . (IC (Comput (((p +* I) +* (I ';' I)),(sISA0 +* (I ';' I)),n)))
by A12, A19, A21, GRFUNC_1:8
;
hence
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
(n + 1)),
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
(n + 1))
equal_outside NAT
by A14, A18, A17, A19, A22, A16, A15, AMISTD_2:def 20, XXREAL_0:2;
verum
end;
(
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
0)
= sISA0 +* (I ';' I) &
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
0)
= sISA0 +* (Directed I) )
by EXTPRO_1:3;
then
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
0),
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
0)
equal_outside NAT
by FUNCT_7:107, FUNCT_7:133;
then A23:
S1[
0 ]
by FUNCT_7:28;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A23, A11);
then A24:
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
k),
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
k)
equal_outside NAT
;
Comput (
(p +* I),
sISA0,
k),
Comput (
((p +* I) +* (I ';' I)),
(sISA0 +* (I ';' I)),
k)
equal_outside NAT
by A1, A5, A7, A10, Th18, A6;
hence
Comput (
(p +* I),
sISA0,
k),
Comput (
((p +* I) +* (Directed I)),
(sISA0 +* (Directed I)),
k)
equal_outside NAT
by A24, FUNCT_7:29;
verum end;
then A25:
IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(LifeSpan ((p +* I),sISA0))))
by COMPOS_1:24;
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 +* (Directed I)),(LifeSpan ((p +* I),sISA0)))) in dom I
by A9, A8, COMPOS_1:24;
then
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(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 +* (Directed I)),((LifeSpan ((p +* I),sISA0)) + 1)) =
Following (((p +* I) +* (Directed I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(LifeSpan ((p +* I),sISA0)))))
by EXTPRO_1:4
.=
Exec ((goto (card I)),(Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(LifeSpan ((p +* I),sISA0)))))
by A25, A27, PBOOLE:158
;
then A28:
( ( for a being Int-Location holds (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),((LifeSpan ((p +* I),sISA0)) + 1))) . a = (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(LifeSpan ((p +* I),sISA0)))) . a ) & ( for f being FinSeq-Location holds (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),((LifeSpan ((p +* I),sISA0)) + 1))) . f = (Comput (((p +* I) +* (Directed I)),(sISA0 +* (Directed I)),(LifeSpan ((p +* I),sISA0)))) . f ) )
by SCMFSA_2:95;
dom (Directed I) = dom I
by FUNCT_4:105;
then A29: (p +* I) +* (Directed I) =
p +* (Directed I)
by FUNCT_4:78
.=
p
by A3, FUNCT_4:79
;
sISA0 +* (Directed I) =
s +* (Directed I)
by A4, Th20
.=
s
by A2, FUNCT_4:79
;
hence
DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)))
by A7, A28, SCMFSA6A:38, A29; verum