thus
STC N is IC-good
STC N is Exec-preserving proof
let I be
Instruction of
(STC N);
AMISTD_2:def 19 I is IC-good let k be
natural number ;
AMISTD_2:def 18 for s1 being State of (STC N) holds (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))let s1 be
State of
(STC N);
(IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
set s2 =
IncrIC s1,
k;
{(IC (STC N))} = dom ((IC (STC N)) .--> ((IC s1) + k))
by FUNCOP_1:19;
then
IC (STC N) in dom ((IC (STC N)) .--> ((IC s1) + k))
by TARSKI:def 1;
then A2:
IC (IncrIC s1,k) =
((IC (STC N)) .--> ((IC s1) + k)) . (IC (STC N))
by FUNCT_4:14
.=
(IC s1) + k
by FUNCOP_1:87
;
end;
let I be Instruction of (STC N); AMISTD_2:def 21 I is Exec-preserving
per cases
( InsCode I = 1 or InsCode I = 0 )
by AMISTD_1:22;
suppose A6:
InsCode I = 1
;
I is Exec-preserving
the
Instructions of
(STC N) = {[0 ,0 ,0 ],[1,0 ,0 ]}
by AMISTD_1:def 11;
then A7:
(
I = [0 ,0 ,0 ] or
I = [1,0 ,0 ] )
by TARSKI:def 2;
let s1,
s2 be
State of
(STC N);
AMISTD_2:def 20 ( s1,s2 equal_outside NAT implies Exec I,s1, Exec I,s2 equal_outside NAT )assume A8:
s1,
s2 equal_outside NAT
;
Exec I,s1, Exec I,s2 equal_outside NAT consider f being
Function of
(product the Object-Kind of (STC N)),
(product the Object-Kind of (STC N)) such that A9:
for
s being
Element of
product the
Object-Kind of
(STC N) holds
f . s = s +* (NAT .--> (succ (s . NAT )))
and A10:
the
Execution of
(STC N) = ([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N))))
by AMISTD_1:def 11;
B9:
for
s being
State of
(STC N) holds
f . s = s +* (NAT .--> (succ (s . NAT )))
[0 ,0 ,0 ] <> [1,0 ,0 ]
by MCART_1:28;
then
not
I in {[0 ,0 ,0 ]}
by A6, A7, RECDEF_2:def 1, TARSKI:def 1;
then
not
I in dom ([0 ,0 ,0 ] .--> (id (product the Object-Kind of (STC N))))
by FUNCOP_1:19;
then A11:
the
Execution of
(STC N) . I = ([1,0 ,0 ] .--> f) . I
by A10, FUNCT_4:12;
A12:
I in {[1,0 ,0 ]}
by A6, A7, RECDEF_2:def 1, TARSKI:def 1;
then A13:
Exec I,
s1 =
f . s1
by A11, FUNCOP_1:13
.=
s1 +* (NAT .--> (succ (s1 . NAT )))
by B9
;
A14:
Exec I,
s2 =
f . s2
by A11, A12, FUNCOP_1:13
.=
s2 +* (NAT .--> (succ (s2 . NAT )))
by B9
;
A15:
dom (Exec I,s1) =
the
carrier of
(STC N)
by PARTFUN1:def 4
.=
dom (Exec I,s2)
by PARTFUN1:def 4
;
for
x being
set st
x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be
set ;
( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A16:
x in (dom (Exec I,s1)) \ NAT
;
(Exec I,s1) . x = (Exec I,s2) . x
then A17:
not
x in NAT
by XBOOLE_0:def 5;
A18:
s1 . NAT =
IC s1
by AMISTD_1:def 11
.=
IC s2
by A8, COMPOS_1:24
.=
s2 . NAT
by AMISTD_1:def 11
;
x in dom (Exec I,s1)
by A16;
then
x in the
carrier of
(STC N)
by PARTFUN1:def 4;
then
x in NAT \/ {NAT }
by AMISTD_1:def 11;
then A19:
x in {NAT }
by A17, XBOOLE_0:def 3;
then A20:
x in dom (NAT .--> (succ (s2 . NAT )))
by FUNCOP_1:19;
x in dom (NAT .--> (succ (s1 . NAT )))
by A19, FUNCOP_1:19;
hence (Exec I,s1) . x =
(NAT .--> (succ (s1 . NAT ))) . x
by A13, FUNCT_4:14
.=
(Exec I,s2) . x
by A14, A18, A20, FUNCT_4:14
;
verum
end; hence
(Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT )
by A15, FUNCT_1:165;
FUNCT_7:def 2 verum