DivisionShift.exact: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend as DivisionShift
Lines 53-55 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&start_line=53&end_line=55

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/word_shift.bend as Shift
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as Bounds

# The range premise concerns the inputs and discharges discarded carry.
def exact(+n: Nat, +w: Word(n), +bit: Bool, bound: {Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))), S.scale_binary(n, 1n)) == True{} : Bool}) -> {S.unsigned(n, Word.shl.put(n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))) : Nat}:
  Bounds.no_wrap(n, S.unsigned(n, Word.shl.put(n, bit, w)), Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))), Shift.carry(n, bit, w), Shift.conservation(n, bit, w), bound)

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=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=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.shl.put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend&name=no_wrap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend&name=carry
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend&name=conservation
  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=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