Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.KnuckleDragger.CaseSplit

Description

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

Synopsis

notDiv3 :: IO Proof

Documentation

notDiv3 :: IO Proof Source #

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

We have:

>>> notDiv3
Lemma: case_n_mod_3_eq_0
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
Lemma: case_n_mod_3_eq_1
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
Lemma: case_n_mod_3_eq_2
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
Lemma: notDiv3
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] notDiv3