law byte_not

lawful-words@0.1.0.0 · LAWS.bend:409

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

409law byte_not:
410  for a: U32
411  for j: Nat
412  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
413  {D.byte(U32.not(a), j) == U32.xor(D.byte(a, j), 255) : U32}