def un.bao

bend-osdev-u32@0.1.0.0 · PROOF.bend:1886

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

1886def un.bao(x: Bool, y: Bool) -> {Nat.add(U.U32Nat.bit(Bool.and(x, y)), U.U32Nat.bit(Bool.or(x, y))) == Nat.add(U.U32Nat.bit(x), U.U32Nat.bit(y)) : Nat}:
1887  match x y:
1888    case True{} True{}:
1889      {==}
1890    case True{} False{}:
1891      {==}
1892    case False{} True{}:
1893      {==}
1894    case False{} False{}:
1895      {==}