def wp_base

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:293

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

293def wp_base(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +h0: {vs(e) == 0n : Nat}) -> {SG.u32_val(acc) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), vs(e))), 1n+mp) : Nat}:
294  %Equal.sym(Nat, vs(e), 0n, h0) : {SG.u32_val(acc) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), _)), 1n+mp) : Nat}
295  %Equal.sym(Nat, Nat.mul(SG.u32_val(acc), 1n), SG.u32_val(acc), NA.mul_one(SG.u32_val(acc))) : {SG.u32_val(acc) == Nat.mod(_, 1n+mp) : Nat}
296  Equal.sym(Nat, Nat.mod(SG.u32_val(acc), 1n+mp), SG.u32_val(acc), R.mod_of(0n, mp, SG.u32_val(acc), lt_m(mp, hp, acc)))