diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -148,6 +148,7 @@
   , AllE
   , NumE
   , Name
+  , Theorem
   -- * Expressions
   -- ** Constants
   , true
@@ -209,9 +210,9 @@
   -- ** Incrementing and decrementing.
   , incr
   , decr
-  -- ** Assertions and  Assumptions
-  , assert
+  -- ** Assumptions and theorems.
   , assume
+  , theorem
   -- * Verification
   , verify
   -- * Code Generation
@@ -363,23 +364,23 @@
 --   And assertion names, and hence counter example trace file names, are produce from labels.
 (-|) :: Name -> Stmt a -> Stmt a
 name -| stmt = do
-  (path0, stmt0) <- get
-  put (path0 ++ [name], Null)
+  (id, path0, stmt0) <- get
+  put (id, path0 ++ [name], Null)
   a <- stmt
-  (_, stmt1) <- get
-  put (path0, stmt0)
+  (id, _, stmt1) <- get
+  put (id, path0, stmt0)
   statement $ Label name stmt1
   return a
 
-get :: Stmt ([Name], Statement)
+get :: Stmt (Int, [Name], Statement)
 get = Stmt $ \ a -> (a, a)
 
-put :: ([Name], Statement) -> Stmt ()
+put :: (Int, [Name], Statement) -> Stmt ()
 put s = Stmt $ \ _ -> ((), s)
 
 getPath :: Stmt [Name]
 getPath = do
-  (path, _) <- get
+  (_, path, _) <- get
   return path
 
 var :: AllE a => Name -> a -> Stmt (V a)
@@ -437,7 +438,7 @@
 decr a = a <== ref a - 1
 
 -- | The Stmt monad holds variable declarations and statements.
-data Stmt a = Stmt (([Name], Statement) -> (a, ([Name], Statement)))
+data Stmt a = Stmt ((Int, [Name], Statement) -> (a, (Int, [Name], Statement)))
 
 instance Monad Stmt where
   return a = Stmt $ \ s -> (a, s)
@@ -449,10 +450,10 @@
       Stmt f4 = f2 a
 
 statement :: Statement -> Stmt ()
-statement a = Stmt $ \ (path, statement) -> ((), (path, Sequence statement a))
+statement a = Stmt $ \ (id, path, statement) -> ((), (id, path, Sequence statement a))
 
-evalStmt :: [Name] -> Stmt () -> ([Name], Statement)
-evalStmt path (Stmt f) = snd $ f (path, Null)
+evalStmt :: Int -> [Name] -> Stmt () -> (Int, [Name], Statement)
+evalStmt id path (Stmt f) = snd $ f (id, path, Null)
 
 class Assign a where
   (<==) :: V a -> E a -> Stmt ()
@@ -460,22 +461,33 @@
 instance Assign Int   where a <== b = statement $ Assign a b
 instance Assign Float where a <== b = statement $ Assign a b
 
--- | Assert that a condition is true.
-assert :: E Bool -> Stmt ()
-assert = statement . Assert
-
 -- | Declare an assumption condition is true.
 --   Assumptions expressions must contain variables directly or indirectly related
 --   to the assertion under verification, otherwise they will be ignored.
 assume :: E Bool -> Stmt ()
 assume a = statement $ Assume a
 
+-- | Theorem to be proven or used as lemmas to assist proofs of other theorems.
+data Theorem = Theorem' Int
+
+-- | Defines a new theorem.
+--
+-- > theorem name k lemmas proposition
+theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem
+theorem name k lemmas proposition
+  | k < 1 = error $ "k-induction search depth must be > 0: " ++ name ++ " k = " ++ show k
+  | otherwise = do
+    (id, path, stmt) <- get
+    put (id + 1, path, Sequence stmt $ Label name $ Theorem id k [ i | Theorem' i <- lemmas ] proposition)
+    return $ Theorem' id
+
 -- | Conditional if-else.
 ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
 ifelse cond onTrue onFalse = do
-  path <- getPath
-  let (_, stmt1) = evalStmt path onTrue
-      (_, stmt2) = evalStmt path onFalse
+  (id0, path, stmt) <- get
+  let (id1, _, stmt1) = evalStmt id0 path onTrue
+      (id2, _, stmt2) = evalStmt id1 path onFalse
+  put (id2, path, stmt)
   statement $ Branch cond stmt1 stmt2
 
 -- | Conditional if without the else.
@@ -498,10 +510,14 @@
 -- | Verify a program.
 --
 -- > verify pathToYices maxK program
-verify :: FilePath -> Int -> Stmt () -> IO ()
-verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program
+verify :: FilePath -> Stmt () -> IO ()
+verify yices program = V.verify yices stmt
+  where
+  (_, _, stmt) = evalStmt 0 [] program
 
 -- | Generate C code.
 code :: Name -> Stmt () -> IO ()
-code name program = C.code name $ snd $ evalStmt [] program
+code name program = C.code name stmt
+  where
+  (_, _, stmt) = evalStmt 0 [] program
 
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -34,7 +34,7 @@
   Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"
   Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"
   Sequence a b -> codeStmt name path a ++ codeStmt name path b
-  Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
+  Theorem _ _ _ a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
   Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
   Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
   Null -> ""
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -4,6 +4,7 @@
   , UV (..)
   , Name
   , Path
+  , UID
   , PathName (..)
   , AllE (..)
   , NumE
@@ -13,6 +14,7 @@
   , varInfo
   , stmtVars
   , exprVars
+  , theorems
   ) where
 
 import Data.List
@@ -22,6 +24,8 @@
 
 type Path = [Name]
 
+type UID = Int
+
 -- | A mutable variable.
 data V a = V Bool [Name] a deriving (Eq, Ord)
 
@@ -101,7 +105,7 @@
   Assign   :: AllE a => V a -> E a -> Statement
   Branch   :: E Bool -> Statement -> Statement -> Statement
   Sequence :: Statement -> Statement -> Statement
-  Assert   :: E Bool -> Statement
+  Theorem  :: Int -> Int -> [Int] -> E Bool -> Statement  -- ^ Theorem id depth lemmas expr
   Assume   :: E Bool -> Statement
   Label    :: Name -> Statement -> Statement
   Null     :: Statement
@@ -122,18 +126,18 @@
     UVInt  a  -> varInfo a
     UVFloat a -> varInfo a
 
--- Variables in a program.
+-- | Variables in a program.
 stmtVars :: Statement -> [UV]
 stmtVars a = case a of
   Assign a b   -> nub $ untype a : exprVars b
   Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
   Sequence a b -> nub $ stmtVars a ++ stmtVars b
-  Assert a     -> exprVars a
+  Theorem _ _ _ a -> exprVars a
   Assume a     -> exprVars a
   Label  _ a   -> stmtVars a
   Null         -> []
 
--- Variables in an expression.
+-- | Variables in an expression.
 exprVars :: E a -> [UV]
 exprVars a = case a of
   Ref a     -> [untype a]
@@ -152,4 +156,15 @@
   Le  a b   -> exprVars a ++ exprVars b
   Ge  a b   -> exprVars a ++ exprVars b
   Mux a b c -> exprVars a ++ exprVars b ++ exprVars c
+
+-- | Theorems in a program.
+theorems :: Statement -> [(Int, Int, [Int], E Bool)]
+theorems a = case a of
+  Theorem id k lemmas expr -> [(id, k, lemmas, expr)]
+  Assign _ _   -> []
+  Branch _ a b -> theorems a ++ theorems b
+  Sequence a b -> theorems a ++ theorems b
+  Assume _     -> []
+  Label  _ a   -> theorems a
+  Null         -> []
 
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
deleted file mode 100644
--- a/Language/ImProve/Examples.hs
+++ /dev/null
@@ -1,200 +0,0 @@
--- | ImProve examples.
-module Language.ImProve.Examples
-  ( buildGCD
-  , counter
-  , verifyCounter
-  , arbiterSpec
-  , arbiter
-  , arbiter1
-  , arbiter2
-  , arbiter3
-  , verifyArbiters
-  , buildArbiters
-  , runAll
-  ) where
-
-import Language.ImProve
-
--- | Computes the greatest common divison of two integers.
---   Returns true if the computation is done, and the result.
-gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)
-gcd' a b = do
-  a0 <- int "a0" 0  -- Copy of input 'a'.
-  b0 <- int "b0" 0  -- Copy of input 'b'.
-  a1 <- int "a1" 0  -- Working copy of 'a'.
-  b1 <- int "b1" 0  -- Working copy of 'b'.
-
-  -- A new input to process.
-  "startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do
-    a0 <== a
-    b0 <== b
-    a1 <== a
-    b1 <== b
-
-  -- Reduce a1.
-  "reduceA" -| if_ (ref a1 >. ref b1) $ do
-    a1 <== ref a1 - ref b1
-
-  -- Reduce b1.
-  "reduceB" -| if_ (ref b1 >. ref a1) $ do
-    b1 <== ref b1 - ref a1
-
-  -- Done if a1 == b1.
-  return (ref a1 ==. ref b1, ref a1)
-
-
--- | A top level wrapper for gcd'.
-gcdMain :: Stmt ()
-gcdMain = do
-  let a = input int ["a"]  -- Input variable 'a'.
-      b = input int ["b"]  -- Input variable 'b'.
-  done   <- bool "done"   False  -- Variable signalling completion.
-  result <- int  "result" 0      -- Result of GCD.
-
-  -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)
-  (done', result') <- "gcd" -| gcd' a b
-
-  -- Bind the results to the output variables.
-  done   <== done'
-  result <== result'
-
--- | Build the gcdMain code (i.e. gcd.c, gcd.h).
-buildGCD :: IO ()
-buildGCD = code "gcd" gcdMain
-
-
-
--- | A rolling counter verification example.
-counter :: Stmt ()
-counter = do
-  -- The counter variable.
-  counter <- int "counter" 0
-
-  -- Specification.
-  "GreaterThanOrEqualTo0" -| assert $ ref counter >=. 0
-  "LessThan10"            -| assert $ ref counter <.  10
-
-  -- Implementation.
-  ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
-
-  -- Alternatives to try.
-  --ifelse "ResetCounter" (ref counter >=. 9) (counter <== 0) (counter <== ref counter + 1)
-  --ifelse "ResetCounter" (ref counter >=. 9 ||. ref counter <. 0)  (counter <== 0) (counter <== ref counter + 1)
-
--- | Verify the 'counter' example.
-verifyCounter :: IO ()
-verifyCounter = verify "yices" 20 counter
-
-
-
--- | Arbiter specification.
-arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
-arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
-
-  -- Mutual exclusion.  At most, only one requester granted at a time.
-  "OneHot" -| assert $      grantA &&. not_ grantB &&. not_ grantC
-                   ||. not_ grantA &&.      grantB &&. not_ grantC
-                   ||. not_ grantA &&. not_ grantB &&.      grantC
-                   ||. not_ grantA &&. not_ grantB &&. not_ grantC
-  
-  -- No grants without requests.
-  "NotRequestedA" -| assert $ not_ requestA --> not_ grantA
-  "NotRequestedB" -| assert $ not_ requestB --> not_ grantB
-  "NotRequestedC" -| assert $ not_ requestC --> not_ grantC
-
-  -- Grants to single requests.
-  "OnlyRequestA" -| assert $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA
-  "OnlyRequestB" -| assert $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB
-  "OnlyRequestC" -| assert $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC
-
-  -- Priority.
-  "Highest" -| assert $ requestA --> grantA
-  "Medium"  -| assert $ (not_ requestA &&. requestB) --> grantB
-  "Lowest"  -| assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
-
--- | An arbiter implementation.
-arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter1 (requestA, requestB, requestC) = do
-  let grantA = requestA
-      grantB = requestB
-      grantC = requestC
-  return (grantA, grantB, grantC)
-
--- | An another arbiter implementation.
-arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter2 (requestA, requestB, requestC) = do
-  grantA <- bool "grantA" False
-  grantB <- bool "grantB" False
-  grantC <- bool "grantC" False
-
-  "GrantA" -| if_ (requestA)                                     (grantA <== true)
-  "GrantB" -| if_ (not_ requestA &&. requestB)                   (grantB <== true)
-  "GrantC" -| if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
-
-  return (ref grantA, ref grantB, ref grantC)
-
--- | Yet another arbiter implementation.
-arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter3 (requestA, requestB, requestC) = do
-  let grantA = requestA
-      grantB = not_ requestA &&. requestB
-      grantC = not_ requestA &&. not_ requestB &&. requestC
-  return (grantA, grantB, grantC)
-
--- | Binding an arbiter implemenation to the arbiter specification.
-arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
-arbiter name implementation = name -| do
-  -- Create input variables.
-  let requestA = input bool ["requestA"]
-      requestB = input bool ["requestB"]
-      requestC = input bool ["requestC"]
-  let requests = (requestA, requestB, requestC)
-
-  -- Instantiate implementation.
-  grants@(grantA, grantB, grantC) <- "impl" -| implementation requests
-
-  -- Bind specification.
-  arbiterSpec requests grants
-
-  -- Create output variables.
-  bool' "grantA" grantA
-  bool' "grantB" grantB
-  bool' "grantC" grantC
-  return ()
-
--- | Verify the different arbiter implementations.
-verifyArbiters :: IO ()
-verifyArbiters = do
-  putStrLn "\nVerifying arbiter1 ..."
-  verify "yices" 20 $ arbiter "arbiter1" arbiter1
-
-  putStrLn "\nVerifying arbiter2 ..."
-  verify "yices" 20 $ arbiter "arbiter2" arbiter2
-
-  putStrLn "\nVerifying arbiter2 ..."
-  verify "yices" 20 $ arbiter "arbiter3" arbiter3
-
--- | Build the different arbiter implementations.
-buildArbiters :: IO ()
-buildArbiters = do
-  putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."
-  code "arbiter1" $ arbiter "arbiter1" arbiter1
-
-  putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."
-  code "arbiter2" $ arbiter "arbiter2" arbiter2
-
-  putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."
-  code "arbiter3" $ arbiter "arbiter3" arbiter3
-
--- | Run all examples.
-runAll :: IO ()
-runAll = do
-  putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."
-  buildGCD
-  putStrLn "\nVerifying counter ..."
-  verifyCounter
-  putStrLn "\nVerifying arbiters ..."
-  verifyArbiters
-  putStrLn "\nBuilding arbiters ..."
-  buildArbiters
-
diff --git a/Language/ImProve/Narrow.hs b/Language/ImProve/Narrow.hs
deleted file mode 100644
--- a/Language/ImProve/Narrow.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-module Language.ImProve.Narrow (narrow) where
-
-import Data.List
-import Data.Maybe
-
-import Language.ImProve.Core
-
-narrow :: Statement -> Statement
-narrow stmt = assumes
-  where
-  assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]
-  optimizations =
-    [ ("constantAssigns", constantAssigns)
-    , ("timerRanges",     timerRanges)
-    ]
-
-constantAssigns :: Statement -> [E Bool]
-constantAssigns stmt = mapMaybe f1 $ stmtVars stmt
-  where
-  f1 :: UV -> Maybe (E Bool)
-  f1 uv
-    | input = Nothing
-    | otherwise = do
-      assigns <- lastConstAssign uv stmt
-      case (init, nub $ init : assigns) of
-        (Bool _, [_, _]) -> Nothing
-	(_, a) -> return $ foldl1 Or $ map f2 a
-    where
-    f2 :: Const -> E Bool
-    f2 assign = case (init, assign) of
-      (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)
-      (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)
-      (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)
-      _ -> undefined
-    (input, path, init) = varInfo uv
-
-lastConstAssign :: UV -> Statement -> Maybe [Const]
-lastConstAssign uv a = do
-  (_, a) <- lastConstAssign a
-  return $ nub a
-  where
-  lastConstAssign :: Statement -> Maybe (Bool, [Const])
-  lastConstAssign a = case a of
-    Assign v (Const a) | untype v == uv -> Just (True, [const' a])
-    Assign v _         | untype v == uv -> Nothing
-    Branch _ a b -> do
-      (aDone, a) <- lastConstAssign a
-      (bDone, b) <- lastConstAssign b
-      return (aDone && bDone, a ++ b)
-    Sequence a b -> do
-      (bDone, b) <- lastConstAssign b
-      if bDone
-        then return (True, b)
-	else do
-          (aDone, a) <- lastConstAssign a
-          return (aDone, a ++ b)
-    Label  _ a -> lastConstAssign a
-    _ -> Just (False, [])
-
-timerRanges :: Statement -> [E Bool]
-timerRanges stmt = [] --XXX
-  where
-  intCode :: [(VarInfo, Statement)]
-  intCode = [ (varInfo a, assignedVar a stmt) | a@(UVInt _) <- stmtVars stmt ]
-
--- | Reduces a program only to assignments of a certain variable.
-assignedVar :: UV -> Statement -> Statement
-assignedVar v a = case a of
-  Assign v' _ | v == untype v' -> a
-  Branch cond a b -> case (assignedVar v a, assignedVar v b) of
-    (Null, Null) -> Null
-    (a, b)       -> Branch cond a b
-  Sequence a b -> case (assignedVar v a, assignedVar v b) of
-    (Null, Null) -> Null
-    (a, b)       -> Sequence a b
-  Label a b -> Label a $ assignedVar v b
-  _ -> Null
-
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -1,7 +1,6 @@
 module Language.ImProve.Verify (verify) where
 
 import Control.Monad.State
-import Data.List
 import Math.SMT.Yices.Pipe
 import Math.SMT.Yices.Syntax
 import System.IO
@@ -9,87 +8,38 @@
 
 import Language.ImProve.Code ()
 import Language.ImProve.Core
-import Language.ImProve.Narrow
 
 -- | Verify a program with k-induction.
-verify :: FilePath -> Int -> Statement -> IO ()
-verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"
-verify yices maxK program = do
-  putStrLn "state variable narrowing ..."
-  print $ narrow program
-  mapM_ (verifyProgram yices format maxK $ narrow program) $ trimAssertions $ labelAssertions program
-  where
-  format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "
-
--- | Set of statements containing only one assertion.
-trimAssertions :: Statement -> [Statement]
-trimAssertions program = [ a | a <- trimAssertions program, length (assertions a) == 1 ]
+verify :: FilePath -> Statement -> IO ()
+verify yices program = mapM_ (proveTheorem yices format program) $ theorems program
   where
-  trimAssertions :: Statement -> [Statement]
-  trimAssertions a = case a of
-    Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions a ]
-                 ++ [ Sequence (removeAssertions a) b | b <- trimAssertions b ]
-    Branch cond a b -> [ Branch cond a (removeAssertions b) | a <- trimAssertions a ]
-                    ++ [ Branch cond (removeAssertions a) b | b <- trimAssertions b ]
-    Label name a -> [ Label name a | a <- trimAssertions a ]
-    a -> [a]
-
--- | Remove all assertions.
-removeAssertions :: Statement -> Statement
-removeAssertions a = case a of
-  Assert _ -> Null
-  Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)
-  Branch cond a b -> Branch cond (removeAssertions a) (removeAssertions b)
-  Label name a -> Label name $ removeAssertions a
-  a -> a
+  format = "%-" ++ show (maximum [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s    "
 
--- | Ensure all assertions are uniquely labed.
-labelAssertions :: Statement -> Statement
-labelAssertions program = evalState (f program) ([], [], 1)
+-- | Path of a theorem.
+theoremPath :: Int -> Statement -> Path
+theoremPath t stmt = case f stmt of
+  Nothing -> error $ "theorem not found: " ++ show t
+  Just p  -> p
   where
-  f :: Statement -> State (Path, [Path], Int) Statement
+  pair :: Statement -> Statement -> Maybe Path
+  pair a b = case (f a, f b) of
+    (Just a, _) -> Just a
+    (_, Just a) -> Just a
+    _ -> Nothing
+  f :: Statement -> Maybe Path
   f a = case a of
-    Branch a b c -> do
-      b <- f b
-      c <- f c
-      return $ Branch a b c
-    Sequence a b -> do
-      a <- f a
-      b <- f b
-      return $ Sequence a b
-    Assert a -> do
-      (path, paths, n) <- get
-      if elem path paths
-        then do
-          put (path, paths, n + 1)
-          f $ Label (show n) $ Assert a
-        else do
-          put (path, path : paths, n)
-          return $ Assert a
+    Theorem t' _ _ _ | t == t' -> Just [show t']
+    Sequence a b -> pair a b
+    Branch _ a b -> pair a b
     Label name a -> do
-      (path, paths, n) <- get
-      put (path ++ [name], paths, n)
-      a <- f a
-      (_, paths, n) <- get
-      put (path, paths, n)
-      return $ Label name a
-    a -> return a
-
--- | Paths of all assertions.
-assertions :: Statement -> [Path]
-assertions = assertions []
-  where
-  assertions :: Path -> Statement -> [Path]
-  assertions path a = case a of
-    Assert _ -> [path]
-    Sequence a b -> assertions path a ++ assertions path b
-    Branch _ a b -> assertions path a ++ assertions path b
-    Label name a -> assertions (path ++ [name]) a
-    _ -> []
+      path <- f a
+      return $ name : path
+    _ -> Nothing
 
+{-
 -- | Trim all unneeded stuff from a program.
-trimProgram :: Statement -> Statement -> Statement
-trimProgram base program = trim program
+trimProgram :: Int -> Statement -> Statement
+trimProgram t program = trim program
   where
   vars = fixPoint []
   fixPoint :: [UV] -> [UV]
@@ -134,47 +84,47 @@
   Assume _        -> []
   Label  _ a      -> modifiedVars a
   Null            -> []
+-}
 
--- | Verify a trimmed program.
-verifyProgram :: FilePath -> String -> Int -> Statement -> Statement -> IO ()
-verifyProgram yices format maxK narrowing program' = do
+-- | Prove a single theorem.
+proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO ()
+proveTheorem yices format program (id, k, lemmas, _) = do
   printf format name
   hFlush stdout
-  env0 <- initEnv program  --XXX Need to add narrowing assumptions.
-  execStateT (check yices name maxK program env0 1) env0
+  env0 <- initEnv program
+  execStateT (check yices name id lemmas program env0 k) env0
   return ()
   where
-  program = Sequence (trimProgram program' narrowing) (trimProgram program' program')
-  name = pathName $ head' "a1" $ assertions program
-
-head' msg a = if null a then error msg else head a
+  name = pathName $ theoremPath id program
 
 data Result = Pass | Fail [ExpY] | Problem
 
 -- | k-induction.
-check :: FilePath -> Name -> Int -> Statement -> Env -> Int -> Y ()
-check yices name maxK program env0 k = do
-  addTrace $ Cycle' $ k - 1
-  inputs program
-  evalStmt (LitB True) program
+check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y ()
+check yices name theorem lemmas program env0 k = do
+  sequence_ [ addTrace (Cycle' i) >> inputs program >> evalStmt theorem lemmas (LitB True) program | i <- [0 .. k - 1] ]
   resultBasis <- checkBasis yices program env0
   case resultBasis of
-    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see %s.trace)\n" k name) >> writeTrace name a
+    Fail a  -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace name a
     Problem -> error "Verify.check1"
     Pass -> do
       resultStep <- checkStep yices
       case resultStep of
-        Fail a | k < maxK  -> check yices name maxK program env0 (k + 1)
-               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see %s.trace)\n" k name) >> writeTrace name a
+        Fail a  -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace name a
         Problem -> error "Verify.check2"
-        Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
+        Pass    -> liftIO $ printf "proved\n"
         
 -- | Check induction step.
 checkStep :: FilePath -> Y Result
 checkStep yices = do
   env <- get
-  r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [ASSERT $ NOT $ head' "a2" $ asserts env] ++ [CHECK]
+  r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [assert env] ++ [CHECK]
   return $ result r
+  where
+  assert env = case asserts env of
+    [] -> error "unexpected: no assertion"
+    [a] -> ASSERT $ NOT $ a
+    a : b -> ASSERT $ NOT $ AND b :=> a
 
 -- | Check induction basis.
 checkBasis :: FilePath -> Statement -> Env -> Y Result
@@ -198,18 +148,23 @@
   _ -> error $ "unexpected yices results: " ++ show a
 
 
-evalStmt :: ExpY -> Statement -> Y ()
-evalStmt enabled a = case a of
+evalStmt :: Int -> [Int] -> ExpY -> Statement -> Y ()
+evalStmt theorem lemmas enabled a = case a of
   Null -> return ()
-  Sequence a b -> evalStmt enabled a >> evalStmt enabled b
+  Sequence a b -> evalStmt theorem lemmas enabled a >> evalStmt theorem lemmas enabled b
   Assign a b -> assign a b
-  Assert a -> do
-    a <- evalExpr a
-    b <- newBoolVar
-    addCmd $ ASSERT (VarE b := (enabled :=> a))
-    env <- get
-    put env { asserts = VarE b : asserts env }
-    addTrace $ Assert' b
+  Theorem id _ _ a
+    | elem id lemmas -> do
+      a <- evalExpr a
+      addCmd $ ASSERT (enabled :=> a)
+    | id == theorem -> do
+      a <- evalExpr a
+      b <- newBoolVar
+      addCmd $ ASSERT (VarE b := (enabled :=> a))
+      env <- get
+      put env { asserts = VarE b : asserts env }
+      addTrace $ Assert' b
+    | otherwise -> return ()
   Assume a -> do
     a <- evalExpr a
     addCmd $ ASSERT (enabled :=> a)
@@ -219,16 +174,16 @@
     addCmd $ ASSERT (VarE b := a)
     env0 <- get
     put env0 { trace = [] }
-    evalStmt (AND [enabled, a]) onTrue
+    evalStmt theorem lemmas (AND [enabled, a]) onTrue
     env1 <- get
     put env1 { trace = [] }
-    evalStmt (AND [enabled, NOT a]) onFalse
+    evalStmt theorem lemmas (AND [enabled, NOT a]) onFalse
     env2 <- get
     put env2 { trace = Branch' b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
   Label name a -> do
     env0 <- get
     put env0 { trace = [] }
-    evalStmt enabled a
+    evalStmt theorem lemmas enabled a
     env1 <- get
     put env1 { trace = Label' name (reverse $ trace env1) : trace env0 }
   where
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.1.6
+version: 0.2.0
 
 category: Language, Formal Methods, Embedded
 
@@ -32,8 +32,6 @@
         Language.ImProve
         Language.ImProve.Code
         Language.ImProve.Core
-        Language.ImProve.Examples
-        Language.ImProve.Narrow
         Language.ImProve.Tree
         Language.ImProve.Verify