let i be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for p being NAT -defined FinPartState of S holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for p being NAT -defined FinPartState of S holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for p being NAT -defined FinPartState of S holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let p be NAT -defined FinPartState of S; :: thesis: Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
set f = Shift (IncAddr p,i),i;
set g = IncAddr (Shift p,i),i;
dom (IncAddr p,i) = dom p
by Def15;
then dom (Shift p,i) =
{ (il. S,(m + i)) where m is Element of NAT : il. S,m in dom (IncAddr p,i) }
by Def16
.=
dom (Shift (IncAddr p,i),i)
by Def16
;
then A1:
dom (Shift (IncAddr p,i),i) = dom (IncAddr (Shift p,i),i)
by Def15;
now let x be
set ;
:: thesis: ( x in dom (Shift (IncAddr p,i),i) implies (Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . x )A2:
dom (Shift (IncAddr p,i),i) c= NAT
by RELAT_1:def 18;
assume A3:
x in dom (Shift (IncAddr p,i),i)
;
:: thesis: (Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . xthen reconsider x' =
x as
Instruction-Location of
S by A2, AMI_1:def 4;
reconsider xx =
x' as
Element of
NAT by ORDINAL1:def 13;
x in { (il. S,(m + i)) where m is Element of NAT : il. S,m in dom (IncAddr p,i) }
by A3, Def16;
then consider m being
Element of
NAT such that A4:
x = il. S,
(m + i)
and A5:
il. S,
m in dom (IncAddr p,i)
;
A6:
x = (il. S,m) + i
by A4, AMISTD_1:def 13;
A7:
il. S,
m in dom p
by A5, Def15;
dom (Shift p,i) = { (il. S,(mm + i)) where mm is Element of NAT : il. S,mm in dom p }
by Def16;
then A8:
x' in dom (Shift p,i)
by A4, A7;
reconsider mm =
il. S,
m as
Element of
NAT by ORDINAL1:def 13;
A9:
pi p,
mm =
p . (il. S,m)
by A7, AMI_1:def 47
.=
(Shift p,i) . ((il. S,m) + i)
by A7, Th65
.=
(Shift p,i) . (il. S,(m + i))
by AMISTD_1:def 13
.=
pi (Shift p,i),
xx
by A4, A8, AMI_1:def 47
;
thus (Shift (IncAddr p,i),i) . x =
(IncAddr p,i) . (il. S,m)
by A5, A6, Th65
.=
IncAddr (pi (Shift p,i),xx),
i
by A7, A9, Th74
.=
(IncAddr (Shift p,i),i) . x
by A8, Th74
;
:: thesis: verum end;
hence
Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
by A1, FUNCT_1:9; :: thesis: verum