U32Division.step: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_division.bend as U32Division
Lines 45-54 of stelliferous@0.0.2.0/proofs/u32_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&start_line=45&end_line=54

import Base
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision

law step:
  for +p: Nat
  for +bit: Bool
  for +b: U32
  for +cap: U32
  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
  for +divisor_bound: {Nat.is_le(Nat.double(U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}
  for pair: Word(p) & U32
  for small: {Nat.is_lt(BinaryDivision.remainder(decode(p,pair)),U32.to_nat(b)) == True{} : Bool}
  {decode(1n+p,U32.divmod.go.rec(p,bit,b,pair)) == BinaryDivision.step(bit,U32.to_nat(b),decode(p,pair)) : BinaryDivision.Quotient}

Uses (37):
  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=Nat.is_ge
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.rec
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ge
  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.out
  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/binary_division.bend&name=Quotient
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=branch
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=remainder
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=digit_bounded
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=le_double
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=transitive
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=uint_trans
  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_comparison.bend&name=ge
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=fin
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=nat_le_native
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=nat_lt_native
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=shifted_bound
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=bounded_put
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=no_carry