law step

stelliferous@0.0.2.0 · proofs/u32_division.bend:45

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

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