let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for i, j being Element of NAT
for p being NAT -defined the Instructions of b1 -valued FinPartState of holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; for i, j being Element of NAT
for p being NAT -defined the Instructions of S -valued FinPartState of holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
let i, j be Element of NAT ; for p being NAT -defined the Instructions of S -valued FinPartState of holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
let p be NAT -defined the Instructions of S -valued FinPartState of ; Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
set f = Shift (IncAddr p,i),j;
set g = IncAddr (Shift p,j),i;
dom (IncAddr p,i) = dom p
by Def15;
then dom (Shift p,j) =
{ (m + j) where m is Element of NAT : m in dom (IncAddr p,i) }
by VALUED_1:def 12
.=
dom (Shift (IncAddr p,i),j)
by VALUED_1:def 12
;
then A1:
dom (Shift (IncAddr p,i),j) = dom (IncAddr (Shift p,j),i)
by Def15;
now let x be
set ;
( x in dom (Shift (IncAddr p,i),j) implies (Shift (IncAddr p,i),j) . x = (IncAddr (Shift p,j),i) . x )A2:
dom (Shift (IncAddr p,i),j) c= NAT
by RELAT_1:def 18;
assume A3:
x in dom (Shift (IncAddr p,i),j)
;
(Shift (IncAddr p,i),j) . x = (IncAddr (Shift p,j),i) . xthen reconsider x9 =
x as
Element of
NAT by A2;
reconsider xx =
x9 as
Element of
NAT ;
x in { (m + j) where m is Element of NAT : m in dom (IncAddr p,i) }
by A3, VALUED_1:def 12;
then consider m being
Element of
NAT such that A4:
x = m + j
and A5:
m in dom (IncAddr p,i)
;
A7:
m in dom p
by A5, Def15;
dom (Shift p,j) = { (mm + j) where mm is Element of NAT : mm in dom p }
by VALUED_1:def 12;
then A8:
x9 in dom (Shift p,j)
by A4, A7;
reconsider mm =
m as
Element of
NAT ;
A9:
p /. mm =
p . m
by A7, PARTFUN1:def 8
.=
(Shift p,j) . (m + j)
by A7, VALUED_1:def 12
.=
(Shift p,j) /. xx
by A4, A8, PARTFUN1:def 8
;
thus (Shift (IncAddr p,i),j) . x =
(IncAddr p,i) . m
by A5, A4, VALUED_1:def 12
.=
IncAddr ((Shift p,j) /. xx),
i
by A7, A9, Def15
.=
(IncAddr (Shift p,j),i) . x
by A8, Def15
;
verum end;
hence
Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
by A1, FUNCT_1:9; verum