def internal_dm_go

bend-mathlib@0.8.1.0 · u32.bend:901

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

901def internal_dm_go(m: Nat, w: Word(m), +b: U32, +hb: MNat.lt(0n, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}) -> internal_dm_inv(m, U32.to_nat(b), Word.to_nat(m, w), U32.divmod.go(m, w, b)):
902  match m:
903    case 0n:
904      match w:
905        case WNil{}:
906          ({==}, hb)
907    case 1n++p:
908      match w:
909        case WCon{+x, +hi}:
910          %internal_to_nat_con(p, x, hi) : internal_dm_inv(1n+p, U32.to_nat(b), _, U32.divmod.go(1n+p, WCon{x, hi}, b))
911          internal_dm_rec(p, x, b, md, em, Word.to_nat(p, hi), U32.divmod.go(p, hi, b), internal_dm_go(p, hi, b, hb, md, em))