WordAddition.with_carry: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WordAddition
Lines 20-22 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend&start_line=20&end_line=22

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/lemmas/proofs/addition.bend as Add
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as M

def with_carry(+n: Nat, +a: Word(n), +b: Word(n), +carry: Bool) -> {Word.adc(n, a, b, False{}, carry) == S.from_nat(n, Nat.add(S.bit_value(carry), Nat.add(S.unsigned(n, a), S.unsigned(n, b)))) : Word(n)}:
  %Add.adc_conservation(n, a, b, carry) : {Word.adc(n, a, b, False{}, carry) == S.from_nat(n, _) : Word(n)}
  Equal.sym(Word(n), S.from_nat(n, Nat.add(S.unsigned(n, Word.adc(n, a, b, False{}, carry)), S.scale_binary(n, S.bit_value(Add.carry_out(n, a, b, carry))))), Word.adc(n, a, b, False{}, carry), M.reconstruct(n, Word.adc(n, a, b, False{}, carry), S.bit_value(Add.carry_out(n, a, b, carry))))

Uses (13):
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=adc_conservation
  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/proofs/modular_addition.bend&name=reconstruct
  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/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=scale_binary
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned