U32Shift.bounded_put: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
Lines 65-70 of stelliferous@0.0.2.0/proofs/u32_shift.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&start_line=65&end_line=70

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

def bounded_put(+c: Bool,+w: Word(32n),+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Comparison.digit(c,
        Word.to_nat(32n,w)),U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32{Word.shl.put(32n,c,w)}) == Comparison.digit(c,
    Word.to_nat(32n,w)) : Nat}:
  %Equal.sym(U32,U32{Word.shl.put(32n,c,w)},U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))),encoded_put(c,
      w)) : {U32.to_nat(_) == Comparison.digit(c,Word.to_nat(32n,w)) : Nat}
  Bounds.roundtrip(Comparison.digit(c,Word.to_nat(32n,w)),cap,cap_ok,h)

Uses (14):
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  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.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=roundtrip
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=digit
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=encoded_put