U64.add_cons: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
Lines 171-177 of bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&start_line=171&end_line=177

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

def add_cons(+x: U32, +y: U32) -> {Nat.add(UD.v(U32.add(x, y)), WD.sc(32n, S.bit_value(carry32(x, y)))) == Nat.add(UD.v(x), UD.v(y)) : Nat}:
  match x y:
    case U32{+a} U32{+b}:
      %Equal.sym(Nat, UD.v(U32{Word.add(32n, a, b)}), WD.uw(32n, Word.add(32n, a, b)), UD.vw(Word.add(32n, a, b))) : {Nat.add(_, WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(UD.v(U32{a}), UD.v(U32{b})) : Nat}
      %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(_, UD.v(U32{b})) : Nat}
      %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(WD.uw(32n, a), _) : Nat}
      A.cons(32n, 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=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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=carry_out
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=cons
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=vw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=carry32