def internal_full_add

bend-mathlib@0.8.1.0 · u32.bend:193

import Base

193def internal_full_add(a: Bool, b: Bool, c: Bool) -> {Nat.add(Nat.add(internal_bv(a), internal_bv(b)), internal_bv(c)) == Nat.add(internal_bv(Pair.fst(Bool, Bool, Bool.full_add(a, b, c))), Nat.double(internal_bv(Pair.snd(Bool, Bool, Bool.full_add(a, b, c))))) : Nat}:
194  match a b c:
195    case False{} False{} False{}:
196      {==}
197    case False{} False{} True{}:
198      {==}
199    case False{} True{} False{}:
200      {==}
201    case False{} True{} True{}:
202      {==}
203    case True{} False{} False{}:
204      {==}
205    case True{} False{} True{}:
206      {==}
207    case True{} True{} False{}:
208      {==}
209    case True{} True{} True{}:
210      {==}