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
  Asms  : 1                             Q.E.D.
  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
  Asms  : 1                             Q.E.D.
  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
  Asms  : 1                             Q.E.D.
  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: Case split 3 ways:
    Case [1 of 3]: n_mod_3[1]           Q.E.D.
    Case [2 of 3]: n_mod_3[2]           Q.E.D.
    Case [3 of 3]: n_mod_3[3]           Q.E.D.
    Completeness:                       Q.E.D.
  Result:                               Q.E.D.
[Proven] notDiv3