let k, m be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being NAT -defined lower FinPartState of S holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being NAT -defined lower FinPartState of S holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for F being NAT -defined lower FinPartState of S holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
let F be NAT -defined lower FinPartState of S; :: thesis: 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 ;
:: thesis: ( x in dom F implies (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x )
assume A3:
x in dom F
;
:: thesis: (IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x
dom F c= NAT
by RELAT_1:def 18;
then reconsider x =
x as
Instruction-Location of
S by A3, AMI_1:def 4;
A4:
x = il. S,
(locnum x)
by AMISTD_1:def 13;
then A5:
il. S,
(locnum x) in dom (IncAddr F,k)
by A3, Def15;
A6:
IncAddr (pi F,(il. S,(locnum x))),
k =
(IncAddr F,k) . (il. S,(locnum x))
by A3, A4, Def15
.=
pi (IncAddr F,k),
(il. S,(locnum x))
by A5, AMI_1:def 47
;
(IncAddr (IncAddr F,k),m) . (il. S,(locnum x)) =
IncAddr (pi (IncAddr F,k),(il. S,(locnum x))),
m
by A5, Def15
.=
IncAddr (pi F,(il. S,(locnum x))),
(k + m)
by A6, Th37
.=
(IncAddr F,(k + m)) . (il. S,(locnum x))
by A3, A4, Def15
;
hence
(IncAddr (IncAddr F,k),m) . x = (IncAddr F,(k + m)) . x
by A4;
:: thesis: verum
end;
hence
IncAddr (IncAddr F,k),m = IncAddr F,(k + m)
by A1, A2, FUNCT_1:9; :: thesis: verum