PROOF.un.cell: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 530-548 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=530&end_line=548

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

# one bit position of the adder
def un.cell(x: Bool, y: Bool, c: Bool, +r: Nat, +d: Nat, +a: Nat, +b: Nat, ih: {Nat.add(r, d) == Nat.add(U.U32Nat.bit(un.maj(x, y, c)), Nat.add(a, b)) : Nat}) -> {Nat.add(un.bv(un.sum(x, y, c), r), Nat.double(d)) == Nat.add(U.U32Nat.bit(c), Nat.add(un.bv(x, a), un.bv(y, b))) : Nat}:
  match x y c:
    case False{} False{} False{}:
      un.dd(r, d, a, b, ih)
    case True{} False{} False{}:
      un.succ_cong(Nat.add(Nat.double(r), Nat.double(d)), Nat.add(Nat.double(a), Nat.double(b)), un.dd(r, d, a, b, ih))
    case False{} True{} False{}:
      Equal.trans(Nat, 1n+Nat.add(Nat.double(r), Nat.double(d)), 1n+Nat.add(Nat.double(a), Nat.double(b)), Nat.add(Nat.double(a), 1n+Nat.double(b)), un.succ_cong(Nat.add(Nat.double(r), Nat.double(d)), Nat.add(Nat.double(a), Nat.double(b)), un.dd(r, d, a, b, ih)), Equal.sym(Nat, Nat.add(Nat.double(a), 1n+Nat.double(b)), 1n+Nat.add(Nat.double(a), Nat.double(b)), un.add_succ(Nat.double(a), Nat.double(b))))
    case False{} False{} True{}:
      un.succ_cong(Nat.add(Nat.double(r), Nat.double(d)), Nat.add(Nat.double(a), Nat.double(b)), un.dd(r, d, a, b, ih))
    case True{} True{} False{}:
      Equal.trans(Nat, Nat.add(Nat.double(r), Nat.double(d)), 2n+Nat.add(Nat.double(a), Nat.double(b)), 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)), un.dd1(r, d, a, b, ih), un.sh(a, b))
    case True{} False{} True{}:
      un.dd1(r, d, a, b, ih)
    case False{} True{} True{}:
      Equal.trans(Nat, Nat.add(Nat.double(r), Nat.double(d)), 2n+Nat.add(Nat.double(a), Nat.double(b)), 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)), un.dd1(r, d, a, b, ih), un.sh(a, b))
    case True{} True{} True{}:
      un.succ_cong(Nat.add(Nat.double(r), Nat.double(d)), 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)), Equal.trans(Nat, Nat.add(Nat.double(r), Nat.double(d)), 2n+Nat.add(Nat.double(a), Nat.double(b)), 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)), un.dd1(r, d, a, b, ih), un.sh(a, b)))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.bv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.dd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.dd1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.maj
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.sh
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.succ_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.sum
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit