diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -3,6 +3,8 @@
 
 [![Speculate Build Status][build-status]][build-log]
 [![Speculate on Hackage][hackage-version]][speculate-on-hackage]
+[![Speculate on Stackage LTS][stackage-lts-badge]][speculate-on-stackage-lts]
+[![Speculate on Stackage Nightly][stackage-nightly-badge]][speculate-on-stackage-nightly]
 
 Speculate automatically discovers laws about [Haskell] functions.
 Give Speculate a bunch of Haskell functions and it will discover laws like:
@@ -136,5 +138,10 @@
 [build-status]: https://travis-ci.org/rudymatela/speculate.svg?branch=master
 [build-log]:    https://travis-ci.org/rudymatela/speculate
 [hackage-version]: https://img.shields.io/hackage/v/speculate.svg
-[speculate-on-hackage]:                  https://hackage.haskell.org/package/speculate
 [latest Speculate version from Hackage]: https://hackage.haskell.org/package/speculate
+[speculate-on-hackage]:                  https://hackage.haskell.org/package/speculate
+[stackage-lts-badge]:            http://stackage.org/package/speculate/badge/lts
+[stackage-nightly-badge]:        http://stackage.org/package/speculate/badge/nightly
+[speculate-on-stackage]:         http://stackage.org/package/speculate
+[speculate-on-stackage-lts]:     http://stackage.org/lts/package/speculate
+[speculate-on-stackage-nightly]: http://stackage.org/nightly/package/speculate
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -9,13 +9,7 @@
 current
 -------
 
-* automatically detect and use orders.  algorithm sketch:
-  1. list everything of the type a -> a -> Bool
-  2. check and filter everything that is an order
-  3. parameterize semiTheoryFromEtc so that it takes an order re-run for
-     several different types
-
-* consistency: rename semi to inequations everywhere.
+* consistency: rename semi to inqualities everywhere.
 
 * improve printing by separating variables, constants and background constants.
 
@@ -23,33 +17,13 @@
   Maybe a new field in args?  Or even things begining with capital letters and
   ":".
 
-
-isolate most of the Expr module
--------------------------------
-
-Maybe most of the `Expr` module could be isolated from the rest of Speculate
-and released as a separate package.
-
-I'll have to see how it goes in other modules, specially the `grounds`
-function.  Which could be interesting to include in the "expr" package but
-would still depend on Listable and LeanCheck (maybe make it depend on it
-anyway...)
-
-
-later
------
-
 * Implement expand by expanding tiers (more robust and flexible).  It
   will allow extraction of constant values from tiers.  This will also make it
   easy to amend a Thy: do theorization; add a bunch of atoms; do it again;
 
-* make regex work on qs1 and qs2.
 
-* check if equivalences (==) are congruences (s == s' ==> f s == f s')
-
-
-stranger things
----------------
+stranger things (bugs?)
+-----------------------
 
 * after adding:
 
@@ -123,6 +97,14 @@
 Later Later
 -----------
 
+* check if equivalences (==) are congruences (s == s' ==> f s == f s')
+
+* automatically detect and use orders.  algorithm sketch:
+  1. list everything of the type a -> a -> Bool
+  2. check and filter everything that is an order
+  3. parameterize semiTheoryFromEtc so that it takes an order re-run for
+     several different types
+
 * improve performance of inequality generation by using the following
   algorithm:
 
@@ -143,8 +125,6 @@
 
 * improve error message for missing typeInfo.  Maybe add full suggestion.
 
-* include Colin's list module example
-
 * (for performance and interface): actually compute what happens with
   undefined values.  e.g.: head [] == undefined.  This will/may make things
   faster as we can prune foo (head []) or head [] ++ head [], which are also
@@ -156,8 +136,6 @@
   testing x + y = y + x.  The second needs to hold for the first to hold.  And,
   it will be far more common!
 
-* (for performance) hardcode laws about `<=`, `<` and `==`?  nah!
-
 * (for interface) I actually do not need to provide 0-argument constants in the
   background algebra.  Since I am using an enumerative strategy, I can actually
   enumerate those from `Instances`.  This way, background will look nicer,
@@ -171,10 +149,6 @@
   I think it can be composed.  Just make everything in the list "smaller" than
   whatever is not in the list.
 
-* (for performance) This one is a maybe.  When generating preconditions, do not
-  consider (<=), only consider (<), because I can always weaken the
-  precondition later.  (update: nah!)
-
 * (performance) Improve the performance of KBCompletion.
   In the process of generating equivalences, the slowest function is complete,
   accounting for 88 percent of runtime.  Of that:
@@ -195,21 +169,3 @@
 
 * require _some_ cases of `e1 == e2` before considering `ce ==> e1 == e2`.
   10% by default?
-
-
-### Properties I want
-
-From:
-	1. `             i <= abs i   `
-	2. `negate (abs i) <= negate i`
-Remove 2 because of:
-	3.  `x < y  ==>  negate y < negate x`
-
-In the list example, I want:
-	* ` x <  y    ==>      x:xs <  y:ys`
-	* `xs <  ys   ==>      x:xs <  x:ys`
-
-In the graph, instead of:
-	1. `isNode x (addNode y emptyDigraph) == isNode y (addNode x emptyDigraph)`
-have:
-    2. `x /= y ==> isNode x (addNode y emptyDigraph) == False`
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.2.7
+version:             0.2.8
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -31,7 +31,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.2.7
+  tag:             v0.2.8
 
 
 library
@@ -53,8 +53,8 @@
                  , Test.Speculate.CondReason
                  , Test.Speculate.Sanity
                  , Test.Speculate.Misc
-  other-modules:   Test.Speculate.Utils
-                 , Test.Speculate.Utils.Class
+                 , Test.Speculate.Utils
+  other-modules:   Test.Speculate.Utils.Class
                  , Test.Speculate.Utils.Colour
                  , Test.Speculate.Utils.Digraph
                  , Test.Speculate.Utils.List
@@ -71,17 +71,89 @@
   hs-source-dirs:    src
   default-language:  Haskell2010
 
+test-suite creason
+  main-is:           test-creason.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite engine
+  main-is:           test-engine.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite eval
+  main-is:           test-eval.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
 test-suite expr
-  type:                exitcode-stdio-1.0
-  main-is:             test-expr.hs
-  other-modules:       Test
-  hs-source-dirs:      src, tests
-  build-depends: base >= 4 && < 5, leancheck, cmdargs, containers
-  default-language:    Haskell2010
+  main-is:           test-expr.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
 
+test-suite match
+  main-is:           test-match.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite misc
+  main-is:           test-misc.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite order
+  main-is:           test-order.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite reason
+  main-is:           test-reason.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+test-suite utils
+  main-is:           test-utils.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
 benchmark plus-abs
   main-is:           plus-abs.hs
-  build-depends: base >= 4 && < 5, leancheck, cmdargs, containers
-  hs-source-dirs:    src, eg
+  hs-source-dirs:    eg
+  build-depends:     base >= 4 && < 5, speculate
+  default-language:  Haskell2010
+  type:              exitcode-stdio-1.0
+
+benchmark test-stats
+  main-is:           test-stats.hs
+  other-modules:     Test
+  hs-source-dirs:    tests
+  build-depends:     base >= 4 && < 5, leancheck, speculate
   default-language:  Haskell2010
   type:              exitcode-stdio-1.0
diff --git a/src/Test/Speculate/Expr/Core.hs b/src/Test/Speculate/Expr/Core.hs
--- a/src/Test/Speculate/Expr/Core.hs
+++ b/src/Test/Speculate/Expr/Core.hs
@@ -36,6 +36,8 @@
   , isSub
   , hasVar
   , unfoldApp
+  , isTuple
+  , unfoldTuple
   , isConstantNamed
 
   -- * Properties of expressions
@@ -160,20 +162,10 @@
     '[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs
     cs -> showParen (d > prec ":")
         $ showsOpExpr ":" e1 . showString ":" . showString cs
-showsPrecExpr d ((Constant "," _ :$ e1) :$ e2) =
-    showString "(" . showsPrecExpr 0 e1
-  . showString "," . showsPrecExpr 0 e2
-  . showString ")"
-showsPrecExpr d (((Constant ",," _ :$ e1) :$ e2) :$ e3) =
-    showString "(" . showsPrecExpr 0 e1
-  . showString "," . showsPrecExpr 0 e2
-  . showString "," . showsPrecExpr 0 e3
-  . showString ")"
-showsPrecExpr d ((((Constant ",,," _ :$ e1) :$ e2) :$ e3) :$ e4) =
-    showString "(" . showsPrecExpr 0 e1
-  . showString "," . showsPrecExpr 0 e2
-  . showString "," . showsPrecExpr 0 e3
-  . showString "," . showsPrecExpr 0 e4
+showsPrecExpr d ee | isTuple ee = id
+    showString "("
+  . foldr1 (\s1 s2 -> s1 . showString "," . s2)
+           (showsPrecExpr 0 `map` unfoldTuple ee)
   . showString ")"
 showsPrecExpr d ((Constant f _ :$ e1) :$ e2)
   | isInfix f = showParen (d > prec f)
@@ -191,6 +183,17 @@
                            $ showsPrecExpr (prec " ") e1
                            . showString " "
                            . showsPrecExpr (prec " " + 1) e2
+-- TODO: the above show instance is getting big.  Move it into a separate file?
+
+isTuple :: Expr -> Bool
+isTuple = not . null . unfoldTuple
+
+unfoldTuple :: Expr -> [Expr]
+unfoldTuple = u . unfoldApp
+  where
+  u (Constant cs _:es) | not (null es) && cs == replicate (length es - 1) ','
+                       = es
+  u _   = []
 
 -- bad smell here, repeated code!
 showsTailExpr :: Expr -> String -> String
diff --git a/src/Test/Speculate/Utils.hs b/src/Test/Speculate/Utils.hs
--- a/src/Test/Speculate/Utils.hs
+++ b/src/Test/Speculate/Utils.hs
@@ -7,6 +7,10 @@
 -- This module is part of Speculate.
 --
 -- Exports utility functions of all utils sub-modules.
+--
+-- This is not intended to be used by users of Speculate, only by modules of
+-- Speculate itself.  Expect symbols exported here to come and go with every
+-- minor version.
 module Test.Speculate.Utils
   ( module Test.Speculate.Utils.Misc
   , module Test.Speculate.Utils.PrettyPrint
diff --git a/tests/Test.hs b/tests/Test.hs
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -42,10 +42,10 @@
   --   Operators are surrounded by dashes.
 
   -- ** Integers
-  , zero, one, two, minusOne, minusTwo
+  , zero, one, two, three, minusOne, minusTwo
   , xx, yy, zz, xx'
   , id', abs'
-  , (-+-), (-*-), (.-.), (-.-)
+  , (-+-), (-*-), (.-.)
   , ii, jj, kk, ii'
   , negate'
   , ff, gg
@@ -53,6 +53,12 @@
   , succ'
   , (-$-)
 
+  , (-|-), pair, duple -- synonyms
+  , triple
+  , quadruple
+  , quintuple
+  , sixtuple
+
   , idE
   , absE
   , succE
@@ -288,6 +294,9 @@
 two :: Expr
 two = showConstant (2 :: Int)
 
+three :: Expr
+three = showConstant (3 :: Int)
+
 minusOne :: Expr
 minusOne = showConstant (-1 :: Int)
 
@@ -349,11 +358,37 @@
 minusE :: Expr
 minusE = constant "-" ((-) :: Int -> Int -> Int)
 
-(-.-) :: Expr -> Expr -> Expr
-e1 -.- e2 = commaE :$ e1 :$ e2
+(-|-) :: Expr -> Expr -> Expr
+e1 -|- e2 = commaE :$ e1 :$ e2
 
 commaE :: Expr
 commaE = constant "," ((,) :: Int -> Int -> (Int,Int))
+
+pair :: Expr -> Expr -> Expr
+pair = (-|-)
+
+duple :: Expr -> Expr -> Expr
+duple = (-|-)
+
+triple :: Expr -> Expr -> Expr -> Expr
+triple e1 e2 e3 = ccE :$ e1 :$ e2 :$ e3
+  where
+  ccE = constant ",," ((,,) :: Int -> Int -> Int -> (Int,Int,Int))
+
+quadruple :: Expr -> Expr -> Expr -> Expr -> Expr
+quadruple e1 e2 e3 e4 = cccE :$ e1 :$ e2 :$ e3 :$ e4
+  where
+  cccE = constant ",,," ((,,,) :: Int -> Int -> Int -> Int -> (Int,Int,Int,Int))
+
+quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr
+quintuple e1 e2 e3 e4 e5 = ccccE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5
+  where
+  ccccE = constant ",,,," ((,,,,) :: Int -> Int -> Int -> Int -> Int -> (Int,Int,Int,Int,Int))
+
+sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr
+sixtuple e1 e2 e3 e4 e5 e6 = cccccE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5 :$ e6
+  where
+  cccccE = constant ",,,,," ((,,,,,) :: Int -> Int -> Int -> Int -> Int -> Int -> (Int,Int,Int,Int,Int,Int))
 
 (-$-) :: Expr -> Expr -> Expr
 e1 -$- e2 = applyE :$ e1 :$ e2
diff --git a/tests/test-creason.hs b/tests/test-creason.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-creason.hs
@@ -0,0 +1,61 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.CondReason
+
+-- Utils
+import Test.Speculate.Reason (canonicalEqn, canonicalizeEqn, emptyThy)
+import Test.Speculate.Expr (falseE)
+
+main :: IO ()
+main = mainTest tests 10000
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+
+  , creductions1 (zero -<=- yy) (yy -+- abs' yy) (zero -<=- xx, abs' xx, xx)
+    == [yy -+- yy]
+
+  , creductions1 (zero -<=- yy) (abs' yy -+- abs' yy) (zero -<=- xx, abs' xx, xx)
+    == [yy -+- abs' yy, abs' yy -+- yy]
+
+  , cnormalize
+      emptyChy{cequations = [(zero -<=- xx, abs' xx, xx)]}
+      (zero -<=- yy) (abs' yy -+- abs' yy)
+    == yy -+- yy
+
+  , not
+  $ cequivalent
+      emptyChy{cequations = []}
+      (zero -<=- yy) (abs' yy -+- yy) (yy -+- yy)
+
+  , cequivalent
+      emptyChy{cequations = [(zero -<=- xx, abs' xx, xx)]}
+      (zero -<=- yy) (abs' yy -+- yy) (yy -+- yy)
+
+  , holds n $ \e1 e2    -> canonicalCEqn compare (falseE,e1,e2) == canonicalEqn emptyThy (e1,e2)
+  , holds n $ \e1 e2    -> sndTrd (canonicalizeCEqn compare (falseE,e1,e2))
+                        == canonicalizeEqn emptyThy (e1,e2)
+  , holds n $ \e1 e2 ce -> sndTrd (canonicalizeCEqn compare (falseE,e1,e2))
+                        == sndTrd (canonicalizeCEqn compare (ce,    e1,e2))
+
+  , const True -- TODO: make the following test pass!
+  $ let chy = cinsert ( elem' xx xxs
+                      , insert' xx (xxs -++- yys)
+                      , insert' xx xxs -++- yys
+                      )
+                      emptyChy
+    in cnormalize chy (elem' xx xxs) (insert' xx (xxs -++- yys)) == insert' xx xxs -++- yys
+
+  , const True -- TODO: make the following test pass!
+  $ creductions1 (elem' xx xxs) (insert' xx (xxs -++- yys))
+      ( elem' xx xxs, insert' xx (xxs -++- yys), insert' xx xxs -++- yys)
+    == [insert' xx xxs -++- yys]
+
+  , const True -- TODO: make the following test pass!
+  $ holds n $ \(BoolE ce) (SameTypeE e1 e2) -> creductions1 ce e1 (ce,e1,e2) == [e2]
+  ]
+  where
+  sndTrd (_,y,z) = (y,z)
diff --git a/tests/test-engine.hs b/tests/test-engine.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-engine.hs
@@ -0,0 +1,87 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.Engine
+
+-- Helper functions
+import Test.Speculate.Reason (emptyThy)
+import Test.Speculate.Utils
+import Data.List
+import Data.Maybe
+
+main :: IO ()
+main = mainTest tests 10000
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+  
+  , tiersExprTypeCorrect (n*2)
+
+  , holds n $ \e -> mostGeneral  e == head (vassignments e)
+  , holds n $ \e -> mostSpecific e == last (vassignments e)
+
+  , vassignments (zero -+- xx) == [zero -+- xx]
+  , vassignments (zero -+- i_) == [zero -+- xx]
+  , vassignments (i_ -+- i_) == [xx -+- yy, xx -+- xx]
+  , map canonicalize (vassignments (i_ -+- (i_ -+- ord' c_)))
+    == [ xx -+- (yy -+- ord' cc)
+       , xx -+- (xx -+- ord' cc) ]
+
+  , vassignments (ii -+- i_) == [ii -+- xx]
+  , map canonicalize (vassignments ((i_ -+- i_) -+- (ord' c_ -+- ord' c_)))
+    == [ (xx -+- yy) -+- (ord' cc -+- ord' dd)
+       , (xx -+- yy) -+- (ord' cc -+- ord' cc)
+       , (xx -+- xx) -+- (ord' cc -+- ord' dd)
+       , (xx -+- xx) -+- (ord' cc -+- ord' cc) ]
+
+  , holds n $ \e -> all (null . snd) (vars e)
+                ==> let xs = map (length . vars) $ vassignments e
+                    in (head xs >) `all` tail xs
+                    && (last xs <) `all` init xs
+  , holds n $ \e -> all null (map snd $ vars e)
+                ==> unrepeatedVars (head (vassignments e))
+  , holds n $ \e -> all (null . snd) (vars e)
+                ==> let es = vassignments e
+                    in (`isInstanceOf` head es) `all` tail es
+                    && (last es `isInstanceOf`) `all` init es
+  , holds n $ \e -> allLater (\e1 e0 -> not (e0 `isInstanceOf` e1))
+                  $ vassignments e
+  , holds n $ \e -> let es = vassignments e
+                    in length (nub (sort es)) == length es
+  , holds n $ \e -> length (vassignments e)
+                 == product (map (bell . snd) . counts $ holes e)
+
+  , equivalencesBetween (===) (i_ -+- i_) (i_ -+- i_)
+    == [ ( xx -+- yy, yy -+- xx ) ]
+
+  , equivalencesBetween (===) (i_ -+- (i_ -+- i_)) ((i_ -+- i_) -+- i_)
+    == [ ( xx -+- (yy -+- zz), (xx -+- yy) -+- zz )
+       , ( xx -+- (yy -+- zz), (xx -+- zz) -+- yy )
+       , ( xx -+- (yy -+- zz), (yy -+- xx) -+- zz )
+       , ( xx -+- (yy -+- zz), (yy -+- zz) -+- xx )
+       , ( xx -+- (yy -+- zz), (zz -+- xx) -+- yy )
+       , ( xx -+- (yy -+- zz), (zz -+- yy) -+- xx ) ]
+
+  , holds n $ \(SameTypeE e1 e2) -> unEquation (phonyEquation e1 e2) == (e1,e2)
+
+-- TODO: make the following pass (add ValueE and SameTypeValueE to Test)
+--, holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4)
+--         -> subConsequence emptyThy (e1 -==- e2) e3 e4
+--         == subConsequence emptyThy (e2 -==- e1) e3 e4
+--, holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4)
+--         -> subConsequence emptyThy (e1 -==- e2) e3 e4
+--         == subConsequence emptyThy (e1 -==- e2) e4 e3
+--, holds n $ \...
+--         -> not $ subConsequence emptyThy (e1 -<=- e2) e3 e4
+  ,       subConsequence emptyThy [] (xx -==- yy) (xx -+- yy) (xx -+- xx)
+  , not $ subConsequence emptyThy [] (xx -<=- yy) (xx -+- yy) (xx -+- xx)
+  ,       subConsequence emptyThy [(xx -<=- yy, [xx -==- yy])]
+                                     (xx -<=- yy) (xx -+- yy) (xx -+- xx)
+  ,       subConsequence emptyThy [] (abs' xx -==- abs' yy) (abs' xx) (abs' yy)
+  , not $ subConsequence emptyThy [] (abs' xx -<=- abs' yy) (abs' xx) (abs' yy)
+  , not $ subConsequence emptyThy [] (abs' xx -==- one) (xx -+- abs' xx) zero
+  ]
+  where
+  x === y = equal preludeInstances 1000 x y
diff --git a/tests/test-eval.hs b/tests/test-eval.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-eval.hs
@@ -0,0 +1,53 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.Expr.Ground
+import Test.Speculate.Utils
+import Test.Speculate.Expr
+
+import Data.Maybe
+
+-- TODO: rename test-eval to test-ground
+
+main :: IO ()
+main = mainTest tests 10000
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+
+  , holds n' $ \e -> if isEqE preludeInstances e
+                      then e === e
+                      else e =/= e
+  ,                                    xx -+- yy === yy -+- xx
+  , holds n' $ \(IntE e1) (IntE e2) -> e1 -+- e2 === e2 -+- e1
+  ,                                    xx -+- yy =/= xx -+- xx
+  ,                                      abs' xx === abs' (abs' xx)
+  ,                      abs' (xx -+- abs' xx) === (xx -+- abs' xx) -- 2*x or 0
+  , holds n' $ \e1 e2 -> typ e1 /= typ e2 ==> e1 =/= e2
+
+  , holds n' $       zero //= one
+  , holds n' $ not $   xx //= yy
+
+  , holds n' $ \e1 e2 -> case equation preludeInstances e1 e2 of
+                           Just e1e2 -> condEqual preludeInstances 500 e1e2 e1 e2
+                           Nothing   -> True
+  , holds n' $ \e1 e2 -> case equation preludeInstances e1 e2 of
+                           Just e1e2 -> condEqualM preludeInstances 500 0 e1e2 e1 e2
+                           Nothing   -> True
+  , fails n' $ \e1 e2 -> case equation preludeInstances e1 e2 of
+                           Just e1e2 -> condEqualM preludeInstances 500 500 e1e2 e1 e2
+                           Nothing   -> True
+
+  , trueBinds preludeInstances 500 (xx -==- zero) == [[("x",zero)]]
+  , trueBinds preludeInstances 500 (xx -==- one)  == [[("x",one)]]
+  , trueBinds preludeInstances 500 ((xx -==- one) -&&- (yy -==- zero))  == [[("x",one),("y",zero)]]
+  ]
+  where
+  n' = n `div` 50
+  x === y = equal preludeInstances 500 x y
+  infix 4 ===
+  x =/= y = not (x === y)
+  infix 4 =/=
+  x //= y = inequal preludeInstances 500 x y
diff --git a/tests/test-expr.hs b/tests/test-expr.hs
--- a/tests/test-expr.hs
+++ b/tests/test-expr.hs
@@ -197,6 +197,19 @@
 #endif
 -}
 
+  , holds n $ \(IntE e1) (IntE e2) -> isTuple (pair e1 e2)
+                                   && unfoldTuple (pair e1 e2) == [e1,e2]
+  , holds n $ \(IntE e1) (IntE e2) (IntE e3) ->
+      isTuple (triple e1 e2 e3) && unfoldTuple (triple e1 e2 e3) == [e1,e2,e3]
+  , holds n $ \(IntE e1) (IntE e2) (IntE e3) (IntE e4) ->
+      isTuple (quadruple e1 e2 e3 e4) &&
+      unfoldTuple (quadruple e1 e2 e3 e4) == [e1,e2,e3,e4]
+  , holds n $ \(IntE  e) -> not (isTuple e) && unfoldTuple e == []
+  , holds n $ \(CharE e) -> not (isTuple e) && unfoldTuple e == []
+  , holds n $ \(BoolE e) -> not (isTuple e) && unfoldTuple e == []
+  , holds n $ \(ListE e) -> not (isTuple e) && unfoldTuple e == []
+  , holds n $ \(FunE  e) -> not (isTuple e) && unfoldTuple e == []
+
   , holds n $ \e1 e2 -> e1 `isSub` e2 == (e1 `elem` subexprsV e2)
 
   , show (emptyString) == "\"\" :: [Char]"
@@ -215,8 +228,12 @@
   , show (one -+- one)           == "1 + 1 :: Int"
   , show (minusOne -+- minusOne) == "(-1) + (-1) :: Int"
 
-  , show (zero -.- one)          == "(0,1) :: (Int,Int)"
-  , show (minusOne -.- minusOne) == "(-1,-1) :: (Int,Int)"
+  , show (zero -|- one)          == "(0,1) :: (Int,Int)"
+  , show (minusOne -|- minusOne) == "(-1,-1) :: (Int,Int)"
+  , show (triple zero one two)   == "(0,1,2) :: (Int,Int,Int)"
+  , show (quadruple minusOne zero one two) == "(-1,0,1,2) :: (Int,Int,Int,Int)"
+  , show (quintuple minusOne zero one two three) == "(-1,0,1,2,3) :: (Int,Int,Int,Int,Int)"
+  , show (sixtuple minusTwo minusOne zero one two three) == "(-2,-1,0,1,2,3) :: (Int,Int,Int,Int,Int,Int)"
 
   , show (one -:- ll)                     == "[1] :: [Int]"
   , show (zero -:- one -:- ll)            == "[0,1] :: [Int]"
diff --git a/tests/test-match.hs b/tests/test-match.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-match.hs
@@ -0,0 +1,92 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.Expr.Match
+import Test.Speculate.Expr
+
+-- Helper functions
+import Test.Speculate.Utils
+import Data.List
+import Data.Maybe
+import Data.Functor ((<$>)) -- for GHC < 7.10
+
+main :: IO ()
+main = mainTest tests 10000
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+
+  , holds n $ \(IntE e1) (IntE e2) -> match (e1 -+- e2) (xx -+- yy) == Just [("y",e2),("x",e1)]
+  , holds n $ \(IntE e)            -> match (e -+- e)   (xx -+- xx) == Just [("x",e)]
+  , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> match (e1 -+- e2) (xx -+- xx) == Nothing
+  , holds n $ \(IntE e1) (IntE e2) (IntE e3) -> e2 /= e3
+                ==> match ((e1 -+- e1) -+- (e2 -+- e3)) (xx -+- (yy -+- yy)) == Nothing
+  , holds n $ \(IntE e1) (IntE e2) -> matchWith [("x",e1)] (e1 -+- e2) (xx -+- yy) == Just [("y",e2),("x",e1)]
+  , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> matchWith [("x",e2)] (e1 -+- e2) (xx -+- yy) == Nothing
+  , holds n $ \e1 e2 -> e1 `match` e2 == matchWith [] e1 e2
+  , holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4) ->
+                not (isFunTy $ typ e1) && not (isFunTy $ typ e3)
+                  ==>
+                (e1 -==- e2) `match` (e3 -==- e4) == (e1,e2) `match2` (e3,e4)
+
+
+  , assign "y" (yy -+- zz) ((xx -+- yy) -+- (yy -+- zz))
+      == (xx -+- (yy -+- zz)) -+- ((yy -+- zz) -+- zz)
+
+  , ((xx -+- yy) -+- (yy -+- zz)) `assigning` [("y",yy -+- zz)]
+      == (xx -+- (yy -+- zz)) -+- ((yy -+- zz) -+- zz)
+
+  , (xx -+- yy) `assigning` [("y",yy -+- zz),("x",xx -+- yy)]
+      == (xx -+- yy) -+- (yy -+- zz)
+
+  , sub (xx -+- yy) zero ((xx -+- yy) -+- zz) == (zero -+- zz)
+  , sub (xx -+- yy) zero (xx -+- (yy -+- zz)) == (xx -+- (yy -+- zz))
+
+  , holds n $ \(SameTypeE e1 e2) -> sub e1 e2 e1 == e2
+  , holds n $ \(IntE e1) (IntE e2) -> sub e1 e2 (e1 -+- e1) == (e2 -+- e2)
+
+  , holds  n $ \(SameTypeE e1 e2) -> unify e1 e2 =$ fmap canonicalize $= unify e2 e1
+
+  , unification xx yy == Just [("x",yy)]
+  , (canonicalize <$> unify xx yy) == Just xx
+  , unification zero zero == Just []
+  , unification zero one  == Nothing
+  , unification xx one == Just [("x",one)]
+  , unification (zero -+- xx) (zero -+- one) == Just [("x",one)]
+  , unification (zero -+- xx) (yy -+- one) == Just [("x",one),("y",zero)]
+  , unify (zero -+- xx) (yy -+- one) == Just (zero -+- one)
+  , unification (ff xx) (ff (gg yy)) == Just [("x",gg yy)]
+  , unification (ff xx -+- xx) (yy -+- zero) == Just [("x",zero),("y",ff zero)]
+  , unify (ff xx -+- xx) (yy -+- zero) == Just (ff zero -+- zero)
+  , unification (ff xx) (gg yy) == Nothing
+  , unification (ff xx) (ff yy) == unification xx yy
+  , (canonicalize <$> unify (negate' (negate' xx) -+- yy) (zz -+- zero))
+    == Just (negate' (negate' xx) -+- zero)
+  , unification (xx -+- one) (one -+- xx) == Just [("x",one)]
+  , unification (xx -+- xx) (one -+- one) == Just [("x",one)]
+  , unification (zz -+- zz) (xx -+- yy) == Just [("x",yy),("z",yy)]
+  , unification (xx    -*- (-+-) xx xx)
+                (ff zz -*- (-+-) xx yy) == Just [("y",ff zz),("x",ff zz)]
+
+  -- The following two tests are adapted from Baader and Snyder:
+  -- Example 2.8, Chapter 8, Handbook of Automated Reasoning (page 453).
+  , unification (hh5 yy zz (ff2 ii ii) (ff2 jj jj) kk) (hh5 (ff2 xx xx) (ff2 yy yy) jj kk zz)
+    == Just [ ("i",xx)
+            , ("k",ff2 (ff2 xx xx) (ff2 xx xx))
+            , ("j",ff2 xx xx)
+            , ("z",ff2 (ff2 xx xx) (ff2 xx xx))
+            , ("y",ff2 xx xx)
+            ]
+  , unification (hh7 yy zz xx' (ff2 ii ii) (ff2 jj jj) (ff2 kk kk) ii')
+                (hh7 (ff2 xx xx) (ff2 yy yy) (ff2 zz zz) jj kk ii' xx')
+    == Just [ ("i",xx)
+            , ("i'",ff2 (ff2 (ff2 xx xx) (ff2 xx xx)) (ff2 (ff2 xx xx) (ff2 xx xx)))
+            , ("k",ff2 (ff2 xx xx) (ff2 xx xx))
+            , ("j",ff2 xx xx)
+            , ("x'",ff2 (ff2 (ff2 xx xx) (ff2 xx xx)) (ff2 (ff2 xx xx) (ff2 xx xx)))
+            , ("z",ff2 (ff2 xx xx) (ff2 xx xx))
+            , ("y",ff2 xx xx)
+            ]
+  ]
diff --git a/tests/test-misc.hs b/tests/test-misc.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-misc.hs
@@ -0,0 +1,91 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.Misc
+
+-- Utils
+import Test.Speculate.Expr
+import Test.Speculate.Utils
+
+main :: IO ()
+main = mainTest tests 10000
+
+-- NOTE: remember that in the expressions returned by functions<N> the
+-- variables are actually values (bound by the arguments of the returned
+-- function)
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+  , fillings (ord' c_) [cc,dd,xx] == [ord' cc, ord' dd]
+
+  , map (show *** ($1))                  (functions1 (i_ -+- i_) :: [(Expr,Int->Int)])
+    == [("x + x :: Int", 2)]
+
+  , map (show *** (($1).($2)))           (functions2 (i_ -+- i_) :: [(Expr,Int->Int->Int)])
+    == [ ("x + x :: Int", 4)
+       , ("x + y :: Int", 3)
+       , ("y + x :: Int", 3)
+       , ("y + y :: Int", 2) ]
+
+  , map (show *** (($1).($2).($3)))      (functions3 (i_ -+- i_) :: [(Expr,Int->Int->Int->Int)])
+    == [ ("x + x :: Int",6)
+       , ("x + y :: Int",5)
+       , ("y + x :: Int",5)
+       , ("x + z :: Int",4)
+       , ("y + y :: Int",4)
+       , ("z + x :: Int",4)
+       , ("y + z :: Int",3)
+       , ("z + y :: Int",3)
+       , ("z + z :: Int",2) ]
+
+  , map (show *** (($1).($2).($3).($4))) (functions4 (i_ -+- i_) :: [(Expr,Int->Int->Int->Int->Int)])
+    == [ ("x + x :: Int",8)
+       , ("x + y :: Int",7)
+       , ("y + x :: Int",7)
+       , ("x + z :: Int",6)
+       , ("y + y :: Int",6)
+       , ("z + x :: Int",6)
+       , ("x + w :: Int",5)
+       , ("y + z :: Int",5)
+       , ("z + y :: Int",5)
+       , ("w + x :: Int",5)
+       , ("y + w :: Int",4)
+       , ("z + z :: Int",4)
+       , ("w + y :: Int",4)
+       , ("z + w :: Int",3)
+       , ("w + z :: Int",3)
+       , ("w + w :: Int",2) ]
+
+  , take 3 (expressionsOf [ zero, xx, absE, plusE ])
+    == [ [ zero, xx, absE, plusE ]
+       , [ abs' zero, abs' xx, plusE :$ zero, plusE :$ xx ]
+       , [ abs' (abs' zero)
+         , abs' (abs' xx)
+         , plusE :$ abs' zero
+         , plusE :$ abs' xx
+         , zero -+- zero
+         , zero -+- xx
+         , xx -+- zero
+         , xx -+- xx ] ]
+
+  , take 3 (valuedExpressionsOf [ zero, one, absE, plusE ])
+    == [ [ (zero, 0 :: Int)
+         , (one,  1) ]
+       , [ (abs' zero, 0)
+         , (abs' one,  1) ]
+       , [ (abs' (abs' zero), 0)
+         , (abs' (abs' one),  1)
+         , (zero -+- zero, 0)
+         , (zero -+- one,  1)
+         , (one -+- zero,  1)
+         , (one -+- one,   2) ] ]
+
+  , take 3 (mapT (id *** ($ (10::Int))) $ valuedExpressionsOf [ zero, one, absE, plusE ])
+    == [ [ (absE, 10 :: Int) ]
+       , [ (plusE :$ zero, 10)
+         , (plusE :$ one,  11) ]
+       , [ (plusE :$ abs' zero, 10)
+         , (plusE :$ abs' one,  11) ] ]
+  ]
diff --git a/tests/test-order.hs b/tests/test-order.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-order.hs
@@ -0,0 +1,91 @@
+import Test
+import Test.Speculate.Utils
+
+import Test.Speculate.Expr
+import Test.Speculate.Reason.Order
+
+main :: IO ()
+main = do
+  n <- getMaxTestsFromArgs 10000
+
+  reportTests (tests n)
+
+
+tests :: Int -> [Bool]
+tests n =
+  [ True -- see test-expr.hs for general Expr orders
+
+  , holds n $ simplificationOrder (|>|)
+  , holds n $ simplificationOrder ( >|)
+  , holds n $ simplificationOrder (|> )
+  , holds n $ simplificationOrder (dwoBy (<))
+
+  , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 |>  e2)
+  , fails n $ \e1 e2 -> (e1 |>| e2) == (e1  >| e2)
+  , fails n $ \e1 e2 -> (e1 |>  e2) == (e1  >| e2)
+
+  , not $ zero |> xx
+  , not $ xx |> zero
+  , negate' xx |> zero
+  , negate' xx -+- xx |> zero
+  , zero > xx
+  , negateE > zero
+
+  , weight xx                            == 1
+  , weight zero                          == 1
+  , weight (xx -+- zero)                 == 2
+  , weight (one -+- yy)                  == 2
+  , weight (xx -*- (yy -+- zz))          == 3
+  , weight ((xx -*- yy) -+- (xx -*- zz)) == 4
+  , holds n $ \e1 e2 -> weight (e1 -+- e2)  == weight e1 + weight e2
+  , holds n $ \e     -> weight (e -+- zero) == 1 + weight e
+  , holds n $ \e     -> weight (abs' e)     == 1 + weight e
+  , holds n $ \e     -> weightExcept absE (abs' e)    <= weight e
+  , holds n $ \e     -> weightExcept absE (negate' e) <= weight e + 1
+  , holds n $ \e     -> weightExcept absE (abs' e)    == weightExcept absE e
+  , holds n $ \e     -> weightExcept absE (negate' e) == weightExcept absE e + 1
+
+  -- lexicompare is compatible (almost as if by coincidence)
+  , fails n $ simplificationOrder lgt
+  , holds n $ compatible          lgt
+  , fails n $ closedUnderSub      lgt
+  , fails n $ subtermProperty     lgt
+
+  -- compareComplexity has the subtermProperty
+  , fails n $ simplificationOrder cgt
+  , fails n $ compatible          cgt
+  , fails n $ closedUnderSub      cgt
+  , holds n $ subtermProperty     cgt
+  ]
+  where
+  e1 `lgt` e2 = e1 `lexicompare` e2 == GT
+  e1 `cgt` e2 = e1 `compareComplexity` e2 == GT
+
+simplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+simplificationOrder (>) = \e1 e2 e3 -> reductionOrder  (>) e1 e2 e3
+                                    && subtermProperty (>) e1
+
+subtermProperty :: (Expr -> Expr -> Bool) -> Expr -> Bool
+subtermProperty (>) = \e -> all (e >)
+                          . filter (\e' -> e' /= e && typ e' == typ e)
+                          $ subexprs e -- isn't this subexprsV? I don't think so
+
+reductionOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+reductionOrder (>) = \e1 e2 e3 -> strictPartialOrder (>) e1 e2 e3
+                               && compatible         (>) e1 e2 e3
+                               && closedUnderSub     (>) e1 e2 e3
+
+compatible :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+compatible (>) = \e e1 e2 -> e1 > e2 && typ e1 == typ e2
+                         ==> and [ assign n e1 e > assign n e2 e
+                                 | (t,n) <- vars e
+                                 , t == typ e1
+                                 , t == typ e2 ]
+
+-- The formal definition contains multiple assignments,
+-- here, just a single variable is assigned.
+closedUnderSub :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
+closedUnderSub (>) = \e1 e2 e -> e1 > e2
+                             ==> and [ assign n e e1 > assign n e e2
+                                     | (t,n) <- vars e1 `nubMerge` vars e2
+                                     , t == typ e ]
diff --git a/tests/test-reason.hs b/tests/test-reason.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-reason.hs
@@ -0,0 +1,230 @@
+{-# LANGUAGE CPP #-}
+-- Test library
+import Test
+import Test.Speculate.Utils
+
+-- Functions under test
+import Test.Speculate
+import Test.Speculate.Expr
+import Test.Speculate.Reason
+import Test.Speculate.Reason.Order
+import Data.Tuple (swap)
+import Data.Function (on)
+import Data.List (sortBy,permutations)
+
+theorize' :: [(Expr,Expr)] -> Thy
+theorize' eqs = finalize $ foldl (flip insert) emptyThy {closureLimit = 3, keepE = keepMaxOf eqs} eqs
+
+theorize'' :: [(Expr,Expr)] -> Thy
+theorize'' eqs = finalize $ foldr insert emptyThy {closureLimit = 3, keepE = keepMaxOf eqs} eqs
+
+main :: IO ()
+main = do
+  n <- getMaxTestsFromArgs 10000
+
+  reportTests (tests n)
+
+  putStrLn "\nlength (rules $ theorize eqs)"
+  reportCountsBy (\(SameTypedPairsE eqs) -> show . length . rules $ theorize eqs)
+                 (take n list)
+
+  putStrLn "length (equations $ theorize eqs)"
+  reportCountsBy (\(SameTypedPairsE eqs) -> show . length . equations $ theorize eqs)
+                 (take n list)
+
+  putStrLn "\\e1 e2 e3 -> e1 > e2 && typ e1 == typ e2,  length (vars e3)"
+  reportCountsBy (\(e1,e2,e3) -> if e1 > e2 && typ e1 == typ e2
+                                   then "OK, length " ++ show (length $ vars e3)
+                                   else "Not OK")
+                 (take n list)
+
+  putStrLn "\\e e1 e2 -> length $ reductions 1 e (e1,e2)"
+  reportCountsBy (\(e,e1,e2) -> if e1 > e2 && typ e1 == typ e2
+                                  then "OK, length " ++ show (length $ reductions1 e (e1,e2))
+                                  else "Not OK")
+                 (take n list)
+
+(~~) :: Expr -> Expr -> (Expr,Expr)
+(~~) = (,)
+infix 4 ~~
+
+mkThy :: [(Expr,Expr)] -> [(Expr,Expr)] -> Thy
+mkThy rs eqs = emptyThy
+             { rules     = rs
+             , equations = eqs }
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+
+  -- Listable Thy sound and complete:
+  , holds n $ okThy
+  , all (`elem` take n list) (take (n`div`10) listThyInefficient)
+
+  , holds n $ \(SameTypedPairsE eqs) -> theorize eqs == theorize (map swap eqs)
+  , holds n $ \(SameTypedPairsE eqs) -> theorize eqs == theorize (reverse eqs)
+
+  , holds n $ \(SameTypedPairsE eqs) -> theorize'  eqs == theorize eqs
+  , holds n $ \(SameTypedPairsE eqs) -> theorize'' eqs == theorize eqs
+
+  , holds n $ okThy . deduce
+  , holds n $ idempotent deduce
+  , holds n $ \thy -> ((>=) `on` length . equations) (deduce thy) thy
+  , holds n $ \thy -> ((==) `on` rules)              (deduce thy) thy
+
+  , holds n $ okThy . simplify
+  , holds n $ idempotent simplify
+  , holds n $ \thy -> ((<=) `on` length . equations) (simplify thy) thy
+  , holds n $ \thy -> ((==) `on` rules)              (simplify thy) thy
+
+  , holds n $ okThy . delete
+  , holds n $ idempotent delete
+  , holds n $ \thy -> ((<=) `on` length . equations) (delete thy) thy
+  , holds n $ \thy -> ((==) `on` rules)              (delete thy) thy
+
+  , holds n $ okThy . orient
+  , holds n $ idempotent orient
+  , holds n $ \thy -> ((<=) `on` length . equations) (orient thy) thy
+  , holds n $ \thy -> ((>=) `on` length . rules)     (orient thy) thy
+  , holds n $ \thy -> length (equations thy)      - length (equations $ orient thy)
+                   >= length (rules $ orient thy) - length (rules thy)
+
+  , holds n $ okThy . compose
+  , holds n $ idempotent compose
+  , holds n $ \thy -> ((<=) `on` length . rules)     (compose thy) thy
+  , holds n $ \thy -> ((==) `on` equations)          (compose thy) thy
+
+  , holds n $ okThy . collapse
+  , holds n $ idempotent collapse
+  , holds n $ \thy -> ((<=) `on` length . rules)     (collapse thy) thy
+  , holds n $ \thy -> ((>=) `on` length . equations) (collapse thy) thy
+
+  , holds n $ okThy . complete . unThyght
+
+  , holds n $ \(Thyght thy') (SameTypedPairsE eqs) ->
+                let thy = complete thy'
+                in  foldr insert thy eqs == complete (append thy eqs)
+
+  -- TODO: make the following pass with n `div` 10
+  -- Inference order should not matter:
+  , holds 100
+  $ \(Thyght thy) -> all (\steps -> iterateUntil (==) (chain steps) thy == complete thy)
+                   $ permutations [collapse, compose, orient, delete . simplify, deduce]
+  -- I now think the above property is not true in all cases, investigate.
+
+  -- NOTE: the following does not hold in general, only for most of the cases
+  , holds 4000
+  $ \(Thyght thy') (SameTypeE e1 e2) -> closureLimit thy' > 0 ==>
+       let thy = insert (e1,e2)
+               $ thy' { keepE = keepUpToLength (max (lengthE e1) (lengthE e2)) }
+       in  equivalent thy e1 e2
+
+  , holds n $ idempotent finalize
+
+  , criticalPairs emptyThy { rules = [ ((xx -+- yy) -+- zz,xx -+- (yy -+- zz))
+                                     , (negate' xx -+- xx, zero) ] }
+      == [ (negate' xx -+- (xx -+- yy),zero -+- yy)
+         , ((xx -+- (yy -+- zz)) -+- xx', (xx -+- yy) -+- (zz -+- xx')) ]
+
+  , criticalPairs emptyThy { rules = [ (negate' (negate' xx), id' xx) ] }
+      == [ (negate' (id' xx), id' (negate' xx)) ]
+
+  , criticalPairs emptyThy { canReduceTo = dwoBy (\e1 e2 -> e1 `lexicompare` e2 == GT)
+                           , rules = [ (ff (gg (ff xx)), xx)
+                                     , (ff (gg xx), gg (ff xx)) ] }
+      == (let sortuple (x,y) | x < y     = (y,x)
+                             | otherwise = (x,y)
+          in nubSort . map sortuple
+           $ [ (gg xx,                ff (gg (gg (ff xx))))
+             , (gg (ff xx),           ff (gg xx))
+             , (gg (ff (ff xx)),      xx)
+             , (gg (ff (ff (gg xx))), gg xx) ])
+
+  , criticalPairs emptyThy { rules = [ (ff (gg (ff xx)), xx)
+                                     , (ff (gg xx), gg (ff xx)) ] }
+      == [ (gg (ff xx),           ff (gg xx))
+         , (gg (ff (ff xx)),      xx)
+         , (ff (gg (gg (ff xx))), gg xx)
+         , (gg (ff (ff (gg xx))), gg xx) ]
+
+  , theorize [ (xx -*- yy) -*- (yy -*- zz)  ~~  yy ]
+    |==|
+    [ (xx -*- yy) -*- (yy -*- zz)  ~~  yy
+    , xx -*- ((xx -*- yy) -*- zz)  ~~  xx -*- yy
+    , (xx -*- (yy -*- zz)) -*- zz  ~~  yy -*- zz
+    ] `mkThy` []
+
+  , theorize [ xx -*- (yy -+- zz)  ~~  (xx -*- yy) -+- (xx -*- zz)
+             , (xx -+- yy) -*- zz  ~~  (xx -*- zz) -+- (yy -*- zz) ]
+    |==|
+    [ (xx -*- yy) -+- (xx -*- zz)  ~~  xx -*- (yy -+- zz)
+    , (xx -*- yy) -+- (zz -*- yy)  ~~  (xx -+- zz) -*- yy
+    ] `mkThy` [ (xx -+- xx) -*- yy  ~~  xx -*- (yy -+- yy) ]
+
+  , theorizeBy (|>|) [ xx -+- zero      ~~  xx
+                     , xx -+- succ' yy  ~~  succ' (xx -+- yy) ]
+    |==|
+    [ xx -+- zero  ~~  xx
+    ] `mkThy` [ xx -+- succ' yy  ~~  succ' (xx -+- yy) ]
+
+  , theorizeBy (kboBy weight (<))
+    [ xx -+- zero      ~~  xx
+    , xx -+- succ' yy  ~~  succ' (xx -+- yy) ]
+    |==|
+    [                 xx -+- zero  ~~  xx
+    , succ' (xx -+- yy)            ~~  xx -+- succ' yy
+    , xx -+-         succ' zero    ~~         succ' xx
+    , xx -+- (succ' (succ' zero))  ~~  succ' (succ' xx)
+    ] `mkThy` []
+
+  , theorizeBy (|>) [ xx -+- zero      ~~  xx
+                    , xx -+- succ' yy  ~~  succ' (xx -+- yy) ]
+    |==|
+    [ xx -+- zero      ~~  xx
+    , xx -+- succ' yy  ~~  succ' (xx -+- yy)
+    ] `mkThy` []
+
+  -- TODO: fix order under GHC <= 7.8
+#if __GLASGOW_HASKELL >= 800
+  , theorizeBy (dwoBy $ \e1 e2 -> if typ e1 == typ e2
+                                      then e1 > e2
+                                      else typ e1 < typ e2)
+    [ ( xx -+- zero, xx )
+    , ( xx -+- succ' yy, succ' (xx -+- yy) ) ]
+    |==|
+    [ ( xx -+- zero, xx )
+    , ( succ' (xx -+- yy), xx -+- (succ' yy) )
+    ] `mkThy` [ xx -+- (succ' zero)  ~~  succ' xx]
+#endif
+
+  , theorizeBy (|>) [ ( zero -+- xx, xx )
+                    , ( negate' xx -+- xx, zero )
+                    , ( (xx -+- yy) -+- zz, xx -+- (yy -+- zz) ) ]
+    |==| [ ( zero -+- xx                , xx )
+         , ( negate' xx -+- xx          , zero )
+         , ( (xx -+- yy) -+- zz         , xx -+- (yy -+- zz) )
+         , ( negate' xx -+- (xx -+- yy) , yy )
+         , ( xx -+- zero                , xx )
+         , ( xx -+- (negate' xx -+- yy) , yy )
+         , ( negate' (negate' xx)         , xx )
+         , ( negate' zero                 , zero )
+         , ( xx -+- negate' xx            , zero )
+         ] `mkThy` []
+
+  , theorizeBy (kboBy (weightExcept negateE) (gtExcept (>) negateE))
+      [ ( zero -+- xx, xx )
+      , ( negate' xx -+- xx, zero )
+      , ( (xx -+- yy) -+- zz, xx -+- (yy -+- zz) ) ]
+    |==| [ ( zero -+- xx                , xx )
+         , ( negate' xx -+- xx          , zero )
+         , ( (xx -+- yy) -+- zz         , xx -+- (yy -+- zz) )
+         , ( negate' xx -+- (xx -+- yy) , yy )
+         , ( negate' zero -+- xx        , xx )
+         , ( xx -+- zero                , xx )
+         , ( xx -+- (negate' xx -+- yy) , yy )
+         , ( negate' (negate' xx)         , xx )
+         , ( xx -+- negate' xx            , zero )
+         ] `mkThy` [( negate' zero, zero )]
+
+  -- TODO: restore tests losts after removing test-kbc
+  ]
diff --git a/tests/test-stats.hs b/tests/test-stats.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-stats.hs
@@ -0,0 +1,46 @@
+-- Test library
+import Test
+
+-- Helper
+import Data.Function (on)
+
+-- Functions under test
+import Test.Speculate
+import Test.Speculate.Expr
+import Test.Speculate.Reason
+import Test.Speculate.Utils
+
+main :: IO ()
+main = do
+  n <- getMaxTestsFromArgs 10000
+
+  putStrLn "typ (e :: Expr)"
+  reportCountsBy typ            (take n list :: [Expr])
+
+  putStrLn "lengthE (e :: Expr)"
+  reportCountsBy lengthInterval (take n list :: [Expr])
+
+  putStrLn "typ (e1 :: Expr) == typ (e2 :: Expr)"
+  reportCountsBy equalTypes (take n list)
+
+  putStrLn "typ (e1 :: Expr) == typ (e2 :: Expr)"
+  reportCountsBy equalTypes . map unSameTypeE . take n $ list
+
+  putStrLn "okThy thy"
+  reportCountsBy (show . okThy) (take n list)
+
+  putStrLn "length (equations thy)"
+  reportCountsBy (show . length . equations) (take n list)
+
+  putStrLn "length (rules thy)"
+  reportCountsBy (show . length . rules) (take n list)
+
+  putStrLn "length (equations thy + rules thy)"
+  reportCountsBy (show . length . (\thy -> rules thy ++ equations thy)) (take n list)
+
+lengthInterval :: Expr -> (Int,Int)
+lengthInterval e = (l, l+2) where l = (lengthE e `div` 3) * 3
+
+equalTypes :: (Expr,Expr) -> String
+equalTypes (e1,e2) | typ e1 == typ e2 = show (typ e1)
+                   | otherwise        = "invalid"
diff --git a/tests/test-utils.hs b/tests/test-utils.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-utils.hs
@@ -0,0 +1,129 @@
+-- Test library
+import Test
+
+-- Functions under test
+import Test.Speculate.Utils
+
+-- Helper functions
+import Data.List
+import Data.Function
+
+import Test.LeanCheck.Utils (comparison)
+
+main :: IO ()
+main = mainTest tests 10000
+
+tests :: Int -> [Bool]
+tests n =
+  [ True
+  
+  -- iss is sound
+  , and [ length xs == n     | m <- [0..5], n <- [0..5], xs <- iss m n ]
+  , and [ head (iss 0 n) == [0..(n-1)]    | n <- [0..10] ]
+  , and [ last (iss 0 n) == replicate n 0 | n <- [0..10] ]
+  , and [ firsts xs `isPrefixOf` [0..]    | n <- [0..10], xs <- iss 0 n ]
+  , holds 100 $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys
+                      ==> strictlyOrdered (nubMerge xs (ys::[Int]))
+  , and [ nubMerge xs xs == xs | n <- [0..10], let xs = [0..n] ]
+
+  , holds 100 $ \xss -> ordered . concat $ discardLaterT (<=) (xss::[[Int]])
+  , (length . concat $ discardLaterT (<=) [[1..100]]) == 100
+
+  , collectOn snd [(1,2),(2,2),(2,3),(3,3)] == [[(1,2),(2,2)],[(2,3),(3,3)]]
+  , collectOn fst [(1,2),(2,2),(2,3),(3,3)] == [[(1,2)],[(2,2),(2,3)],[(3,3)]]
+  , collectOn (uncurry (+)) [(1,2),(2,2),(2,3),(3,3)] == [[(1,2)],[(2,2)],[(2,3)],[(3,3)]]
+  , collectBy (compare `on` snd) [(1,2),(2,2),(2,3),(3,3)] == [[(1,2),(2,2)],[(2,3),(3,3)]]
+
+  , holds n $ \x           -> medianate (,) [x::Int]           == [(x,x)]
+  , holds n $ \x y         -> medianate (,) [x::Int,y]         == [(x,y)]
+  , holds n $ \x y z       -> medianate (,) [x::Int,y,z]       == [(x,z),(y,y)]
+  , holds n $ \x y z w     -> medianate (,) [x::Int,y,z,w]     == [(x,w),(y,z)]
+  , holds n $ \x y z w v   -> medianate (,) [x::Int,y,z,w,v]   == [(x,v),(y,w),(z,z)]
+  , holds n $ \x y z w v u -> medianate (,) [x::Int,y,z,w,v,u] == [(x,u),(y,v),(z,w)]
+
+  , all (\f -> discardOthers f [] == ([]::[Int])) [(<=),(>=),(<),(>),(==),(/=),\x y -> True]
+  , holds n $ \x -> all (\f -> discardOthers f [x] == [x::Int])
+                        [(<=),(>=),(<),(>),(==),(/=),\x y -> True]
+  , holds n $ \xs -> not (null xs) ==> discardOthers (<=) xs == [maximum xs::Int]
+  , holds n $ \xs -> not (null xs) ==> discardOthers (>=) xs == [minimum xs::Int]
+  , holds n $ \xs -> not (null xs) ==>
+      discardOthers (<) xs == replicate (count (maximum xs) xs) (maximum xs::Int)
+  , holds n $ \xs -> not (null xs) ==>
+      discardOthers (>) xs == replicate (count (minimum xs) xs) (minimum xs::Int)
+
+  , ["x","y","z","x'","y'"]    `isPrefixOf` namesFromTemplate "x"
+  , ["xs","ys","zs","xs'"]     `isPrefixOf` namesFromTemplate "xs"
+  , ["xss","yss","zss","xss'"] `isPrefixOf` namesFromTemplate "xss"
+  , ["c","d","e","c'","d'"]    `isPrefixOf` namesFromTemplate "c"
+  , ["s","t","u","s'","t'"]    `isPrefixOf` namesFromTemplate "s"
+  , ["0","1","2","3","4"]      `isPrefixOf` namesFromTemplate "0"
+  , ["1","2","3","4","5"]      `isPrefixOf` namesFromTemplate "1"
+--, ["z","a","b","z'","a'"]    `isPrefixOf` namesFromTemplate "z" -- TODO: make this pass
+  , ["x1","x2","x3","x4"]      `isPrefixOf` namesFromTemplate "x1"
+  , ["a0","a1","a2","a3"]      `isPrefixOf` namesFromTemplate "a0"
+  , ["e1","e2","e3","e4"]      `isPrefixOf` namesFromTemplate "e1"
+  , ["xs1","xs2","xs3"]        `isPrefixOf` namesFromTemplate "xs1"
+  , ["xy","zw","xy'","zw'"]    `isPrefixOf` namesFromTemplate "xy"
+  , ["ab","cd","ab'","cd'"]    `isPrefixOf` namesFromTemplate "ab"
+  , ["xys","zws","xys'"]       `isPrefixOf` namesFromTemplate "xys"
+  , ["xyz","xyz'","xyz''"]     `isPrefixOf` namesFromTemplate "xyz"
+
+  , table "l  l  l" [ ["asdf", "qwer",     "zxvc\nzxvc"]
+                    , ["0",    "1",        "2"]
+                    , ["123",  "456\n789", "3"] ] ==
+      "asdf  qwer  zxvc\n\
+      \            zxvc\n\
+      \0     1     2\n\
+      \123   456   3\n\
+      \      789\n"
+
+  , table "r  l  l" [ ["asdf", "qwer",     "zxvc\nzxvc"]
+                    , ["0",    "1",        "2"]
+                    , ["123",  "456\n789", "3"] ] ==
+      "asdf  qwer  zxvc\n\
+      \            zxvc\n\
+      \   0  1     2\n\
+      \ 123  456   3\n\
+      \      789\n"
+
+  , table "r  r  l" [ ["asdf", "qwer",     "zxvc\nzxvc"]
+                    , ["0",    "1",        "2"]
+                    , ["123",  "456\n789", "3"] ] ==
+      "asdf  qwer  zxvc\n\
+      \            zxvc\n\
+      \   0     1  2\n\
+      \ 123   456  3\n\
+      \       789\n"
+
+  -- different versions of GHC/typeable impose different orders on TypeReps,
+  -- hence: map show . sort
+  , (sort . map show . typesIn $ typeOf (undefined :: (Int -> Int) -> Int -> Bool))
+      == ["Bool","Int"]
+  , (sort . map show . typesIn $ typeOf (undefined :: (Int -> Char) -> Integer -> Bool))
+      == ["Bool","Char","Int","Integer"]
+
+  , splitAtCommas "1,2,3" == ["1","2","3"]
+  , splitAtCommas "123,456,789," == ["123","456","789"]
+  , splitAtCommas "123 456,789"  == ["123","456","789"] -- weird behaviour, but fine for speculate
+
+  , compareIndex [3,2,1] 3 1 == LT
+  , compareIndex [3,2,1] 1 3 == GT
+  , compareIndex [3,2,1] 4 1 == GT
+  , compareIndex [3,2,1] 1 0 == LT
+  , holds n $ \xs -> comparison (compareIndex (xs::[Int]))
+
+  , partitionByMarkers '#' '*' "" == ("","")
+  , partitionByMarkers '#' '*' "abc*def" == ("abc","def")
+  , partitionByMarkers '#' '*'  "abcdef" == ("abcdef","")
+  , partitionByMarkers '#' '*' "#abcdef" == ("abcdef","")
+  , partitionByMarkers '#' '*' "abc#def" == ("abcdef","")
+  , partitionByMarkers '#' '*' "*ab#cd" == ("cd","ab")
+  , partitionByMarkers '#' '*' "abc#def*ghi*jkl#mno*pqr#stu" == ("abcdefmnostu","ghijklpqr")
+  , partitionByMarkers '#' '*' "#foreground*background#foreground" == ("foregroundforeground","background")
+
+  , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys
+                    ==> strictlyOrdered (xs +++ ys :: [Int])
+  , holds n $ \xs ys -> xs +++ ys == ys +++ (xs :: [Int])
+  , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys
+                    ==> xs +++ ys == nubSort (xs ++ ys :: [Int])
+  ]