diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -549,6 +549,13 @@
     rules = map rule_rule (filter ok (IntMap.elems (st_rule_ids state)))
     ok r = unMax (rule_max r) `IntSet.disjoint` excluded
 
+-- Assume that all rules form a confluent rewrite system.
+{-# INLINEABLE assumeComplete #-}
+assumeComplete :: Function f => State f -> State f
+assumeComplete state =
+  state { st_not_complete = IntSet.empty,
+          st_complete = Index.fromListWith lhs (map rule_rule (IntMap.elems (st_rule_ids state))) }
+
 -- For goal terms we store the set of all their normal forms.
 -- Name and number are for information only.
 data Goal f =
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -229,7 +229,7 @@
       cp_top = subst_ sub cp_top,
       cp_proof = subst_ sub cp_proof }
 
-instance PrettyTerm f => Pretty (CriticalPair f) where
+instance (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) where
   pPrint CriticalPair{..} =
     vcat [
       pPrint cp_eqn,
diff --git a/Twee/Constraints.hs b/Twee/Constraints.hs
--- a/Twee/Constraints.hs
+++ b/Twee/Constraints.hs
@@ -35,7 +35,7 @@
 fromTerm (Var x) = Just (Variable x)
 fromTerm _ = Nothing
 
-instance PrettyTerm f => Pretty (Atom f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where
   pPrint = pPrint . toTerm
 
 data Formula f =
@@ -45,7 +45,7 @@
   | Or  [Formula f]
   deriving (Eq, Ord, Show)
 
-instance PrettyTerm f => Pretty (Formula f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Formula f) where
   pPrintPrec _ _ (Less t u) = hang (pPrint t <+> text "<") 2 (pPrint u)
   pPrintPrec _ _ (LessEq t u) = hang (pPrint t <+> text "<=") 2 (pPrint u)
   pPrintPrec _ _ (And []) = text "true"
@@ -103,7 +103,7 @@
     equals      :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair
   deriving (Eq, Ord)
 
-instance PrettyTerm f => Pretty (Branch f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Branch f) where
   pPrint Branch{..} =
     braces $ fsep $ punctuate (text ",") $
       [pPrint x <+> text "<" <+> pPrint y | (x, y) <- less ] ++
@@ -189,7 +189,7 @@
 -- x <  y if major x < major y
 -- x <= y if major x = major y and minor x < minor y
 
-instance PrettyTerm f => Pretty (Model f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Model f) where
   pPrint (Model m)
     | Map.size m <= 1 = text "empty"
     | otherwise = fsep (go (sortBy (comparing snd) (Map.toList m)))
diff --git a/Twee/Equation.hs b/Twee/Equation.hs
--- a/Twee/Equation.hs
+++ b/Twee/Equation.hs
@@ -21,7 +21,7 @@
   termsDL (t :=: u) = termsDL t `mplus` termsDL u
   subst_ sub (t :=: u) = subst_ sub t :=: subst_ sub u
 
-instance PrettyTerm f => Pretty (Equation f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Equation f) where
   pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y
 
 -- | Order an equation roughly left-to-right.
diff --git a/Twee/Pretty.hs b/Twee/Pretty.hs
--- a/Twee/Pretty.hs
+++ b/Twee/Pretty.hs
@@ -72,7 +72,7 @@
 instance (Pretty f, Labelled f) => Pretty (Fun f) where
   pPrintPrec l p = pPrintPrec l p . fun_value
 
-instance PrettyTerm f => Pretty (Term f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Term f) where
   pPrintPrec l p (Var x) = pPrintPrec l p x
   pPrintPrec l p (App f xs) =
     pPrintTerm (termStyle (fun_value f)) l p (pPrint f) (unpack xs)
@@ -94,7 +94,7 @@
 maybeHighlight cs (Just []) d = highlight cs d
 maybeHighlight _ _ d = d
 
-instance PrettyTerm f => Pretty (HighlightedTerm f) where
+instance (Labelled f, PrettyTerm f) => Pretty (HighlightedTerm f) where
   pPrintPrec l p (HighlightedTerm cs h (Var x)) =
     maybeHighlight cs h (pPrintPrec l p x)
   pPrintPrec l p (HighlightedTerm cs h (App f xs)) =
@@ -107,10 +107,10 @@
           Just (n:ns) | i == n -> HighlightedTerm cs (Just ns) t
           _ -> HighlightedTerm cs Nothing t
 
-instance PrettyTerm f => Pretty (TermList f) where
+instance (Labelled f, PrettyTerm f) => Pretty (TermList f) where
   pPrintPrec _ _ = pPrint . unpack
 
-instance PrettyTerm f => Pretty (Subst f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Subst f) where
   pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"
     where
       docs =
@@ -118,7 +118,7 @@
         | (x, t) <- substToList sub ]
 
 -- | A class for customising the printing of function symbols.
-class (Pretty f, Labelled f) => PrettyTerm f where
+class Pretty f => PrettyTerm f where
   -- | The style of the function symbol. Defaults to 'curried'.
   termStyle :: f -> TermStyle
   termStyle _ = curried
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -86,7 +86,7 @@
 -- This is the trusted core of the module.
 {-# INLINEABLE certify #-}
 {-# SCC certify #-}
-certify :: PrettyTerm f => Derivation f -> Proof f
+certify :: Function f => Derivation f -> Proof f
 certify p =
   case check p of
     Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)
@@ -146,7 +146,7 @@
 
 instance Function f => Pretty (Proof f) where
   pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation)
-instance PrettyTerm f => Pretty (Derivation f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Derivation f) where
   pPrint (UseLemma lemma sub) =
     text "subst" <#> pPrintTuple [text "lemma" <+> pPrint (equation lemma), pPrint sub]
   pPrint (UseAxiom axiom sub) =
@@ -160,12 +160,12 @@
   pPrint (Cong f ps) =
     text "cong" <#> pPrintTuple (pPrint f:map pPrint ps)
 
-instance PrettyTerm f => Pretty (Axiom f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Axiom f) where
   pPrint Axiom{..} =
     text "axiom" <#>
     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
 
-foldLemmas :: PrettyTerm f => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
+foldLemmas :: (Labelled f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
 foldLemmas op ds =
   execState (mapM_ foldGoal ds) Map.empty
   where
@@ -190,7 +190,7 @@
     op lem = certify . f . unfoldLemmas (\pf -> Just (simpleLemma (lem Map.! pf)))
     lem = foldLemmas op ds
 
-allLemmas :: PrettyTerm f => [Derivation f] -> [Proof f]
+allLemmas :: Function f => [Derivation f] -> [Proof f]
 allLemmas ds =
   reverse [p | (_, p, _) <- map vertex (topSort graph)]
   where
@@ -215,7 +215,7 @@
 lemma :: Proof f -> Subst f -> Derivation f
 lemma p sub = UseLemma p sub
 
-simpleLemma :: PrettyTerm f => Proof f -> Derivation f
+simpleLemma :: Function f => Proof f -> Derivation f
 simpleLemma p =
   UseLemma p (autoSubst (equation p))
 
@@ -270,7 +270,7 @@
 --   * Trans is right-associated
 --   * Each Cong has at least one non-Refl argument
 --   * Refl is not used unnecessarily
-simplify :: PrettyTerm f => Derivation f -> Derivation f
+simplify :: Function f => Derivation f -> Derivation f
 simplify (Symm p) = symm (simplify p)
 simplify (Trans p q) = trans (simplify p) (simplify q)
 simplify (Cong f ps) = cong f (map simplify ps)
@@ -851,7 +851,7 @@
 --
 -- Used both here and in the main file.
 describeEquation ::
-  PrettyTerm f =>
+  Function f =>
   String -> String -> Maybe String -> Equation f -> Doc
 describeEquation kind num mname eqn =
   text kind <+> text num <#>
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -109,7 +109,7 @@
   subst_ sub (Permutative ts) = Permutative (subst_ sub ts)
   subst_ _   Unoriented = Unoriented
 
-instance PrettyTerm f => Pretty (Rule f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Rule f) where
   pPrint (Rule or _ l r) =
     pPrint l <+> text (showOrientation or) <+> pPrint r
     where
@@ -188,7 +188,11 @@
 {-# INLINEABLE simplify #-}
 {-# SCC simplify #-}
 simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-simplify !idx !t
+simplify = simplifyOutermost
+
+-- | Compute the normal form of a term wrt only oriented rules, using outermost reduction.
+simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
+simplifyOutermost !idx !t
   | t == u = t
   | otherwise = simplify idx u
   where
@@ -202,6 +206,18 @@
     simp (Cons (App f ts) us) =
       app f (simp ts) `mappend` simp us
 
+-- | Compute the normal form of a term wrt only oriented rules, using innermost reduction.
+simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
+simplifyInnermost !idx !t = simp t
+  where
+    simp t =
+      case [rw | u <- reverseSubterms t, Just rw <- [simpleRewrite idx u]] of
+        [] -> t
+        (rule, sub):_ ->
+          let l = build (Term.subst sub (lhs rule))
+              r = build (Term.subst sub (rhs rule))
+          in simp (build (replace l r (singleton t)))
+
 -- | Find a simplification step that applies to a term.
 {-# INLINEABLE simpleRewrite #-}
 {-# SCC simpleRewrite #-}
@@ -242,7 +258,7 @@
     u = result t rs
 
 -- | Turn a reduction into a proof.
-reductionProof :: PrettyTerm f => Term f -> Reduction f -> Derivation f
+reductionProof :: Function f => Term f -> Reduction f -> Derivation f
 reductionProof t ps = red t (Proof.Refl t) (reverse ps)
   where
     red _ p [] = p
@@ -253,7 +269,7 @@
 ruleResult :: Term f -> Rule f -> Term f
 ruleResult t r = build (replace (lhs r) (rhs r) (singleton t))
 
-ruleProof :: PrettyTerm f => Term f -> Rule f -> Derivation f
+ruleProof :: Function f => Term f -> Rule f -> Derivation f
 ruleProof t r@(Rule _ _ lhs _)
   | t == lhs = ruleDerivation r
   | len t < len lhs = Proof.Refl t
@@ -316,7 +332,15 @@
 
 -- | Apply a strategy anywhere in a term.
 anywhere :: Strategy f -> Strategy f
-anywhere strat t = concatMap strat (subterms t)
+anywhere = anywhereOutermost
+
+-- | Apply a strategy anywhere in a term, preferring outermost reductions.
+anywhereOutermost :: Strategy f -> Strategy f
+anywhereOutermost strat t = concatMap strat (subterms t)
+
+-- | Apply a strategy anywhere in a term, preferring innermost reductions.
+anywhereInnermost :: Strategy f -> Strategy f
+anywhereInnermost strat t = concatMap strat (reverseSubterms t)
 
 --------------------------------------------------------------------------------
 -- * Basic strategies. These only apply at the root of the term.
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -26,14 +26,14 @@
   pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest,
   empty, unpack, lenList,
   -- * Function symbols and variables
-  Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..),
+  Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..), AutoLabel(..),
   -- * Building terms
   Build(..),
   Builder,
   build, buildList,
   con, app, var,
   -- * Access to subterms
-  children, properSubterms, subtermsList, subterms, occurs, isSubtermOf, isSubtermOfList, at,
+  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at,
   -- * Substitutions
   Substitution(..),
   subst,
@@ -75,6 +75,8 @@
 import qualified Data.IntMap.Strict as IntMap
 import Control.Arrow((&&&))
 import Twee.Utils
+import qualified Twee.Label as Label
+import Data.Typeable
 
 --------------------------------------------------------------------------------
 -- * A type class for builders
@@ -596,6 +598,18 @@
 subterms :: Term f -> [Term f]
 subterms = subtermsList . singleton
 
+-- | Find all subterms of a term, but in reverse order.
+{-# INLINE reverseSubtermsList #-}
+reverseSubtermsList :: TermList f -> [Term f]
+reverseSubtermsList t =
+  [ unsafeAt n t | n <- [k-1,k-2..0] ]
+  where
+    k = lenList t
+
+{-# INLINE reverseSubterms #-}
+reverseSubterms :: Term f -> [Term f]
+reverseSubterms t = reverseSubtermsList (singleton t)
+
 -- | Find all proper subterms of a term.
 {-# INLINE properSubterms #-}
 properSubterms :: Term f -> [Term f]
@@ -640,6 +654,7 @@
 replace !_ !_ Empty = mempty
 replace t u (Cons v vs)
   | t == v = builder u `mappend` replace t u vs
+  | len v < len t = builder v `mappend` replace t u vs
   | otherwise =
     case v of
       Var x -> var x `mappend` replace t u vs
@@ -708,6 +723,12 @@
   find :: Int -> f
 
 instance (Labelled f, Show f) => Show (Fun f) where show = show . fun_value
+
+-- | For "deriving via": a Labelled instance which uses Twee.Label.
+newtype AutoLabel a = AutoLabel { unAutoLabel :: a }
+instance (Ord a, Typeable a) => Labelled (AutoLabel a) where
+  label = fromIntegral . Label.labelNum . Label.label . unAutoLabel
+  find = AutoLabel . Label.find . Label.unsafeMkLabel . fromIntegral
 
 -- | A pattern which extracts the 'fun_value' from a 'Fun'.
 pattern F :: Labelled f => Int -> f -> Fun f
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -79,11 +79,15 @@
 
 -- | Index into a termlist.
 at :: Int -> TermList f -> Term f
-at n (TermList lo hi arr)
-  | n < 0 || lo+n >= hi = error "term index out of bounds"
-  | otherwise =
-    case TermList (lo+n) hi arr of
-      UnsafeCons t _ -> t
+at n t
+  | n < 0 || low t + n >= high t = error "term index out of bounds"
+  | otherwise = unsafeAt n t
+
+-- | Index into a termlist, without bounds checking.
+unsafeAt :: Int -> TermList f -> Term f
+unsafeAt n (TermList lo hi arr) =
+  case TermList (lo+n) hi arr of
+    UnsafeCons t _ -> t
 
 {-# INLINE lenList #-}
 -- | The length of (number of symbols in) a termlist.
diff --git a/twee-lib.cabal b/twee-lib.cabal
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,5 +1,5 @@
 name:                twee-lib
-version:             2.3
+version:             2.3.1
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3