~/jendhub

law wxor_zero

lawful-words@0.1.0.0 · proof_u32.bend:327

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

327law wxor_zero:
328  for +n: Nat
329  for +a: Word(n)
330  for +b: Word(n)
331  {Cmp.is_eq(Word.cmp(n, Word.xor(n, a, b), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, a, b)) : Bool}

Uses (16)

Used by (1)