def wp_base

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:283

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/src/math/u64.bend as WU
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

283def wp_base(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +e: U32, +b: WU.U64, +acc: WU.U64, +h0: {vs(e) == 0n : Nat}) -> {SG.u64_val(acc) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), vs(e))), 1n+mp) : Nat}:
284  %Equal.sym(Nat, vs(e), 0n, h0) : {SG.u64_val(acc) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), _)), 1n+mp) : Nat}
285  %Equal.sym(Nat, Nat.mul(SG.u64_val(acc), 1n), SG.u64_val(acc), NA.mul_one(SG.u64_val(acc))) : {SG.u64_val(acc) == Nat.mod(_, 1n+mp) : Nat}
286  Equal.sym(Nat, Nat.mod(SG.u64_val(acc), 1n+mp), SG.u64_val(acc), R.mod_of(0n, mp, SG.u64_val(acc), lt_m(mp, hp, acc)))