let S be COM-Struct ; for i, j being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let i, j be Nat; for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let p be NAT -defined the InstructionsF of S -valued finite Function; 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 Def9;
then dom (Shift (p,j)) =
{ (m + j) where m is 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 Def9;
now for x being object st x in dom (Shift ((IncAddr (p,i)),j)) holds
(Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . xlet x be
object ;
( 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 Nat : m in dom (IncAddr (p,i)) }
by A3, VALUED_1:def 12;
then consider m being
Nat such that A4:
x = m + j
and A5:
m in dom (IncAddr (p,i))
;
A6:
m in dom p
by A5, Def9;
dom (Shift (p,j)) = { (mm + j) where mm is Nat : mm in dom p }
by VALUED_1:def 12;
then A7:
x9 in dom (Shift (p,j))
by A4, A6;
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
A8:
p /. mm =
p . m
by A6, PARTFUN1:def 6
.=
(Shift (p,j)) . (m + j)
by A6, VALUED_1:def 12
.=
(Shift (p,j)) /. xx
by A4, A7, PARTFUN1:def 6
;
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 A6, A8, Def9
.=
(IncAddr ((Shift (p,j)),i)) . x
by A7, Def9
;
verum end;
hence
Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
by A1, FUNCT_1:2; verum