law go

stelliferous@0.0.2.0 · proofs/u32_division.bend:84

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

84law go:
85  for +n: Nat
86  for +w: Word(n)
87  for +b: U32
88  for +cap: U32
89  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
90  for +divisor_bound: {Nat.is_le(Nat.double(U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}
91  for +positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}
92  {decode(n,U32.divmod.go(n,w,b)) == BinaryDivision.go(n,w,U32.to_nat(b)) : BinaryDivision.Quotient}