law byte_lt

lawful-words@0.1.0.0 · LAWS.bend:463

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

463# Every byte is below 256.
464law byte_lt:
465  for w: U32
466  for j: Nat
467  {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}