def internal_dm_rec

bend-mathlib@0.8.1.0 · u32.bend:892

import Base

892def internal_dm_rec(+p: Nat, +x: Bool, +b: U32, +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, -a: Nat, qr: Word(p) & U32, ih: internal_dm_inv(p, U32.to_nat(b), a, qr)) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.rec(p, x, b, qr)):
893  match qr:
894    case (+q, r):
895      match r:
896        case U32{+rw}:
897          match ih:
898            case (ea, +hr):
899              internal_dm_shl(p, q, b, x, Word.to_nat(32n, rw), a, ea, hr, md, em, Word.shl.out(32n, x, rw), internal_shl_out32(md, em, x, rw))