let S be COM-Struct ; :: thesis: for il being Nat
for g being NAT -defined the InstructionsF of S -valued finite Function
for k being 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 Nat; :: thesis: for g being NAT -defined the InstructionsF of S -valued finite Function
for k being 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 InstructionsF of S -valued finite Function; :: thesis: for k being 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 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 by ORDINAL1:def 12;
A3: il in dom (IncAddr (g,k)) by A1, Def9;
thus (Reloc (g,k)) . (il + k) = (IncAddr (g,k)) . ii by A3, VALUED_1:def 12
.= IncAddr ((g /. ii),k) by A1, Def9
.= IncAddr (I,k) by A1, A2, PARTFUN1:def 6 ; :: thesis: verum