From 14b3777c732d316026bd781a183b7a65d71af876 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 8 Oct 2024 07:37:39 -0700 Subject: [PATCH] improve pow axiomatization --- Documentation/SBV/Examples/KnuckleDragger/Induction.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs index 68fe97e0..488ed55d 100644 --- 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]