law byte_put_other

lawful-words@0.1.0.0 · LAWS.bend:337

import Base
import lawful-words@0.1.0.0/defs.bend as D

337# Setting byte j leaves every other byte as it was (from j = 4 up,
338# put_byte changes nothing).
339law byte_put_other:
340  for w: U32
341  for i: Nat
342  for j: Nat
343  for b: U32
344  for hb: {U32.is_lt(b, 256) == True{} : Bool}
345  for hij: {Nat.is_eq(i, j) == False{} : Bool}
346  {D.byte(D.put_byte(w, j, b), i) == D.byte(w, i) : U32}