let k 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 p being NAT -defined FinPartState of S
for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
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 p being NAT -defined FinPartState of S
for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for p being NAT -defined FinPartState of S
for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
let p be NAT -defined FinPartState of S; :: thesis: for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
let l be Element of NAT ; :: thesis: ( l in dom p implies (IncAddr p,k) . l = IncAddr (pi p,l),k )
assume A1: l in dom p ; :: thesis: (IncAddr p,k) . l = IncAddr (pi p,l),k
l is Instruction-Location of S by AMI_1:def 4;
then ex m being natural number st l = il. S,m by AMISTD_1:26;
hence (IncAddr p,k) . l = IncAddr (pi p,l),k by A1, Def15; :: thesis: verum