law byte_not

lawful-words@0.1.0.0 · proof_bytes.bend:660

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

660law byte_not:
661  for +a: U32
662  for +j: Nat
663  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
664  {D.byte(U32.not(a), j) == U32.xor(D.byte(a, j), 255) : U32}