law byte_put_same

lawful-words@0.1.0.0 · LAWS.bend:328

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

328# Byte j of a word whose byte j was set to b (below 256) is b.
329law byte_put_same:
330  for w: U32
331  for j: Nat
332  for b: U32
333  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
334  for hb: {U32.is_lt(b, 256) == True{} : Bool}
335  {D.byte(D.put_byte(w, j, b), j) == b : U32}