:: deftheorem Def9 defines IncAddr COMPOS_1:def 21 :
for S being COM-Struct
for p being preProgram of S
for k being Nat
for b₄ being NAT -defined the InstructionsF of b₁ -valued finite Function holds
( b₄ = IncAddr (p,k) iff ( dom b₄ = dom p & ( for m being Nat st m in dom p holds
b₄ . m = IncAddr ((p /. m),k) ) ) );