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 il being Element of NAT
for g being NAT -defined the Instructions of b₁ -valued finite Function
for k being Element of NAT
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
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 il being Element of NAT
for g being NAT -defined the Instructions of S -valued finite Function
for k being Element of NAT
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let il be Element of NAT ; :: thesis: for g being NAT -defined the Instructions of S -valued finite Function
for k being Element of NAT
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let g be NAT -defined the Instructions of S -valued finite Function; :: thesis: for k being Element of NAT
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let k be Element of NAT ; :: thesis: for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let I be Instruction of S; :: thesis: ( il in dom g & I = g . il implies IncAddr (I,k) = (Reloc (g,k)) . (il + k) )
assume that
A1: il in dom g and
A2: I = g . il ; :: thesis: IncAddr (I,k) = (Reloc (g,k)) . (il + k)
reconsider ii = il as Element of NAT ;
A3: il in dom (IncAddr (g,k)) by A1, Def40;
thus (Reloc (g,k)) . (il + k) = (IncAddr ((Shift (g,k)),k)) . (il + k)
.= (Shift ((IncAddr (g,k)),k)) . (il + k) by Th121
.= (IncAddr (g,k)) . il by A3, VALUED_1:def 12
.= IncAddr ((g /. ii),k) by A1, Def40
.= IncAddr (I,k) by A1, A2, PARTFUN1:def 8 ; :: thesis: verum