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 homogeneous regular J/A-independent COM-Struct of N
for p being NAT -defined the Instructions of b₁ -valued finite Function
for m, n being Element of NAT holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued finite Function
for m, n being Element of 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 Element of NAT holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let m, n be Element of NAT ; :: thesis: Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
thus Reloc ((Reloc (p,m)),n) = Reloc ((Reloc (p,m)),n)
.= Reloc ((Reloc (p,m)),n)
.= IncAddr ((Shift ((IncAddr ((Shift (p,m)),m)),n)),n)
.= IncAddr ((IncAddr ((Shift ((Shift (p,m)),n)),m)),n) by Th121
.= IncAddr ((IncAddr ((Shift (p,(m + n))),m)),n) by VALUED_1:22
.= Reloc (p,(m + n)) by Th99
.= Reloc (p,(m + n)) ; :: thesis: verum