:: deftheorem Def8 defines IncAddr COMPOS_0:def 9 :
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S
for k being Nat
for b₄ being Element of S holds
( b₄ = IncAddr (I,k) iff ( InsCode b₄ = InsCode I & AddressPart b₄ = AddressPart I & JumpPart b₄ = k + (JumpPart I) ) );