Word.sub_wrap: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 71-91 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=71&end_line=91

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/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

# If x + 2^n == d + b with d < 2^n, the machine difference x - b is d.
def sub_wrap(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +xw: Word(n), +bw: Word(n), +d: Nat, +e: {Nat.add(uw(n, xw), sc(n, one)) == Nat.add(d, uw(n, bw)) : Nat}, +hd: {Nat.is_lt(d, sc(n, one)) == True{} : Bool}) -> {uw(n, Word.sub(n, xw, bw)) == d : Nat}:
  +us = uw(n, Word.sub(n, xw, bw))
  +ux = uw(n, xw)
  +ub = uw(n, bw)
  +un = uw(n, Word.not(n, bw))
  +c5 = A.cy(n, xw, Word.not(n, bw), True{})
  +e5 = A.cons_sub(n, xw, bw)
  +nv = A.not_value(n, bw)
  +ew = L.subst(Nat, o => {Nat.add(ux, S.scale_binary(n, o)) == Nat.add(d, ub) : Nat}, one, 1n, h1, e)
  # (1 + (ux + un)) + ub == ux + (1 + (un + ub)) == ux + 2^n
  +mid = Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), 1n+Nat.add(ux, Nat.add(un, ub)), Nat.add(ux, sc(n, 1n)),
    N.succ_cong(Nat.add(Nat.add(ux, un), ub), Nat.add(ux, Nat.add(un, ub)), N.add_assoc(ux, un, ub)),
    Equal.trans(Nat, 1n+Nat.add(ux, Nat.add(un, ub)), Nat.add(ux, 1n+Nat.add(un, ub)), Nat.add(ux, sc(n, 1n)), Equal.sym(Nat, Nat.add(ux, 1n+Nat.add(un, ub)), 1n+Nat.add(ux, Nat.add(un, ub)), N.add_succ(ux, Nat.add(un, ub))), Equal.cong(Nat, Nat, z => Nat.add(ux, z), Nat.add(1n, Nat.add(un, ub)), sc(n, 1n), nv)))
  +chain = Equal.trans(Nat, Nat.add(Nat.add(us, sc(n, c5)), ub), Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), Nat.add(d, ub),
    Equal.cong(Nat, Nat, z => Nat.add(z, ub), Nat.add(us, sc(n, c5)), Nat.add(1n, Nat.add(ux, un)), e5),
    Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), Nat.add(ux, sc(n, 1n)), Nat.add(d, ub), mid, ew))
  +e0 = A.add_cancel_r(Nat.add(us, sc(n, c5)), d, ub, chain)
  +e1 = Equal.trans(Nat, Nat.add(us, sc(n, c5)), d, Nat.add(d, sc(n, 0n)), e0,
    Equal.trans(Nat, d, Nat.add(d, 0n), Nat.add(d, sc(n, 0n)), Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)), Equal.cong(Nat, Nat, z => Nat.add(d, z), 0n, sc(n, 0n), Equal.sym(Nat, sc(n, 0n), 0n, A.sc_zero(n)))))
  uniq(n, one, h1, us, d, c5, 0n, e1, wb(n, one, h1, Word.sub(n, xw, bw)), hd)

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.sub
  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/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=succ_cong
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=add_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=cons_sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=cy
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=not_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=sc_zero
  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=uniq
  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/lib/word.bend&name=wb