diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -88,6 +88,7 @@
 bench/arithficial
 bench/nord
 bench/unit
+bench/trilean
 bench/qs*/0arith
 bench/qs*/arith-negate-abs
 bench/qs*/arith
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -51,6 +51,7 @@
   eg/speculate-reason \
   bench/arithficial \
   bench/nord \
+  bench/trilean \
   bench/unit
 EXTRAEG = \
   eg/regexes \
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,12 +3,9 @@
 
 A list of things to do for Speculate.
 
-* simpilfy "bench" handing.  Do like in LeanCheck and Extrapolate.
+* remove lexicompare as it is already exported by Express
 
-* improve performance of the Reason module:
-  when listing rewrites of a given expression,
-  I can use a custom data structure that computes
-  matches all at once while traversing an expression.
+* simpilfy "bench" handing.  Do like in LeanCheck and Extrapolate.
 
 * (code readability) review and document code
 
@@ -21,8 +18,3 @@
   the expensive thing.  But it does not pay off to test x + y = z + w before
   testing x + y = y + x.  The second needs to hold for the first to hold.  And,
   it will be far more common!
-
-* (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
-  undefined.
diff --git a/bench/runtime-zero b/bench/runtime-zero
--- a/bench/runtime-zero
+++ b/bench/runtime-zero
@@ -1,34 +1,35 @@
 GHC 8.10.4
-express-0.1.4
-leancheck-0.9.3
+express-0.1.5
+leancheck-0.9.4
 arith               0.233
-arith-c             0.570
-arithficial         0.860
-arith-negate-abs    1.713
-binarytree          1.633
-binarytree0         0.483
-bool                1.963
-bool-c              1.730
-colour              1.946
-digraphs            1.460
-fun                 1.103
-insertsort          7.613
+arith-c             0.593
+arithficial         0.636
+arith-negate-abs    1.776
+binarytree          1.666
+binarytree0         0.506
+bool                1.973
+bool-c              1.776
+colour              2.006
+digraphs            1.513
+fun                 1.086
+insertsort          7.743
 insertsort0         0.913
-length              0.460
-list                2.586
-list-c              1.596
-minus               0.506
-minus-c             0.883
-monad               0.583
+length              0.480
+list                2.593
+list-c              1.660
+minus               0.516
+minus-c             0.880
+monad               0.570
 nord                0.010
-oddeven             6.673
-plus-abs            3.543
-pretty              8.953
-ratio               8.093
-sets                7.183
-speculate-reason    3.016
-string              0.856
-tauts               4.073
-tuples              1.200
+oddeven             6.593
+plus-abs            3.663
+pretty              9.030
+ratio               8.336
+sets                7.230
+speculate-reason    2.950
+string              0.860
+tauts               4.070
+trilean             0.010
+tuples              1.233
 unit                0.010
-zip                 2.303
+zip                 2.323
diff --git a/bench/trilean.hs b/bench/trilean.hs
new file mode 100644
--- /dev/null
+++ b/bench/trilean.hs
@@ -0,0 +1,113 @@
+-- bench/trilean.hs -- Speculate example on trileans
+--
+-- Copyright (C) 2021  Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+--
+--
+-- If used correctly,
+-- Speculate deals with Trileans just fine producing correct equations.
+--
+--
+-- The point of this example is to make Speculate produce incorrect equations
+-- by failing to include all possible values on the 'Listable' enumeration.
+--
+-- Of the three possible trilean values (@M@, @F@ and @T@),
+-- here we fail to enumerate @M@.  This ultimately causes Speculate print:
+--
+-- > p == M
+--
+-- How does that happen?
+--
+-- We first test to discover that:
+--
+-- > p &&& F == F
+--
+-- This is only true when x is F and T (the tested values)
+-- but not true in general.
+-- Speculate does not know this, then by consequence,
+-- it infers:
+--
+-- > M &&& F == F
+--
+-- Which, using the correct equation @ M &&& p  ==  M @, rewrites to:
+--
+-- > M == F
+--
+-- Similarly we also get that:
+--
+-- > T == M
+--
+-- Ultimately arriving at:
+--
+-- > p == M
+--
+--
+-- This illustrates why Speculate cannot consider equality between error values
+-- using 'Test.LeanCheck.Error.errorToEither'
+-- or    'Test.LeanCheck.Error.errorToNothing'.
+--
+-- You could also think now, to include error values in the generation,
+-- however you will lose interesting equations if you do that
+-- so it does not pay off.
+
+{-# Language DeriveDataTypeable, StandaloneDeriving #-}  -- for GHC <= 7.8
+
+import Test.Speculate hiding ((|||), (&&&))
+import Test.Speculate.Function.A10
+import Test.LeanCheck.Function.ShowFunction
+
+data Tril = M | F | T deriving (Show, Eq, Ord)
+
+deriving instance Typeable Tril  -- for GHC <= 7.8
+
+instance Listable Tril where
+  tiers  =  cons0 F
+         \/ cons0 T
+--       \/ cons0 M `ofWeight` 1
+-- Here we intentionally fail to enumerate M.
+
+instance ShowFunction Tril where bindtiers = bindtiersShow
+
+instance Name Tril where
+  name _  =  "p"
+
+neg :: Tril -> Tril
+neg T = F
+neg F = T
+neg M = M
+
+unc :: Tril -> Tril
+unc M = T
+unc _ = F
+
+(&&&) :: Tril -> Tril -> Tril
+M &&& _  =  M
+_ &&& M  =  M
+T &&& T  =  T
+_ &&& _  =  F
+
+(|||) :: Tril -> Tril -> Tril
+M ||| _  =  M
+_ ||| M  =  M
+F ||| F  =  F
+_ ||| _  =  T
+
+(===>) :: Tril -> Tril -> Tril
+M ===> _  =  M
+F ===> _  =  T
+T ===> p  =  p
+
+main :: IO ()
+main = speculate args
+  { constants =
+      [ showConstant M
+      , showConstant F
+      , showConstant T
+      , constant "neg" neg
+      , constant "&&&" (&&&)
+--    , constant "|||" (|||)
+      ]
+  , instances = [ reifyInstances (undefined :: Tril)
+--              , reifyInstances (undefined :: Tril -> Tril -> Tril)
+                ]
+  }
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -64,6 +64,41 @@
   src/Test/Speculate/CondReason.hs \
   src/Test/Speculate/Args.hs \
   bench/nord.hs
+bench/trilean: \
+  bench/trilean.hs \
+  mk/toplibs
+bench/trilean.o: \
+  src/Test/Speculate/Utils/Tuple.hs \
+  src/Test/Speculate/Utils/Timeout.hs \
+  src/Test/Speculate/Utils/Tiers.hs \
+  src/Test/Speculate/Utils/String.hs \
+  src/Test/Speculate/Utils/PrettyPrint.hs \
+  src/Test/Speculate/Utils.hs \
+  src/Test/Speculate/Utils/Ord.hs \
+  src/Test/Speculate/Utils/Misc.hs \
+  src/Test/Speculate/Utils/Memoize.hs \
+  src/Test/Speculate/Utils/List.hs \
+  src/Test/Speculate/Utils/Digraph.hs \
+  src/Test/Speculate/Utils/Colour.hs \
+  src/Test/Speculate/Utils/Class.hs \
+  src/Test/Speculate/SemiReason.hs \
+  src/Test/Speculate/Sanity.hs \
+  src/Test/Speculate/Report.hs \
+  src/Test/Speculate/Reason.hs \
+  src/Test/Speculate/Reason/Order.hs \
+  src/Test/Speculate/Pretty.hs \
+  src/Test/Speculate.hs \
+  src/Test/Speculate/Function.hs \
+  src/Test/Speculate/Function/A100.hs \
+  src/Test/Speculate/Expr.hs \
+  src/Test/Speculate/Expr/Instance.hs \
+  src/Test/Speculate/Expr/Ground.hs \
+  src/Test/Speculate/Expr/Equate.hs \
+  src/Test/Speculate/Expr/Core.hs \
+  src/Test/Speculate/Engine.hs \
+  src/Test/Speculate/CondReason.hs \
+  src/Test/Speculate/Args.hs \
+  bench/trilean.hs
 bench/unit: \
   bench/unit.hs \
   mk/toplibs
@@ -1078,6 +1113,15 @@
   src/Test/Speculate/Engine.hs \
   src/Test/Speculate/CondReason.hs
 src/Test/Speculate/Expr/Core.o: \
+  src/Test/Speculate/Utils/Tuple.hs \
+  src/Test/Speculate/Utils/Timeout.hs \
+  src/Test/Speculate/Utils/Tiers.hs \
+  src/Test/Speculate/Utils/String.hs \
+  src/Test/Speculate/Utils/PrettyPrint.hs \
+  src/Test/Speculate/Utils.hs \
+  src/Test/Speculate/Utils/Ord.hs \
+  src/Test/Speculate/Utils/Misc.hs \
+  src/Test/Speculate/Utils/Memoize.hs \
   src/Test/Speculate/Utils/List.hs \
   src/Test/Speculate/Expr/Core.hs
 src/Test/Speculate/Expr/Equate.o: \
diff --git a/mk/haskell.mk b/mk/haskell.mk
--- a/mk/haskell.mk
+++ b/mk/haskell.mk
@@ -80,7 +80,8 @@
 
 
 # Cleaning rule (add as a clean dependency)
-.PHONY: clean-hi-o
+clean-hs: clean-hi-o clean-haddock clean-cabal clean-stack
+
 clean-hi-o:
 	find $(ALL_HSS) | sed -e 's/hs$$/o/'      | xargs rm -f
 	find $(ALL_HSS) | sed -e 's/hs$$/hi/'     | xargs rm -f
@@ -113,6 +114,11 @@
 	  $(HADDOCK_HLNK_SRC) \
 	  $(HADDOCKFLAGS)
 
+clean-cabal:
+	rm -rf dist/ dist-newstyle/ cabal.project.local cabal.project.local~
+
+clean-stack:
+	rm -rf .stack-work/ stack.yaml.lock
 
 # lists all Haskell source files
 list-all-hss:
diff --git a/speculate.cabal b/speculate.cabal
--- a/speculate.cabal
+++ b/speculate.cabal
@@ -1,5 +1,5 @@
 name:                speculate
-version:             0.4.4
+version:             0.4.6
 synopsis:            discovery of properties about Haskell functions
 description:
   Speculate automatically discovers laws about Haskell functions.
@@ -84,13 +84,13 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/speculate
-  tag:             v0.4.4
+  tag:             v0.4.6
 
 
 library
   exposed-modules: Test.Speculate
                  , Test.Speculate.Args
-                 , Test.Speculate.Function
+                 , Test.Speculate.Function.A10
                  , Test.Speculate.Function.A100
                  , Test.Speculate.Function.A1000
                  , Test.Speculate.Report
@@ -120,8 +120,8 @@
                  , Test.Speculate.Utils.Timeout
                  , Test.Speculate.Utils.Tuple
   build-depends: base >= 4 && < 5
-               , leancheck >= 0.9.3
-               , express >= 0.1.4
+               , leancheck >= 0.9.4
+               , express >= 0.1.6
                , cmdargs
                , containers
   hs-source-dirs:    src
diff --git a/src/Test/Speculate.hs b/src/Test/Speculate.hs
--- a/src/Test/Speculate.hs
+++ b/src/Test/Speculate.hs
@@ -52,6 +52,7 @@
   , reifyOrd
   , reifyEqOrd
   , reifyListable
+  , reifyName
   , mkEq
   , mkOrd
   , mkOrdLessEqual
@@ -87,6 +88,7 @@
   , reifyOrd
   , reifyEqOrd
   , reifyListable
+  , reifyName
   , mkEq
   , mkOrd
   , mkOrdLessEqual
diff --git a/src/Test/Speculate/Args.hs b/src/Test/Speculate/Args.hs
--- a/src/Test/Speculate/Args.hs
+++ b/src/Test/Speculate/Args.hs
@@ -23,7 +23,6 @@
   , computeInstances
   , types
   , atoms
-  , compareExpr
   , keepExpr
   , timeout
   , shouldShowEquation
@@ -228,17 +227,6 @@
 timeout :: Args -> Bool -> Bool
 timeout Args{evalTimeout = Nothing} = id
 timeout Args{evalTimeout = Just t}  = timeoutToFalse t
-
-compareExpr :: Args -> Expr -> Expr -> Ordering
-compareExpr args = compareComplexity <> lexicompareBy cmp
-  where
-  e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT
-  e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT
-  e1 `cmp` e2 = compareIndex (exprPair:concat (atoms args)) e1 e2 <> e1 `compare` e2
-  exprPair = head . unfoldApp $ foldPair (val (), val ())
--- NOTE: "concat $ atoms args" may be an infinite list.  This function assumes
--- that the symbols will appear on the list eventually for termination.  If I
--- am correct this ivariant is assured by the rest of the code.
 
 constant :: Typeable a => String -> a -> Expr
 constant = value
diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs
--- a/src/Test/Speculate/Engine.hs
+++ b/src/Test/Speculate/Engine.hs
@@ -15,6 +15,9 @@
   , theoryAndRepresentativesFromAtoms
   , representativesFromAtoms
   , theoryFromAtoms
+  , theoryAndRepresentativesFromAtomsKeeping
+  , representativesFromAtomsKeeping
+  , theoryFromAtomsKeeping
   , equivalencesBetween
 
   , consider
@@ -110,7 +113,7 @@
 
 -- | Computes a theory from atomic expressions.  Example:
 --
--- > > theoryFromAtoms 5 compare (const True) (equal preludeInstances 100)
+-- > > theoryFromAtoms 5 (const True) (equal preludeInstances 100)
 -- > >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
 -- > Thy { rules = [ (x + y) + z == x + (y + z) ]
 -- >     , equations = [ y + x == x + y
@@ -121,15 +124,21 @@
 -- >     , closureLimit = 2
 -- >     , keepE = keepUpToLength 5
 -- >     }
-theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> Thy
-theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===)
--- TODO: eliminate two arguments:
--- * cmp can default to use order of appearance
--- * keep can default to "const True"
+theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
+theoryFromAtoms  =  theoryFromAtomsKeeping (const True)
 
-representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]
-representativesFromAtoms sz cmp keep (===) = snd . theoryAndRepresentativesFromAtoms sz cmp keep (===)
+representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
+representativesFromAtoms  =  representativesFromAtomsKeeping (const True)
 
+theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy,[[Expr]])
+theoryAndRepresentativesFromAtoms  =  theoryAndRepresentativesFromAtomsKeeping (const True)
+
+theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
+theoryFromAtomsKeeping keep (===) sz  =  fst . theoryAndRepresentativesFromAtomsKeeping keep (===) sz
+
+representativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
+representativesFromAtomsKeeping keep (===) sz  =  snd . theoryAndRepresentativesFromAtomsKeeping keep (===) sz
+
 expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [Expr] -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
 expand keep (===) sz ss (thy,sss) = (complete *** id)
                                   . foldl (flip $ consider (===) sz) (thy,sss)
@@ -141,12 +150,10 @@
   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes]
 
 -- | Given atomic expressions, compute theory and representative schema
---   expressions.
-theoryAndRepresentativesFromAtoms :: Int
-                                  -> (Expr -> Expr -> Ordering)
-                                  -> (Expr -> Bool) -> (Expr -> Expr -> Bool)
-                                  -> [[Expr]] -> (Thy,[[Expr]])
-theoryAndRepresentativesFromAtoms sz cmp keep (===) dss =
+--   expressions.  (cf. 'theoryFromAtoms')
+theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool)
+                                         -> Int -> [[Expr]] -> (Thy,[[Expr]])
+theoryAndRepresentativesFromAtomsKeeping keep (===) sz dss  =
   chain [expand keep (===) sz' (dss ! (sz'-1)) | sz' <- reverse [1..sz]] (iniThy,[])
   where
   iniThy = emptyThy { keepE = keepUpToLength sz
@@ -154,6 +161,10 @@
                     , canReduceTo = dwoBy (\e1 e2 -> e1 `cmp` e2 == GT)
                     , compareE = cmp
                     }
+  cmp  =  compareComplexityThenIndex (concat dss)
+  -- NOTE: "concat dss" may be an infinite list.  This function assumes that
+  -- the symbols will appear on the list eventually for termination.  If I am
+  -- correct, this invariant is assured by the rest of the code.
 
 -- considers a schema
 consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
@@ -163,8 +174,8 @@
   | otherwise =
     ( append thy $ equivalencesBetween (-===-) ns ns ++ eqs
     , if any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs
-        then sss
-        else sssWs )
+      then sss
+      else sssWs )
   where
   ns = rehole $ normalizeE thy (fastMostGeneralVariation s)
   e1 -===- e2  =  normalize thy e1 == normalize thy e2 || e1 === e2
@@ -240,13 +251,11 @@
   . filter (isOrd ti)
 
 conditionalTheoryFromThyAndReps :: Instances
-                                -> (Expr -> Expr -> Ordering)
                                 -> Int -> Int -> Int
                                 -> Thy -> [Expr] -> Chy
-conditionalTheoryFromThyAndReps ti cmp nt nv csz thy es' =
+conditionalTheoryFromThyAndReps ti nt nv csz thy es' =
   conditionalEquivalences
-    cmp
-    (canonicalCEqnBy cmp ti)
+    (canonicalCEqnBy (compareE thy) ti)
     (condEqual ti nt)
     (lessOrEqual ti nt)
     csz thy clpres cles
@@ -256,15 +265,14 @@
                 . filter (isEq ti . fst)
                 $ classesFromSchemas ti nt nv thy es'
 
-conditionalEquivalences :: (Expr -> Expr -> Ordering)
-                        -> ((Expr,Expr,Expr) -> Bool)
+conditionalEquivalences :: ((Expr,Expr,Expr) -> Bool)
                         -> (Expr -> Expr -> Expr -> Bool)
                         -> (Expr -> Expr -> Bool)
                         -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy
-conditionalEquivalences cmp canon cequal (==>) csz thy clpres cles =
+conditionalEquivalences canon cequal (==>) csz thy clpres cles =
     cdiscard (\(ce,e1,e2) -> subConsequence thy clpres ce e1 e2)
   . foldl (flip cinsert) (Chy [] cdg clpres thy)
-  . sortBy (cmp `on` foldTrio)
+  . sortBy (compareE thy `on` foldTrio)
   . discard (\(pre,e1,e2) -> pre == val False
                           || length (nubVars pre \\ (nubVars e1 +++ nubVars e2)) > 0
                           || subConsequence thy [] pre e1 e2)
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
@@ -12,9 +12,8 @@
   , module Data.Express.Utils.Typeable
 
   -- * Order
-  , lexicompare
-  , lexicompareBy
-  , fastCompare
+  , compareLexicographicallyBy
+  , compareComplexityThenIndex
 
   -- * Properties
   , isConstantNamed
@@ -34,25 +33,15 @@
 
 import Data.Express
 import Data.Express.Utils.Typeable
-import Test.Speculate.Utils.List
+import Test.Speculate.Utils
 import Data.Monoid ((<>))
 import Data.Functor ((<$>)) -- for GHC <= 7.8
 
--- faster comparison, to be used when nubSorting Expr values
-fastCompare :: Expr -> Expr -> Ordering
-fastCompare  =  cmp
-  where
-  (f :$ x)       `cmp` (g :$ y)        =  f  `cmp` g <> x `cmp` y
-  (_ :$ _)       `cmp` _               =  GT
-  _              `cmp` (_ :$ _)        =  LT
-  x@(Value n1 _) `cmp` y@(Value n2 _)  =  typ x `compareTy` typ y
-                                       <> n1 `compare` n2
-
-lexicompare :: Expr -> Expr -> Ordering
-lexicompare = lexicompareBy compare
-
-lexicompareBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
-lexicompareBy compareConstants  =  cmp
+-- | Lexicographical comparison of 'Expr's
+--   where variables < constants < applications and
+--   constants are disambiguated by the given function.
+compareLexicographicallyBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
+compareLexicographicallyBy compareConstants  =  cmp
   where
   (f :$ x) `cmp` (g :$ y)  =  f  `cmp` g <> x `cmp` y
   (_ :$ _) `cmp` _         =  GT
@@ -60,11 +49,23 @@
   e1 `cmp` e2  =  case (isVar e1, isVar e2) of
     (True,  True)  -> let Value n1 _ = e1
                           Value n2 _ = e2
-                      in typ e1 `compareTy` typ e2 <> n1 `compare` n2
+                      in typ e1 `compareTy` typ e2
+                      <> length n1 `compare` length n2
+                      <> n1 `compare` n2
     (False, True)  -> GT
     (True,  False) -> LT
     (False, False) -> e1 `compareConstants` e2
-  -- Var < Constants < Apps
+
+-- | Comparison of 'Expr's:
+--
+-- 1. 'compareComplexity' from 'Data.Express'
+-- 2. 'lexicompareBy' index of the given list
+compareComplexityThenIndex :: [Expr] -> Expr -> Expr -> Ordering
+compareComplexityThenIndex as  =  compareComplexity <> compareLexicographicallyBy cmp
+  where
+  e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT
+  e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT
+  e1 `cmp` e2 = compareIndex as e1 e2 <> e1 `compare` e2
 
 countVars :: Expr -> [(Expr,Int)]
 countVars e = map (\e' -> (e',length . filter (== e') $ vars e)) $ nubVars e
diff --git a/src/Test/Speculate/Function.hs b/src/Test/Speculate/Function.hs
deleted file mode 100644
--- a/src/Test/Speculate/Function.hs
+++ /dev/null
@@ -1,44 +0,0 @@
--- |
--- Module      : Test.Speculate.Function
--- Copyright   : (c) 2016-2019 Rudy Matela
--- License     : 3-Clause BSD  (see the file LICENSE)
--- Maintainer  : Rudy Matela <rudy@matela.com.br>
---
--- This module is part of Speculate.
---
--- If should import this if you want Speculate to treat functions as data
--- values.  This exports a Listable instance for functions an a facility to
--- define Eq and Ord instances for functions.
---
--- Please see the @fun@ and @monad@ examples from Speculate's source
--- repository for more details.
-module Test.Speculate.Function
-  ( funToList
-  , areEqualFor
-  , compareFor
-  )
-where
-
-import Test.Speculate
-import Test.LeanCheck.Function()
-import Test.LeanCheck.Error (errorToNothing)
-import Data.Function (on)
-
-funToList :: Listable a => (a -> b) -> [Maybe b]
-funToList f = map (errorToNothing . f) list
-
--- | This function can be used to define an Eq instance for functions based on
---   testing and equality of returned values, like so:
---
--- > instance (Listable a, Eq b) => Eq (a -> b) where
--- >   (==) = areEqualFor 100
-areEqualFor :: (Listable a, Eq b) => Int -> (a -> b) -> (a -> b) -> Bool
-areEqualFor n = (==) `on` (take n . funToList)
-
--- | This function can be used to define an Ord instance for functions based on
---   testing and ordering of returned values, like so:
---
--- > instance (Listable a, Ord b) => Ord (a -> b) where
--- >   compare = compareFor 100
-compareFor :: (Listable a, Ord b) => Int -> (a -> b) -> (a -> b) -> Ordering
-compareFor n = compare `on` (take n . funToList)
diff --git a/src/Test/Speculate/Function/A10.hs b/src/Test/Speculate/Function/A10.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Speculate/Function/A10.hs
@@ -0,0 +1,21 @@
+-- |
+-- Module      : Test.Speculate.Function.A10
+-- Copyright   : (c) 2019 Rudy Matela
+-- License     : 3-Clause BSD  (see the file LICENSE)
+-- Maintainer  : Rudy Matela <rudy@matela.com.br>
+--
+-- This module is part of Speculate.
+--
+-- This module exports a Listable instance for functions along with two toy Eq
+-- and Ord instances for functions based on 10 sample return values.
+module Test.Speculate.Function.A10 () where
+
+import Test.Speculate
+import Test.LeanCheck.Function ()
+import Test.LeanCheck.Function.List (areEqualFor, compareFor)
+
+instance (Listable a, Eq b) => Eq (a -> b) where
+  (==) = areEqualFor 10
+
+instance (Listable a, Ord b) => Ord (a -> b) where
+  compare = compareFor 10
diff --git a/src/Test/Speculate/Function/A100.hs b/src/Test/Speculate/Function/A100.hs
--- a/src/Test/Speculate/Function/A100.hs
+++ b/src/Test/Speculate/Function/A100.hs
@@ -11,7 +11,8 @@
 module Test.Speculate.Function.A100 () where
 
 import Test.Speculate
-import Test.Speculate.Function
+import Test.LeanCheck.Function ()
+import Test.LeanCheck.Function.List (areEqualFor, compareFor)
 
 instance (Listable a, Eq b) => Eq (a -> b) where
   (==) = areEqualFor 100
diff --git a/src/Test/Speculate/Function/A1000.hs b/src/Test/Speculate/Function/A1000.hs
--- a/src/Test/Speculate/Function/A1000.hs
+++ b/src/Test/Speculate/Function/A1000.hs
@@ -11,7 +11,8 @@
 module Test.Speculate.Function.A1000 () where
 
 import Test.Speculate
-import Test.Speculate.Function
+import Test.LeanCheck.Function ()
+import Test.LeanCheck.Function.List (areEqualFor, compareFor)
 
 instance (Listable a, Eq b) => Eq (a -> b) where
   (==) = areEqualFor 1000
diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs
--- a/src/Test/Speculate/Reason.hs
+++ b/src/Test/Speculate/Reason.hs
@@ -13,6 +13,8 @@
   , normalize
   , normalizeE
   , isNormal
+  , isRootNormal
+  , isRootNormalE
   , complete
   , equivalent
   , equivalentInstance
@@ -157,16 +159,28 @@
 
 -- normalize by rules and equations
 normalizeE :: Thy -> Expr -> Expr
-normalizeE Thy {rules = rs, equations = eqs, canReduceTo = (->-) } = n
+normalizeE thy@(Thy {equations = eqs, canReduceTo = (->-)})  =  n1
   where
-  n e = case concatMap (e `reductions1`) rs
-          ++ filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of
-          []     -> e -- already normalized
-          (e':_) -> n e'
+  n1  =  n2 . normalize thy
+  n2 e = case filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of
+         []     -> e -- already normalized
+         (e':_) -> n1 e'
 
 isNormal :: Thy -> Expr -> Bool
 isNormal thy e = normalizeE thy e == e
 
+isRootNormal :: Thy -> Expr -> Bool
+isRootNormal thy e  =  none (e `isInstanceOf`) $ map fst (rules thy)
+  where
+  none p  =  not . any p
+
+isRootNormalE :: Thy -> Expr -> Bool
+isRootNormalE thy e  =  isRootNormal thy e
+                    &&  null (filter (e ->-) . mapMaybe (reduceRoot e) $ equations thy ++ map swap (equations thy))
+  where
+  (->-)  =  canReduceTo thy
+  reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1)
+
 reduceRoot :: Expr -> Rule -> Maybe Expr
 reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1)
 
@@ -209,22 +223,22 @@
 
 criticalPairs :: Thy -> [(Expr,Expr)]
 criticalPairs thy@Thy{rules = rs}  =
-  nubMergesBy fastCompareEqn [r `criticalPairsWith` s | r <- rs, s <- rs]
+  nubMergesBy compareEqnQuickly [r `criticalPairsWith` s | r <- rs, s <- rs]
   where
   criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)]
   r1@(e1,_) `criticalPairsWith` r2@(e2,_) =
-      nubSortBy fastCompareEqn
+      nubSortBy compareEqnQuickly
     . map sortuple
     . filter (uncurry (/=))
     . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))
-    . nubSortBy fastCompare
+    . nubSortBy compareQuickly
     $ overlaps e1 e2
   xs ** ys = [(x,y) | x <- xs, y <- ys]
   sortuple (x,y) | x < y     = (y,x)
                  | otherwise = (x,y)
-  fastCompareEqn = fastCompare `on` foldPair
+  compareEqnQuickly = compareQuickly `on` foldPair
   (<) :: Expr -> Expr -> Bool
-  e1 < e2 = e1 `fastCompare` e2 == LT
+  e1 < e2 = e1 `compareQuickly` e2 == LT
 
 -- Warning: will have to also be applied in reverse to get all overlaps.
 --
diff --git a/src/Test/Speculate/Report.hs b/src/Test/Speculate/Report.hs
--- a/src/Test/Speculate/Report.hs
+++ b/src/Test/Speculate/Report.hs
@@ -32,7 +32,7 @@
   let ti = computeInstances args
   let ats = types args
   let dss = atoms args
-  let (thy,ess) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) dss
+  let (thy,ess) = theoryAndRepresentativesFromAtomsKeeping (keepExpr args) (timeout args .: equal ti n) sz dss
   let es = uptoT sz ess
   putArgs args
   -- TODO: somehow show the tail of dss, maybe use "..."
@@ -50,7 +50,7 @@
   when (showTheory args)       . putStrLn $ showThy thy
   let shy = semiTheoryFromThyAndReps ti n (maxVars args) thy
           $ filter (\e -> size e <= computeMaxSemiSize args) es
-  let chy = conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es
+  let chy = conditionalTheoryFromThyAndReps ti n (maxVars args) (computeMaxCondSize args) thy es
   let equations     = finalEquations     (shouldShowEquation args) ti                          thy
   let semiEquations = finalSemiEquations (shouldShowEquation args) ti (equivalentInstance thy) shy
   let condEquations = finalCondEquations (shouldShowConditionalEquation args)                  chy
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -4,5 +4,5 @@
 - .
 
 extra-deps:
-- leancheck-0.9.3
-- express-0.1.4
+- leancheck-0.9.4
+- express-0.1.6
diff --git a/test/model/trilean-s4.out b/test/model/trilean-s4.out
new file mode 100644
--- /dev/null
+++ b/test/model/trilean-s4.out
@@ -0,0 +1,18 @@
+max expr size  =    4
+  |- on ineqs  =    3
+  |- on conds  =    3
+max  #-tests   =  500
+min  #-tests   =   25  (to consider p ==> q true)
+max  #-vars    =    2  (for inequational and conditional laws)
+
+_ :: Tril
+M :: Tril
+F :: Tril
+T :: Tril
+neg :: Tril -> Tril
+(&&&) :: Tril -> Tril -> Tril
+
+p == M
+
+M <= p
+
diff --git a/test/model/trilean.out b/test/model/trilean.out
new file mode 100644
--- /dev/null
+++ b/test/model/trilean.out
@@ -0,0 +1,18 @@
+max expr size  =    5
+  |- on ineqs  =    4
+  |- on conds  =    4
+max  #-tests   =  500
+min  #-tests   =   25  (to consider p ==> q true)
+max  #-vars    =    2  (for inequational and conditional laws)
+
+_ :: Tril
+M :: Tril
+F :: Tril
+T :: Tril
+neg :: Tril -> Tril
+(&&&) :: Tril -> Tril -> Tril
+
+p == M
+
+M <= p
+
diff --git a/test/order.hs b/test/order.hs
--- a/test/order.hs
+++ b/test/order.hs
@@ -19,23 +19,10 @@
 tests n =
   [ True -- see test-expr.hs for general Expr orders
 
-  , holds n $ compare ==== (compareComplexity <> lexicompare)
-  , holds n $ isComparison lexicompare
-  , holds n $ isComparison compareComplexity
-
-  , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompare in
-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
-  , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompareBy (flip compare) in
-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
-  , holds n $ \(BoolToBoolE e1) (BoolToBoolE e2) (BoolE e3) -> let cmp = lexicompare in
-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
-  , holds n $ \(BoolToBoolE e1) (BoolToBoolE e2) (BoolE e3) -> let cmp = lexicompareBy (flip compare) in
-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
-
-  -- some tests of order
-  , value "xx" xx < zero
-  , value "xxeqxx" (Equation xx xx) < value "xx" xx
-  , value "xx" xx < value "emptyThyght" (Thyght emptyThy)
+  , holds n $ compareLexicographicallyBy compareLexicographically ==== compareLexicographically
+  , holds n $ compareLexicographicallyBy compare ==== compareLexicographically
+  , holds n $ isComparison (compareLexicographicallyBy $ flip compareLexicographically)
+  , holds n $ isComparison (compareLexicographicallyBy $ flip compare)
 
   , holds n $ simplificationOrder (|>|)
   , holds n $ seriousSimplificationOrder (|> )
@@ -78,7 +65,7 @@
   , 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)
+  -- compareLexicographically is compatible (almost as if by coincidence)
   , fails n $ simplificationOrder lgt
   , holds n $ compatible          lgt
   , fails n $ closedUnderSub      lgt
@@ -91,7 +78,7 @@
   , holds n $ subtermProperty     cgt
   ]
   where
-  e1 `lgt` e2 = e1 `lexicompare` e2 == GT
+  e1 `lgt` e2 = e1 `compareLexicographically` e2 == GT
   e1 `cgt` e2 = e1 `compare` e2 == GT
 
 -- weaker than simplificationOrder