~/jendhub

def natural_remainder

stelliferous@0.0.2.0 · proofs/u32_division.bend:132

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

132def natural_remainder(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.mod(Word.to_nat(32n,w),
133    b) == BinaryDivision.remainder(BinaryDivision.go(32n,w,b)) : Nat}:
134  %Equal.sym(Nat & Nat,Nat.divmod(Word.to_nat(32n,w),b),BinaryDivision.pair(BinaryDivision.go(32n,w,b)),BinaryDivision.natural(32n,w,b,
135      positive)) : {Pair.snd(Nat,Nat,_) == BinaryDivision.remainder(BinaryDivision.go(32n,w,b)) : Nat}
136  remainder_pair(BinaryDivision.go(32n,w,b))

Uses (15)

Used by (1)