Documentation.SBV.Examples.KnuckleDragger.CaseSplit

Use KnuckleDragger to prove 2n^2 + n + 1 is never divisible by 3.

Documentation

z3NoAutoConfig :: SMTConfig

The default settings for z3 have trouble running this proof out-of-the-box. We have to pass auto_config=false to z3!

notDiv3 :: IO Proof

Prove that 2n^2 + n + 1 is not divisible by 3.

We have:

>>> notDiv3
Chain: case_n_mod_3_eq_0
  Lemma: case_n_mod_3_eq_0.1            Q.E.D.
  Lemma: case_n_mod_3_eq_0.2            Q.E.D.
Lemma: case_n_mod_3_eq_0                Q.E.D.
Chain: case_n_mod_3_eq_1
  Lemma: case_n_mod_3_eq_1.1            Q.E.D.
  Lemma: case_n_mod_3_eq_1.2            Q.E.D.
Lemma: case_n_mod_3_eq_1                Q.E.D.
Chain: case_n_mod_3_eq_2
  Lemma: case_n_mod_3_eq_2.1            Q.E.D.
  Lemma: case_n_mod_3_eq_2.2            Q.E.D.
Lemma: case_n_mod_3_eq_2                Q.E.D.
Lemma: notDiv3                          Q.E.D.
[Proven] notDiv3