WordPowerOfTwo.native_half_power: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as WordPowerOfTwo
Lines 298-301 of stelliferous@0.0.2.0/proofs/word_power_of_two.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&start_line=298&end_line=301

import Base

law native_half_power:
  for +depth: Nat
  for fits: {Nat.is_lt(depth,31n) == True{} : Bool}
  {U32.shr(U32.shln(1,1n+depth)) == U32.shln(1,depth) : U32}

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=Equal.cong
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shr.pad
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=native_power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=pad_power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=power