DivisionNoOverflow.double_value: 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_no_overflow.bend as DivisionNoOverflow
Lines 70-74 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&start_line=70&end_line=74

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Shift

def double_value(d: U32, high: {W.last(32n, bits(d)) == False{} : Bool}) -> {U32.to_nat(U32.shl(d)) == Nat.double(U32.to_nat(d)) : Nat}:
  match d:
    case U32{+w}:
      %Equal.sym(Word(32n), Word.shl(32n, w), Word.shl.put(32n, False{}, w), Shift.same_as_put(32n, w)) : {Word.to_nat(32n, _) == Nat.double(Word.to_nat(32n, w)) : Nat}
      decoded_high(w, False{}, high)

Uses (15):
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=decoded_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend&name=same_as_put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=last