def pm_140

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:215

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

215def pm_140(+j: Nat, +m: Nat, +e: Nat, +base: Nat, +acc: Nat, +hj: {Nat.is_le(j, 140n) == True{} : Bool}, +he: {Nat.is_lt(e, C.pow2(j)) == True{} : Bool}) -> {M.pow_mod_go(140n, m, e, base, acc) == M.pow_mod_go(e, m, e, base, acc) : Nat}:
216  pm_fuel(140n, e, m, e, base, acc, bends_bound(j, 140n, e, he, hj), bends_self(e, e, N.le_refl(e)))