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

Documentation.SBV.Examples.TP.CaseSplit

Description

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

Synopsis

notDiv3 :: IO (Proof (Forall "n" Integer -> SBool))

Documentation

notDiv3 :: IO (Proof (Forall "n" Integer -> SBool)) Source #

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

We have:

>>> notDiv3
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 :: Ɐn ∷ Integer → Bool