thus
STC N is IC-relocable
STC N is Exec-preserving proof
let I be
Instruction of
(STC N);
AMISTD_2:def 19 I is IC-relocable let j,
k be
natural number ;
AMISTD_2:def 18 for s being State of (STC N) holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))let s1 be
State of
(STC N);
(IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 =
IncIC (
s1,
k);
{(IC )} = dom ((IC ) .--> ((IC s1) + k))
by FUNCOP_1:19;
then
IC in dom ((IC ) .--> ((IC s1) + k))
by TARSKI:def 1;
then A1:
IC (IncIC (s1,k)) =
((IC ) .--> ((IC s1) + k)) . (IC )
by FUNCT_4:14
.=
(IC s1) + k
by FUNCOP_1:87
;
per cases
( InsCode I = 1 or InsCode I = 0 )
by AMISTD_1:22;
suppose A2:
InsCode I = 1
;
(IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))then A3:
InsCode (IncAddr (I,k)) = 1
by COMPOS_1:def 38;
A4:
IncAddr (
I,
j)
= I
by COMPOS_1:92;
IC (Exec (I,s1)) =
succ (IC s1)
by A2, AMISTD_1:38
.=
(IC s1) + 1
;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k =
succ (IC (IncIC (s1,k)))
by A1, A4
.=
IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k))))
by A4, A3, AMISTD_1:38
.=
IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
by COMPOS_1:97
;
verum end; suppose
InsCode I = 0
;
(IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))then A5:
I is
halting
by AMISTD_1:20;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k =
(IC s1) + k
by EXTPRO_1:def 3
.=
IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k))))
by A1, A5, EXTPRO_1:def 3
.=
IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
by COMPOS_1:97
;
verum end;
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 ( NPP s1 = NPP s2 implies NPP (Exec (I,s1)) = NPP (Exec (I,s2)) )assume A8:
NPP s1 = NPP s2
;
NPP (Exec (I,s1)) = NPP (Exec (I,s2))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;
A11:
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 A12:
the
Execution of
(STC N) . I = ([1,0,0] .--> f) . I
by A10, FUNCT_4:12;
A13:
I in {[1,0,0]}
by A6, A7, RECDEF_2:def 1, TARSKI:def 1;
then A14:
Exec (
I,
s1) =
f . s1
by A12, FUNCOP_1:13
.=
s1 +* (NAT .--> (succ (s1 . NAT)))
by A11
;
A15:
Exec (
I,
s2) =
f . s2
by A12, A13, FUNCOP_1:13
.=
s2 +* (NAT .--> (succ (s2 . NAT)))
by A11
;
A16:
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 A17:
x in (dom (Exec (I,s1))) \ NAT
;
(Exec (I,s1)) . x = (Exec (I,s2)) . x
then A18:
not
x in NAT
by XBOOLE_0:def 5;
A19:
s1 . NAT =
IC s1
by AMISTD_1:def 11
.=
IC s2
by A8, COMPOS_1:230
.=
s2 . NAT
by AMISTD_1:def 11
;
x in dom (Exec (I,s1))
by A17;
then
x in the
carrier of
(STC N)
by PARTFUN1:def 4;
then
x in NAT \/ {NAT}
by AMISTD_1:def 11;
then A20:
x in {NAT}
by A18, XBOOLE_0:def 3;
then A21:
x in dom (NAT .--> (succ (s2 . NAT)))
by FUNCOP_1:19;
x in dom (NAT .--> (succ (s1 . NAT)))
by A20, FUNCOP_1:19;
hence (Exec (I,s1)) . x =
(NAT .--> (succ (s1 . NAT))) . x
by A14, FUNCT_4:14
.=
(Exec (I,s2)) . x
by A15, A19, A21, FUNCT_4:14
;
verum
end; then
(Exec (I,s1)) | ((dom (Exec (I,s1))) \ NAT) = (Exec (I,s2)) | ((dom (Exec (I,s2))) \ NAT)
by A16, FUNCT_1:165;
hence
NPP (Exec (I,s1)) = NPP (Exec (I,s2))
by COMPOS_1:233;
verum