U32Shift.encoded_put: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
Lines 54-63 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=54&end_line=63

import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

def encoded_put(+c: Bool,+w: Word(32n)) -> {U32{Word.shl.put(32n,c,w)} == U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))) : U32}:
  match c:
    case False{}:
      %WordArithmetic.shift_put(32n,w) : {U32{_} == U32.from_nat(Nat.double(Word.to_nat(32n,w))) : U32}
      encoded_shift(w)
    case True{}:
      %Equal.sym(Word(32n),Word.shl.put(32n,True{},w),Word.inc(32n,Word.shl(32n,w)),put_inc(32n,
          w)) : {U32{_} == U32.inc(U32.from_nat(Nat.double(Word.to_nat(32n,w)))) : U32}
      %encoded_shift(w) : {U32.inc(U32{Word.shl(32n,w)}) == U32.inc(_) : U32}
      {==}

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.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.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  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.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=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_shift
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=put_inc
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=shift_put