let N be non empty with_non-empty_elements set ; for k, m being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being NAT -defined the Instructions of b3 -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let k, m be natural number ; for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being NAT -defined the Instructions of b1 -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N; for F being NAT -defined the Instructions of S -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let F be NAT -defined the Instructions of S -valued finite Function; IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
A1: dom (IncAddr ((IncAddr (F,k)),m)) =
dom (IncAddr (F,k))
by Def15
.=
dom F
by Def15
;
A2:
dom (IncAddr (F,(k + m))) = dom F
by Def15;
for x being set st x in dom F holds
(IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
proof
let x be
set ;
( x in dom F implies (IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x )
assume A3:
x in dom F
;
(IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
reconsider x =
x as
Element of
NAT by A3, ORDINAL1:def 13;
A5:
x in dom (IncAddr (F,k))
by A3, Def15;
A6:
IncAddr (
(F /. x),
k) =
(IncAddr (F,k)) . x
by A3, Def15
.=
(IncAddr (F,k)) /. x
by A5, PARTFUN1:def 8
;
(IncAddr ((IncAddr (F,k)),m)) . x =
IncAddr (
((IncAddr (F,k)) /. x),
m)
by A5, Def15
.=
IncAddr (
(F /. x),
(k + m))
by A6, Th37
.=
(IncAddr (F,(k + m))) . x
by A3, Def15
;
hence
(IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
;
verum
end;
hence
IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
by A1, A2, FUNCT_1:9; verum