def pm_fuel

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

204def pm_fuel(+f1: Nat, +f2: Nat, +m: Nat, +e: Nat, +base: Nat, +acc: Nat, +h1: {bends(f1, e) == True{} : Bool}, +h2: {bends(f2, e) == True{} : Bool}) -> {M.pow_mod_go(f1, m, e, base, acc) == M.pow_mod_go(f2, m, e, base, acc) : Nat}:
205  match f1 f2 e:
206    case _ _ 0n:
207      Equal.trans(Nat, M.pow_mod_go(f1, m, 0n, base, acc), acc, M.pow_mod_go(f2, m, 0n, base, acc), pm_zero(f1, m, base, acc), Equal.sym(Nat, M.pow_mod_go(f2, m, 0n, base, acc), acc, pm_zero(f2, m, base, acc)))
208    case 0n _ 1n+ep:
209      Empty.absurd({M.pow_mod_go(0n, m, 1n+ep, base, acc) == M.pow_mod_go(f2, m, 1n+ep, base, acc) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
210    case 1n+g1 0n 1n+ep:
211      Empty.absurd({M.pow_mod_go(1n+g1, m, 1n+ep, base, acc) == M.pow_mod_go(0n, m, 1n+ep, base, acc) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))
212    case 1n+ +g1 1n+ +g2 1n+ +ep:
213      pm_fuel(g1, g2, m, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(base, base), m), M.pow_mod_odd(m, Nat.mod(1n+ep, 2n), base, acc), h1, h2)