Word.add_one: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 237-246 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=237&end_line=246

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA

# adding one is incrementing
def add_one(+p: Nat, +x: Word(1n+p)) -> {Word.add(1n+p, x, one_word(p)) == Word.inc(1n+p, x) : Word(1n+p)}:
  +ux = uw(1n+p, x)
  +u1 = Equal.cong(Nat, Nat, z => Nat.add(1n, Nat.double(z)), uw(p, Word.zero(p)), 0n, A.uw_zero(p))
  Equal.trans(Word(1n+p), Word.add(1n+p, x, one_word(p)), S.from_nat(1n+p, Nat.add(ux, uw(1n+p, one_word(p)))), Word.inc(1n+p, x),
    WA.refines(1n+p, x, one_word(p)),
    Equal.trans(Word(1n+p), S.from_nat(1n+p, Nat.add(ux, uw(1n+p, one_word(p)))), S.from_nat(1n+p, 1n+ux), Word.inc(1n+p, x),
      Equal.cong(Nat, Word(1n+p), z => S.from_nat(1n+p, z), Nat.add(ux, uw(1n+p, one_word(p))), 1n+ux,
        Equal.trans(Nat, Nat.add(ux, uw(1n+p, one_word(p))), Nat.add(ux, 1n), 1n+ux, Equal.cong(Nat, Nat, z => Nat.add(ux, z), uw(1n+p, one_word(p)), 1n, u1), N.add_comm(ux, 1n))),
      Equal.sym(Word(1n+p), Word.inc(1n+p, x), S.from_nat(1n+p, 1n+ux), MA.increment_refines(1n+p, x))))

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=Nat.double
  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=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend&name=increment_refines
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend&name=refines
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=uw_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=one_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw