def internal_dm_wrap

bend-mathlib@0.8.1.0 · u32.bend:861

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

861def internal_dm_wrap(+b: U32, +s: Word(32n), +x: Bool, +r: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), m) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b))) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}:
862  +bn = U32.to_nat(b)
863  +sn = Word.to_nat(32n, s)
864  +v = Nat.add(internal_bv(x), Nat.double(r))
865  %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.add(sn, Nat.sub(m, bn)), m), internal_u32_sub_wrap(m, U32{s}, b, em)) : {Nat.add(bn, _) == v : Nat}
866  internal_wrap_rem(bn, sn, m, v, internal_u32_to_nat_lt(m, b, em), es, internal_bit_double_lt(x, r, bn, hr))