From 67a107c34b5e5c24714a46aa5b572f2c08d84ddf Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 14 May 2017 10:01:27 +0200
Subject: [PATCH] Added PowerMod

---
 discrete_log.txt | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/discrete_log.txt b/discrete_log.txt
index b2e6535..410da66 100644
--- 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
 
 
 
+
-- 
2.1.4