diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Examples.hs
@@ -0,0 +1,198 @@
+-- | 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.
+  theorem "GreaterThanOrEqualTo0" 1 [] $ ref counter >=. 0
+  theorem "LessThan10"            1 [] $ ref counter <=. 9
+
+  -- Implementation.
+  ifelse (ref counter ==. 9) (counter <== 0) (counter <== ref counter + 1)
+
+-- | Verify the 'counter' example.
+verifyCounter :: IO ()
+verifyCounter = verify "yices" 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.
+  theorem "OneHot" 1 [] $      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.
+  theorem "NotRequestedA" 1 [] $ not_ requestA --> not_ grantA
+  theorem "NotRequestedB" 1 [] $ not_ requestB --> not_ grantB
+  theorem "NotRequestedC" 1 [] $ not_ requestC --> not_ grantC
+
+  -- Grants to single requests.
+  theorem "OnlyRequestA" 1 [] $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA
+  theorem "OnlyRequestB" 1 [] $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB
+  theorem "OnlyRequestC" 1 [] $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC
+
+  -- Priority.
+  theorem "Highest" 1 [] $ requestA --> grantA
+  theorem "Medium"  1 [] $ (not_ requestA &&. requestB) --> grantB
+  theorem "Lowest"  1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
+
+  return ()
+
+-- | 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" $ arbiter "arbiter1" arbiter1
+
+  putStrLn "\nVerifying arbiter2 ..."
+  verify "yices" $ arbiter "arbiter2" arbiter2
+
+  putStrLn "\nVerifying arbiter2 ..."
+  verify "yices" $ 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/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -1,6 +1,7 @@
 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
@@ -13,7 +14,7 @@
 verify :: FilePath -> Statement -> IO ()
 verify yices program = mapM_ (proveTheorem yices format program) $ theorems program
   where
-  format = "%-" ++ show (maximum [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s    "
+  format = "%-" ++ show (maximum' [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s    "
 
 -- | Path of a theorem.
 theoremPath :: Int -> Statement -> Path
@@ -28,7 +29,7 @@
     _ -> Nothing
   f :: Statement -> Maybe Path
   f a = case a of
-    Theorem t' _ _ _ | t == t' -> Just [show t']
+    Theorem t' _ _ _ | t == t' -> Just []
     Sequence a b -> pair a b
     Branch _ a b -> pair a b
     Label name a -> do
@@ -36,56 +37,6 @@
       return $ name : path
     _ -> Nothing
 
-{-
--- | Trim all unneeded stuff from a program.
-trimProgram :: Int -> Statement -> Statement
-trimProgram t program = trim program
-  where
-  vars = fixPoint []
-  fixPoint :: [UV] -> [UV]
-  fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b
-    where
-    b = requiredVars base a
-  trim :: Statement -> Statement
-  trim a = case a of
-    Null -> Null
-    Assign b _ -> if elem (untype b) vars then a else Null
-    Branch a b c    -> case (trim b, trim c) of
-      (Null, Null) -> Null
-      (b, c)       -> Branch a b c
-    Sequence a b    -> case (trim a, trim b) of
-      (Null, a) -> a
-      (a, Null) -> a
-      (a, b)    -> Sequence a b
-    Assert a -> Assert a
-    Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null
-    Label name a -> case trim a of
-      Null -> Null
-      a    -> Label name a
-
-requiredVars :: Statement -> [UV] -> [UV]
-requiredVars a required = case a of
-  Assign a b -> if elem (untype a) required then nub $ untype a : exprVars b ++ required else required
-  Branch a b c    -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required || (not $ null $ requiredVars b []) || (not $ null $ requiredVars c [])
-    then nub $ exprVars a ++ requiredVars b (requiredVars c required)
-    else required
-  Sequence a b    -> requiredVars a (requiredVars b required)
-  Assert a        -> nub $ exprVars a ++ required
-  Assume a        -> if any (flip elem required) (exprVars a) then nub $ exprVars a ++ required else required
-  Label  _ a      -> requiredVars a required
-  Null            -> required
-
-modifiedVars :: Statement -> [UV]
-modifiedVars a = case a of
-  Assign a _      -> [untype a]
-  Branch _ b c    -> modifiedVars b ++ modifiedVars c
-  Sequence a b    -> modifiedVars a ++ modifiedVars b
-  Assert _        -> []
-  Assume _        -> []
-  Label  _ a      -> modifiedVars a
-  Null            -> []
--}
-
 -- | Prove a single theorem.
 proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO ()
 proveTheorem yices format program (id, k, lemmas, _) = do
@@ -102,24 +53,26 @@
 -- | k-induction.
 check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y ()
 check yices name theorem lemmas program env0 k = do
-  mapM_ step [0 .. k - 1]
+  replicateM_ k step
   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  -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace False name a
     Problem -> error "Verify.check1"
     Pass -> do
-      step k
+      step
       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  -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace True name a
         Problem -> error "Verify.check2"
         Pass    -> liftIO $ printf "proved\n"
   where
-  step :: Int -> Y ()
-  step i = do
-      addTrace $ Cycle' i
-      inputs program
+  step :: Y ()
+  step = do
+      addTrace $ Step' 0
+      sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program, not input ]
+      sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program,     input ]
       evalStmt theorem lemmas (LitB True) program
+  f (_, a, _) (_, b, _) = compare a b
 
 -- | Check induction step.
 checkStep :: FilePath -> Y Result
@@ -143,10 +96,6 @@
           ++ [CHECK]
   return $ result r
 
--- | Insert new input variables.
-inputs :: Statement -> Y ()
-inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, input ]
-
 result :: ResY -> Result
 result a = case a of
   Sat a   -> Fail a
@@ -285,7 +234,7 @@
   }
  
 initEnv :: Statement -> IO Env
-initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, not input ]) Env
+initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- map varInfo $ stmtVars program, not input ]) Env
   { nextId  = 0
   , var     = \ v -> error $ "variable not found in environment: " ++ pathName v
   , cmds    = []
@@ -294,8 +243,8 @@
   }
 
 data Trace
-  = Init'   Name Var
-  | Cycle'  Int
+  = Step'  Int
+  | State'  Name Var
   | Input'  Name Var
   | Assign' Name Var
   | Assert' Var
@@ -335,41 +284,66 @@
   env <- get
   put env { trace = t : trace env }
 
-getVar :: AllE a => V a -> Y String
-getVar v = do
+getVar :: AllE a => V a -> Y Var
+getVar v = getVar' $ varInfo v
+
+getVar' :: VarInfo -> Y Var
+getVar' v = do
   env <- get
-  return $ var env $ varInfo v
+  return $ var env $ v
 
-writeTrace :: String -> [ExpY] -> Y ()
-writeTrace name table' = do
+writeTrace :: Bool -> String -> [ExpY] -> Y ()
+writeTrace dropFirst name table' = do
   env <- get
-  liftIO $ writeFile (name ++ ".trace") $ concatMap f $ reverse $ trace env
+  let trace'' = reverse $ trace env
+      trace' = reorderSteps 1 $ if dropFirst then dropWhile notStep $ tail trace'' else trace''
+      format path indent = printf (printf "%%-%ds : %%s" $ maximum' $ 12 : map maxLabelWidth trace') (intercalate "." path) indent
+      varFormat :: Name -> String
+      varFormat = printf $ printf "%%-%ds" l
+        where
+        l = maximum $ 0 : map length ([ n | State' n _ <- trace' ] ++ [ n | Input' n _ <- trace' ])
+  liftIO $ writeFile (name ++ ".trace") $ concatMap (f varFormat format [] "") trace'
   where
+  notStep (Step' _) = False
+  notStep _ = True
+
+  reorderSteps :: Int -> [Trace] -> [Trace]
+  reorderSteps _ [] = []
+  reorderSteps n (Step' _ : a) = Step' n : reorderSteps (n + 1) a
+  reorderSteps n (a : b) = a : reorderSteps n b
+
   table = [ (n, if v then "true" else "false") | VarE n := LitB v <- table' ]
        ++ [ (n, show v) | VarE n := LitI v <- table' ]
        ++ [ (n, show v) | VarE n := LitR v <- table' ]
-  f :: Trace -> String
-  f a = case a of
-    Init' path var -> case lookup var table of
+
+  f :: (String -> String) -> (Path -> String -> String) -> Path -> String -> Trace -> String
+  f varFormat format path' indent a = case a of
+    Step' n -> "(step " ++ show n ++ ")\n"
+    State' path var -> case lookup var table of
       Nothing -> ""
-      Just value -> "initialize " ++ path ++ " <== " ++ value ++ "\n"
-    Cycle' n -> "\nstep " ++ show n ++ "\n"
+      Just value -> format ["(state)"] indent ++ varFormat path ++ " == " ++ value ++ "\n"
     Input' path var -> case lookup var table of
       Nothing -> ""
-      Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"
+      Just value -> format ["(input)"] indent ++ varFormat path ++ " <== " ++ value ++ "\n"
     Assign' path var -> case lookup var table of
       Nothing -> ""
-      Just value -> path ++ " <== " ++ value ++ "\n"
+      Just value -> format path' indent ++ path ++ " <== " ++ value ++ "\n"
     Assert' var -> case lookup var table of
-      Just "true"  -> "assertion passed\n"
-      Just "false" -> "assertion FAILED\n"
+      Just "true"  -> format path' indent ++ "theorem assertion passed\n"
+      Just "false" -> format path' indent ++ "theorem assertion FAILED\n"
       _ -> ""
     Branch' cond onTrue onFalse -> case lookup cond table of
-      Just "true"  -> "ifelse true:\n"  ++ indent (concatMap f onTrue)
-      Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse)
+      Just "true"  -> format path' indent ++ "ifelse true:\n"  ++ concatMap (f varFormat format path' $ "    " ++ indent) onTrue
+      Just "false" -> format path' indent ++ "ifelse false:\n" ++ concatMap (f varFormat format path' $ "    " ++ indent) onFalse
       _ -> ""
-    Label' name traces -> name ++ " |-\n" ++ indent (concatMap f traces)
+    Label' name traces -> concatMap (f varFormat format (path' ++ [name]) indent) traces
 
-indent :: String -> String
-indent = unlines . map ("    " ++) . lines
+maxLabelWidth :: Trace -> Int
+maxLabelWidth a = case a of
+  Branch' _ a b -> maximum' $ map maxLabelWidth $ a ++ b
+  Label' a b -> length a + 1 + maximum' (map maxLabelWidth b)
+  _ -> 0
 
+maximum' :: [Int] -> Int
+maximum' [] = 0
+maximum' a = maximum a
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.2.1
+version: 0.2.2
 
 category: Language, Formal Methods, Embedded
 
@@ -8,8 +8,7 @@
 description:
   ImProve is an imperative programming language for high assurance applications.
   ImProve uses infinite state, unbounded model checking to verify programs adhere
-  to specifications, which are written in the form of assertion statements.
-  Yices (required) is the backend SMT solver.
+  to specifications.  Yices (required) is the backend SMT solver.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>
@@ -32,6 +31,7 @@
         Language.ImProve
         Language.ImProve.Code
         Language.ImProve.Core
+        Language.ImProve.Examples
         Language.ImProve.Tree
         Language.ImProve.Verify