U32half.shr_value: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as U32half
Lines 53-56 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend&start_line=53&end_line=56

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

def shr_value(+x: U32) -> {U32.to_nat(U32.shr(x)) == hlf(U32.to_nat(x)) : Nat}:
  %Equal.sym(Nat, U32.to_nat(x), Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))), U.shr_split(x)) : {U32.to_nat(U32.shr(x)) == hlf(_) : Nat}
  Equal.sym(Nat, hlf(Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x))))), U32.to_nat(U32.shr(x)),
    hlf_bit(U.low_bit(x), U32.to_nat(U32.shr(x))))

Uses (12):
  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.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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=low_bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=shr_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend&name=hlf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend&name=hlf_bit