let i, j be Element of NAT ; for p being preProgram of SCM+FSA holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
let p be preProgram of SCM+FSA ; Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
dom (IncAddr p,i) = dom p
by Def6;
then A1: 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
;
A2:
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 )assume A3:
x in dom (Shift (IncAddr p,i),j)
;
(Shift (IncAddr p,i),j) . x = (IncAddr (Shift p,j),i) . xthen A4:
x in { (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) c= NAT
by RELAT_1:def 18;
then reconsider x9 =
x as
Element of
NAT by A3;
reconsider xx =
x9 as
Element of
NAT ;
consider m being
Element of
NAT such that A5:
x = m + j
and A6:
m in dom (IncAddr p,i)
by A4;
A7:
m in dom p
by A6, Def6;
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 A5, A7;
A9:
pi p,
m =
p . m
by A7, AMI_1:def 47
.=
(Shift p,j) . (m + j)
by A7, VALUED_1:def 12
.=
(Shift p,j) . (m + j)
.=
pi (Shift p,j),
xx
by A5, A8, AMI_1:def 47
;
thus (Shift (IncAddr p,i),j) . x =
(IncAddr p,i) . m
by A5, A6, VALUED_1:def 12
.=
IncAddr (pi (Shift p,j),xx),
i
by A7, A9, Th24
.=
(IncAddr (Shift p,j),i) . x
by A8, Th24
;
verum end;
dom (IncAddr (Shift p,j),i) = dom (Shift p,j)
by Def6;
hence
Shift (IncAddr p,i),j = IncAddr (Shift p,j),i
by A1, A2, FUNCT_1:9; verum