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 & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I
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 & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I
set A = NAT ;
let I be InitClosed Program of SCM+FSA; ( p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s implies IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I )
assume that
A1:
p +* I halts_on s
and
A3:
Directed I c= p
and
A4:
Initialize ((intloc 0) .--> 1) c= s
; IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I
set sISA0 = s +* (Initialize ((intloc 0) .--> 1));
set pISA0 = p +* I;
set s1 = (s +* (Initialize ((intloc 0) .--> 1))) +* EP;
set p1 = (p +* I) +* (I ';' I);
P2:
s +* (Initialize ((intloc 0) .--> 1)) = s
by A4, FUNCT_4:104;
then P3:
(s +* (Initialize ((intloc 0) .--> 1))) +* EP = s
by FUNCT_4:22;
A5:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by A4, P2;
A6:
I c= p +* I
by FUNCT_4:26;
set IAt = Initialize I;
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:
I c= p +* I
by FUNCT_4:26;
A9:
IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) in dom I
by A5, Def1, A8;
set s2 = sISA0 +* EP;
set p2 = (p +* I) +* (Directed I);
XX:
sISA0 +* EP = sISA0
by FUNCT_4:22;
A10:
Directed I c= (p +* I) +* (Directed I)
by FUNCT_4:26;
now let k be
Element of
NAT ;
( 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)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),$1)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),$1)) );
assume A12:
k <= LifeSpan (
(p +* I),
sISA0)
;
NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k))A13:
for
n being
Element of
NAT st
S1[
n] holds
S1[
n + 1]
proof
let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )
assume A14:
(
n <= k implies
NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) )
;
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)),
((s +* (Initialize ((intloc 0) .--> 1))) +* EP),
(n + 1)) =
Following (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
by EXTPRO_1:4
.=
Exec (
(CurInstr (((p +* I) +* (I ';' I)),(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))),
(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
;
A17:
n <= n + 1
by NAT_1:12;
assume A18:
n + 1
<= k
;
NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),(n + 1))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1)))
then A19:
IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)) = IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n))
by A14, A17, COMPOS_1:230, XXREAL_0:2;
A20:
I c= p +* I
by FUNCT_4:26;
n <= k
by A18, A17, XXREAL_0:2;
then
n <= LifeSpan (
(p +* I),
sISA0)
by A12, XXREAL_0:2;
then
NPP (Comput ((p +* I),sISA0,n)) = NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))
by A1, A5, Th18, A6, P2, P3;
then
IC (Comput ((p +* I),sISA0,n)) = IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))
by COMPOS_1:230;
then A21:
IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)) in dom I
by A5, Def1, A20;
then A22:
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),n)) in dom (Directed I)
by A19, FUNCT_4:105;
A23:
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 A22, FUNCT_4:14
;
(
dom I c= dom (I ';' I) &
CurInstr (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
= ((p +* I) +* (I ';' I)) . (IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) )
by PBOOLE:158, SCMFSA6A:56;
then
(
Directed I c= I ';' I &
CurInstr (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
= (I ';' I) . (IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n))) )
by A21, FUNCT_4:14, SCMFSA6A:55;
then
CurInstr (
((p +* I) +* (I ';' I)),
(Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
= (Directed I) . (IC (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),n)))
by A19, A22, GRFUNC_1:8;
hence
NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),(n + 1))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(n + 1)))
by A14, A18, A17, A19, A23, A16, A15, AMISTD_2:def 20, XXREAL_0:2;
verum
end;
(
Comput (
((p +* I) +* (I ';' I)),
((s +* (Initialize ((intloc 0) .--> 1))) +* EP),
0)
= (s +* (Initialize ((intloc 0) .--> 1))) +* 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)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),0))
;
then A24:
S1[
0 ]
;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A24, A13);
then A25:
NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k))
;
NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (I ';' I)),((s +* (Initialize ((intloc 0) .--> 1))) +* EP),k))
by A1, A5, A12, Th18, A6, P2, P3;
hence
NPP (Comput ((p +* I),sISA0,k)) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),k))
by A25;
verum end;
then B26:
NPP (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))) = NPP (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0))))
;
then A26:
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;
A27: I . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0))))) =
(p +* I) . (IC (Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))))
by A9, A6, GRFUNC_1:8
.=
CurInstr ((p +* I),(Comput ((p +* I),sISA0,(LifeSpan ((p +* I),sISA0)))))
by PBOOLE:158
.=
halt SCM+FSA
by A1, P2, EXTPRO_1:def 14
;
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),(LifeSpan ((p +* I),sISA0)))) in dom I
by A9, B26, 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 A28: ((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 A26, A10, GRFUNC_1:8
.=
goto (card I)
by A9, A27, FUNCT_4:112
;
A29: 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 A26, A28, PBOOLE:158
;
set m = LifeSpan ((p +* I),sISA0);
dom (Directed I) = dom I
by FUNCT_4:105;
then A31: (p +* I) +* (Directed I) =
p +* (Directed I)
by FUNCT_4:78
.=
p
by A3, FUNCT_4:103, FUNCT_4:104
;
sISA0 +* EP =
sISA0
by FUNCT_4:22
.=
s
by A4, FUNCT_4:104
;
hence IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) =
IC (Comput (((p +* I) +* (Directed I)),(sISA0 +* EP),((LifeSpan ((p +* I),sISA0)) + 1)))
by A31, XX
.=
card I
by A29, SCMFSA_2:95
;
verum