diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -57,7 +57,7 @@
 /Assertion Statements/
 
 @
-assert(condition);        'theorem' name k lemmas condition
+assert(condition);        'assert' name k condition
 @
 
 /Statement Labels/
@@ -148,7 +148,6 @@
   , AllE
   , NumE
   , Name
-  , Theorem
   -- * Expressions
   -- ** Constants
   , true
@@ -213,9 +212,9 @@
   -- ** Incrementing and decrementing.
   , incr
   , decr
-  -- ** Assumptions and theorems.
+  -- ** Assumptions and assertions.
   , assume
-  , theorem
+  , assert
   -- * Verification
   , verify
   -- * Code Generation
@@ -472,27 +471,22 @@
 class Assign a where (<==) :: V a -> E a -> Stmt ()
 instance AllE a => Assign a where a <== b = statement $ Assign a b
 
--- | Theorem to be proven or used as lemmas to assist proofs of other theorems.
-data Theorem = Theorem' Int
-
 -- | Assume a condition is true.
---   Assumptions are used as lemmas to other theorems.
-assume :: Name -> E Bool -> Stmt Theorem
+--   Assumptions are used as lemmas to other assertions.
+assume :: Name -> E Bool -> Stmt ()
 assume name a = do
   (id, path, stmt) <- get
   put (id + 1, path, Sequence stmt $ Label name $ Assume id a)
-  return $ Theorem' id
 
--- | Defines a new theorem.
+-- | Defines a new assertion.
 --
--- > theorem name k lemmas proposition
-theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem
-theorem name k lemmas proposition
+-- > assert name k proposition
+assert :: Name -> Int -> E Bool -> Stmt ()
+assert name k 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
+    put (id + 1, path, Sequence stmt $ Label name $ Assert id k proposition)
 
 -- | Conditional if-else.
 ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
diff --git a/Language/ImProve/Code/Ada.hs b/Language/ImProve/Code/Ada.hs
--- a/Language/ImProve/Code/Ada.hs
+++ b/Language/ImProve/Code/Ada.hs
@@ -55,11 +55,11 @@
   Assign a b -> name ++ "_Variables." ++ pathName a ++ " := " ++ codeExpr b ++ ";\n"
   Branch a b Null -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "end if;\n"
   Branch a b c    -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "\nelse\n" ++ indent (codeStmt name path c) ++ "end if;\n"
-  Sequence a b -> codeStmt name path a ++ codeStmt name path b
-  Theorem _ _ _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
+  Sequence a b    -> codeStmt name path a ++ codeStmt name path b
+  Assert _ _ a    -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
   Assume _ a      -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
-  Label name' a -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)
-  Null -> ""
+  Label name' a   -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)
+  Null            -> ""
   where
 
   codeExpr :: E a -> String
diff --git a/Language/ImProve/Code/C.hs b/Language/ImProve/Code/C.hs
--- a/Language/ImProve/Code/C.hs
+++ b/Language/ImProve/Code/C.hs
@@ -41,8 +41,8 @@
   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
-  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
-  Assume _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
+  Assert _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
+  Assume _ a   -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
   Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
   Null -> ""
   where
diff --git a/Language/ImProve/Code/Simulink.hs b/Language/ImProve/Code/Simulink.hs
--- a/Language/ImProve/Code/Simulink.hs
+++ b/Language/ImProve/Code/Simulink.hs
@@ -102,7 +102,7 @@
   Assign   a b     -> Assign a b
   Branch   a b c   -> Branch a (lowerConditionals (And cond a) b) (lowerConditionals (And cond $ Not a) c)
   Sequence a b     -> Sequence (lowerConditionals cond a) (lowerConditionals cond b)
-  Theorem  a b c d -> Theorem a b c $ Or (Not cond) d
+  Assert   a b c   -> Assert a b $ Or (Not cond) c
   Assume   i a     -> Assume i $ Or (Not cond) a
   Label    a b     -> Label a $ lowerConditionals cond b
   Null             -> Null
@@ -188,7 +188,7 @@
 
   Sequence a b    -> evalStmt a >> evalStmt b
 
-  Theorem _ _ _ a -> do
+  Assert _ _ a -> do
     a <- evalExpr a
     name <- getPathName
     assert <- block' name Assertion
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -14,7 +14,7 @@
   , varInfo
   , stmtVars
   , arrayLength
-  , theorems
+  , assertions
   ) where
 
 import Data.List
@@ -107,8 +107,8 @@
   Assign   :: AllE a => V a -> E a -> Statement
   Branch   :: E Bool -> Statement -> Statement -> Statement
   Sequence :: Statement -> Statement -> Statement
-  Theorem  :: Int -> Int -> [Int] -> E Bool -> Statement -- Theorem id k lemmas expr
-  Assume   :: Int -> E Bool -> Statement                 -- Assume id expr
+  Assert   :: Int -> Int -> E Bool -> Statement -- Assert id k expr
+  Assume   :: Int -> E Bool -> Statement        -- Assume id expr
   Label    :: Name -> Statement -> Statement
   Null     :: Statement
 
@@ -127,13 +127,13 @@
 -- | Variables in a program.
 stmtVars :: Statement -> [VarInfo]
 stmtVars a = case a of
-  Assign a b   -> nub $ varInfo a : exprVars b
-  Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
-  Sequence a b -> nub $ stmtVars a ++ stmtVars b
-  Theorem _ _ _ a -> exprVars a
-  Assume  _ a     -> exprVars a
-  Label  _ a   -> stmtVars a
-  Null         -> []
+  Assign a b    -> nub $ varInfo 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
+  Assume  _ a   -> exprVars a
+  Label  _ a    -> stmtVars a
+  Null          -> []
 
 -- | Variables in an expression.
 exprVars :: E a -> [VarInfo]
@@ -155,14 +155,14 @@
   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)]
+-- | Assertions in a program.
+assertions :: Statement -> [(Int, Int, E Bool)]
+assertions a = case a of
+  Assert id k expr -> [(id, k, expr)]
   Assign _ _   -> []
-  Branch _ a b -> theorems a ++ theorems b
-  Sequence a b -> theorems a ++ theorems b
+  Branch _ a b -> assertions a ++ assertions b
+  Sequence a b -> assertions a ++ assertions b
   Assume _ _   -> []
-  Label  _ a   -> theorems a
+  Label  _ a   -> assertions a
   Null         -> []
 
diff --git a/Language/ImProve/Path.hs b/Language/ImProve/Path.hs
--- a/Language/ImProve/Path.hs
+++ b/Language/ImProve/Path.hs
@@ -14,7 +14,7 @@
   Assign _ _      -> 1
   Branch _ a b    -> paths a + paths b
   Sequence a b    -> paths a * paths b
-  Theorem _ _ _ _ -> 1
+  Assert _ _ _ -> 1
   Assume  _ _     -> 1
   Label  _ a      -> paths a
   Null            -> 1
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -12,13 +12,13 @@
 
 -- | Verify a program with k-induction.
 verify :: FilePath -> Statement -> IO ()
-verify yices program = mapM_ (proveTheorem yices format program) $ theorems program
+verify yices program = proveAssertions yices format program [] $ assertions program
   where
-  format = "%-" ++ show (maximum' [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s    "
+  format = "%-" ++ show (maximum' [ length $ pathName $ assertionPath t program | (t, _, _) <- assertions program ]) ++ "s    "
 
--- | Path of a theorem.
-theoremPath :: Int -> Statement -> Path
-theoremPath t stmt = case f stmt of
+-- | Path of an assertion.
+assertionPath :: Int -> Statement -> Path
+assertionPath t stmt = case f stmt of
   Nothing -> error $ "theorem not found: " ++ show t
   Just p  -> p
   where
@@ -29,7 +29,7 @@
     _ -> Nothing
   f :: Statement -> Maybe Path
   f a = case a of
-    Theorem t' _ _ _ | t == t' -> Just []
+    Assert t' _ _ | t == t' -> Just []
     Sequence a b -> pair a b
     Branch _ a b -> pair a b
     Label name a -> do
@@ -37,34 +37,42 @@
       return $ name : path
     _ -> Nothing
 
--- | Prove a single theorem.
-proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO ()
-proveTheorem yices format program (id, k, lemmas, _) = do
+proveAssertions :: FilePath -> String -> Statement -> [Int] -> [(Int, Int, E Bool)] -> IO ()
+proveAssertions _ _ _ _ [] = return ()
+proveAssertions yices format program lemmas ((id, k, _) : rest) = do
   printf format name
   hFlush stdout
   env0 <- initEnv program
-  execStateT (check yices name id lemmas program env0 k) env0
-  return ()
+  pass <- evalStateT (check yices name id lemmas program env0 k) env0
+  proveAssertions yices format program (if pass then id : lemmas else lemmas) rest
   where
-  name = pathName $ theoremPath id program
+  name = pathName $ assertionPath id program
 
 data Result = Pass | Fail [ExpY] | Problem
 
 -- | k-induction.
-check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y ()
+check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y Bool
 check yices name theorem lemmas program env0 k = do
   mapM_ step [0 .. k - 1]
   resultBasis <- checkBasis yices program env0
   case resultBasis of
-    Fail a  -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace name a
+    Fail a  -> do
+      liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name)
+      writeTrace name a
+      return False
     Problem -> error "Verify.check1"
     Pass -> do
       step k
       resultStep <- checkStep yices
       case resultStep of
-        Fail a  -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace name a
+        Fail a  -> do
+	  liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name)
+	  writeTrace name a
+	  return False
         Problem -> error "Verify.check2"
-        Pass    -> liftIO $ printf "proved\n"
+        Pass    -> do
+	  liftIO $ printf "proved\n"
+	  return True
   where
   step :: Int -> Y ()
   step i = do
@@ -110,7 +118,7 @@
   Null -> return ()
   Sequence a b -> evalStmt theorem lemmas enabled a >> evalStmt theorem lemmas enabled b
   Assign a b -> assign a b
-  Theorem id _ _ a
+  Assert id _ a
     | elem id lemmas -> do
       a <- evalExpr a
       addCmd $ ASSERT (enabled :=> a)
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.3.4
+version: 0.4.0
 
 category: Language, Formal Methods, Embedded