let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for k being Element of NAT
for p being NAT -defined the Instructions of b₁ -valued finite Function holds dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for k being Element of NAT
for p being NAT -defined the Instructions of S -valued finite Function holds dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
let k be Element of NAT ; :: thesis: for p being NAT -defined the Instructions of S -valued finite Function holds dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
let p be NAT -defined the Instructions of S -valued finite Function; :: thesis: dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }
thus dom (Reloc p,k) = dom (Shift p,k) by Def15
.= { (j + k) where j is Element of NAT : j in dom p } by VALUED_1:def 12 ; :: thesis: verum