let i be Element of NAT ; for p being NAT -defined the Instructions of SCM -valued finite Function holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let p be NAT -defined the Instructions of SCM -valued finite Function; Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
dom (IncAddr p,i) = dom p
by Def5;
then A1: dom (Shift p,i) =
{ (m + i) where m is Element of NAT : m in dom (IncAddr p,i) }
by VALUED_1:def 12
.=
dom (Shift (IncAddr p,i),i)
by VALUED_1:def 12
;
A2:
now let x be
set ;
( x in dom (Shift (IncAddr p,i),i) implies (Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . x )assume A3:
x in dom (Shift (IncAddr p,i),i)
;
(Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . xthen A4:
x in { (m + i) where m is Element of NAT : m in dom (IncAddr p,i) }
by VALUED_1:def 12;
dom (Shift (IncAddr p,i),i) c= NAT
by RELAT_1:def 18;
then reconsider x9 =
x as
Element of
NAT by A3;
consider m being
Element of
NAT such that A5:
x = m + i
and A6:
m in dom (IncAddr p,i)
by A4;
A7:
m in dom p
by A6, Def5;
dom (Shift p,i) = { (mm + i) where mm is Element of NAT : mm in dom p }
by VALUED_1:def 12;
then A8:
x9 in dom (Shift p,i)
by A5, A7;
A9:
p /. m =
p . m
by A7, PARTFUN1:def 8
.=
(Shift p,i) . (m + i)
by A7, VALUED_1:def 12
.=
(Shift p,i) /. x9
by A5, A8, PARTFUN1:def 8
;
thus (Shift (IncAddr p,i),i) . x =
(IncAddr p,i) . m
by A5, A6, VALUED_1:def 12
.=
IncAddr ((Shift p,i) /. x9),
i
by A7, A9, Def5
.=
(IncAddr (Shift p,i),i) . x
by A8, Def5
;
verum end;
dom (IncAddr (Shift p,i),i) = dom (Shift p,i)
by Def5;
hence
Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
by A1, A2, FUNCT_1:9; verum