def un.sub_v

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

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

681# s + B = A + 2^n * C, from adc(a, not b, True) + 2^n * carry = 1 + A + not B
682# and 1 + not B + B = 2^n
683def un.sub_v(c: Bool, +n: Nat, +s: Nat, +a: Nat, +b: Nat, +nb: Nat, e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(c))) == 1n+Nat.add(a, nb) : Nat}, en: {1n+Nat.add(nb, b) == U.U32Nat.dbl(n, 1n) : Nat}) -> {Nat.add(s, b) == Nat.add(a, U.U32Nat.dbl(n, U.U32Nat.bit(Bool.not(c)))) : Nat}:
684  match c:
685    case True{}:
686      +k = U.U32Nat.dbl(n, 1n)
687      +e2 = Equal.trans(Nat, Nat.add(Nat.add(s, b), k), Nat.add(Nat.add(s, k), b), Nat.add(a, k), un.add_swap(s, b, k), Equal.trans(Nat, Nat.add(Nat.add(s, k), b), Nat.add(1n+Nat.add(a, nb), b), Nat.add(a, k), Equal.cong(Nat, Nat, v => Nat.add(v, b), Nat.add(s, k), 1n+Nat.add(a, nb), e), un.sub_mid(a, nb, b, k, en)))
688      +e3 = un.add_cancel_r(Nat.add(s, b), a, k, e2)
689      Equal.trans(Nat, Nat.add(s, b), a, Nat.add(a, U.U32Nat.dbl(n, 0n)), e3, Equal.trans(Nat, a, Nat.add(a, 0n), Nat.add(a, U.U32Nat.dbl(n, 0n)), Equal.sym(Nat, Nat.add(a, 0n), a, un.add_zero(a)), Equal.cong(Nat, Nat, v => Nat.add(a, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, Laws.dbl_zero(n)))))
690    case False{}:
691      +e0 = Equal.trans(Nat, s, Nat.add(s, 0n), 1n+Nat.add(a, nb), Equal.sym(Nat, Nat.add(s, 0n), s, un.add_zero(s)), Equal.trans(Nat, Nat.add(s, 0n), Nat.add(s, U.U32Nat.dbl(n, 0n)), 1n+Nat.add(a, nb), Equal.cong(Nat, Nat, v => Nat.add(s, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, Laws.dbl_zero(n))), e))
692      Equal.trans(Nat, Nat.add(s, b), Nat.add(1n+Nat.add(a, nb), b), Nat.add(a, U.U32Nat.dbl(n, 1n)), Equal.cong(Nat, Nat, v => Nat.add(v, b), s, 1n+Nat.add(a, nb), e0), un.sub_mid(a, nb, b, U.U32Nat.dbl(n, 1n), en))