let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for p being NAT -defined FinPartState of
for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for p being NAT -defined FinPartState of
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 N; :: thesis: for p being NAT -defined FinPartState of
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 ; :: 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
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