Added PowerMod

diff --git a/discrete_log.txt b/discrete_log.txt
index b2e6535..410da66 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -51,6 +51,21 @@ proc IntegerRoot(a:nat): nat
    return x;
 }
 
+proc PowerMod(a:nat, b:nat, p:nat): nat
+{
+   var x:nat;
+
+   if b=0 then
+     x = 1;
+   else
+     x = a%p;
+     for var i:nat=1;i<b;i = i+1 do
+       x = a*x%p;
+   return x;
+}
+
+theorem PowerModWorks() ⇔ ∀a:nat. ∀b:nat. ∀p:nat. p>1 ⇒ PowerMod(a,b,p) = (a^b)%p;
+
 theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒
                           ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1;
 
@@ -123,3 +138,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
 
 
 
+