let i be Element of NAT ; for p being NAT -defined the Instructions of SCM -valued finite Function holds Shift (IncAddr p,i),i = Reloc p,i
let p be NAT -defined the Instructions of SCM -valued finite Function; Shift (IncAddr p,i),i = Reloc p,i
dom (IncAddr p,i) = dom p
by AMISTD_2:def 15;
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 = (Reloc p,i) . x )assume A3:
x in dom (Shift (IncAddr p,i),i)
;
(Shift (IncAddr p,i),i) . x = (Reloc p,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, AMISTD_2:def 15;
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, AMISTD_2:def 15
.=
(Reloc p,i) . x
by A8, AMISTD_2:def 15
;
verum end;
dom (Reloc p,i) = dom (Shift p,i)
by AMISTD_2:def 15;
hence
Shift (IncAddr p,i),i = Reloc p,i
by A1, A2, FUNCT_1:9; verum