improve pow axiomatization

LeventErkok · Oct 8, 2024 · 14b3777 · 14b3777
1 parent cc2e013
commit 14b3777
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -99,7 +99,7 @@ elevenMinusFour = runKD $ do
        emf :: SInteger -> SBool
        emf n = 7 `sDivides` (11 `pow` n - 4 `pow` n)
 
-   pow0 <- axiom "pow0" (\(Forall @"x" x)                 -> x `pow` 0     .== 1)
-   powN <- axiom "powN" (\(Forall @"x" x) (Forall @"n" n) -> x `pow` (n+1) .== x * x `pow` n)
+   pow0 <- axiom "pow0" (\(Forall @"x" x)                 ->             x `pow` 0     .== 1)
+   powN <- axiom "powN" (\(Forall @"x" x) (Forall @"n" n) -> n .>= 0 .=> x `pow` (n+1) .== x * x `pow` n)
 
    lemma "elevenMinusFour" (\(Forall @"n" n) -> n .>= 0 .=> emf n) [pow0, powN, induct emf]