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