let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for p being NAT -defined the Instructions 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 Instructions 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) = IncAddr ((IncAddr ((Shift ((Shift (p,m)),n)),m)),n) by Th121
.= IncAddr ((IncAddr ((Shift (p,(m + n))),m)),n) by VALUED_1:21
.= Reloc (p,(m + n)) by Th99 ; :: thesis: verum