def un.add_v

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

550# adc(a, b, False, c) + 2^n * carry out = c + a + b
551def un.add_v(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), U.U32Nat.dbl(n, U.U32Nat.bit(un.co(n, a, b, c)))) == Nat.add(U.U32Nat.bit(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}:
552  match n:
553    case 0n:
554      match a b c:
555        case WNil{} WNil{} False{}:
556          {==}
557        case WNil{} WNil{} True{}:
558          {==}
559    case 1n+ +p:
560      match a b c:
561        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
562          un.cell(False{}, False{}, False{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, False{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, False{}))
563        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
564          un.cell(True{}, False{}, False{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, False{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, False{}))
565        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
566          un.cell(False{}, True{}, False{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, False{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, False{}))
567        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
568          un.cell(False{}, False{}, True{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, False{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, False{}))
569        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
570          un.cell(True{}, True{}, False{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, True{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, True{}))
571        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
572          un.cell(True{}, False{}, True{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, True{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, True{}))
573        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
574          un.cell(False{}, True{}, True{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, True{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, True{}))
575        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
576          un.cell(True{}, True{}, True{}, Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), U.U32Nat.dbl(p, U.U32Nat.bit(un.co(p, at, bt, True{}))), Word.to_nat(p, at), Word.to_nat(p, bt), un.add_v(p, at, bt, True{}))
def un.add_v

Uses (12)

Used by (3)
