U64.add: 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 222-228 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=222&end_line=228

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
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/modular_addition.bend as MA
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

# THEOREM: add is 64-bit wrapping addition.
def add(+a: U.U64, +b: U.U64) -> {bits(U.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}:
  Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(a), val(b))), Word.add(64n, bits(a), bits(b)),
    Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), S.from_nat(64n, Nat.add(val(a), val(b))),
      Equal.sym(Word(64n), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), bits(U.add(a, b)), MA.reconstruct(64n, bits(U.add(a, b)), add_over(a, b))),
      Equal.cong(Nat, Word(64n), z => S.from_nat(64n, z), Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b))), Nat.add(val(a), val(b)), add_value(a, b))),
    Equal.sym(Word(64n), Word.add(64n, bits(a), bits(b)), S.from_nat(64n, Nat.add(val(a), val(b))), WA.refines(64n, bits(a), bits(b))))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.add
  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/proofs/word_addition.bend&name=refines
  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/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=add_over
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=add_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=add