~/jendhub

def pow_pow2

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/roots.bend:192

import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as Roots
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

192# (2^a)^k == 2^(k a)
193def pow_pow2(+a: Nat, +k: Nat) -> {Nat.pow(SC.pow2(a), k) == SC.pow2(Nat.mul(k, a)) : Nat}:
194  match k:
195    case 0n:
196      {==}
197    case 1n+ +kp:
198      Equal.trans(Nat, Nat.mul(SC.pow2(a), Nat.pow(SC.pow2(a), kp)), Nat.mul(SC.pow2(a), SC.pow2(Nat.mul(kp, a))), SC.pow2(Nat.add(a, Nat.mul(kp, a))),
199        Equal.cong(Nat, Nat, z => Nat.mul(SC.pow2(a), z), Nat.pow(SC.pow2(a), kp), SC.pow2(Nat.mul(kp, a)), pow_pow2(a, kp)),
200        Equal.sym(Nat, SC.pow2(Nat.add(a, Nat.mul(kp, a))), Nat.mul(SC.pow2(a), SC.pow2(Nat.mul(kp, a))), pow2_add(a, Nat.mul(kp, a))))

Uses (9)

Used by (1)