def internal_dm_shl

bend-mathlib@0.8.1.0 · u32.bend:887

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

887def internal_dm_shl(+p: Nat, +q: Word(p), +b: U32, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, ts: Bool & Word(32n), es: {internal_shl_val(32n, md, ts) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.shl(p, q, b, ts)):
888  match ts:
889    case (+t, +s):
890      internal_dm_fin(p, q, s, b, x, r, a, md, em, t, Bool.or(t, U32.is_ge(U32{s}, b)), ea, hr, es, {==})