let S be COM-Struct ; :: thesis: for p being NAT -defined the InstructionsF of S -valued finite Function
for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let p be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let m, n be Nat; :: thesis: Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
thus Reloc ((Reloc (p,m)),n) = Shift ((Shift ((IncAddr ((IncAddr (p,m)),n)),m)),n) by Th22
.= Shift ((Shift ((IncAddr (p,(m + n))),m)),n) by Th8
.= Reloc (p,(m + n)) by VALUED_1:21 ; :: thesis: verum