let S be COM-Struct ; :: thesis: for k being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))
let k be Nat; :: thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))
let p be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: dom (Reloc (p,k)) = dom (Shift (p,k))
A1: dom (IncAddr (p,k)) = dom p by Def9;
thus dom (Reloc (p,k)) = { (m + k) where m is Nat : m in dom p } by A1, VALUED_1:def 12
.= dom (Shift (p,k)) by VALUED_1:def 12 ; :: thesis: verum