def un.cell

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

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

530# one bit position of the adder
531def 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}:
532  match x y c:
533    case False{} False{} False{}:
534      un.dd(r, d, a, b, ih)
535    case True{} False{} False{}:
536      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))
537    case False{} True{} False{}:
538      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))))
539    case False{} False{} True{}:
540      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))
541    case True{} True{} False{}:
542      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))
543    case True{} False{} True{}:
544      un.dd1(r, d, a, b, ih)
545    case False{} True{} True{}:
546      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))
547    case True{} True{} True{}:
548      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)))