diff --git a/Language/Nock5K.hs b/Language/Nock5K.hs
--- a/Language/Nock5K.hs
+++ b/Language/Nock5K.hs
@@ -1,5 +1,5 @@
-module Language.Nock5K (Noun(Atom, (:-)), Nock, nock, noun, repl) where
+module Language.Nock5K (Noun(..), Nock, nock, noun, repl) where
 
-import Language.Nock5K.Parse
-import Language.Nock5K.Repl
-import Language.Nock5K.Spec
+import Language.Nock5K.Parse (noun)
+import Language.Nock5K.Repl (repl)
+import Language.Nock5K.Spec (Noun(..), Nock, nock)
diff --git a/Language/Nock5K/Spec.hs b/Language/Nock5K/Spec.hs
--- a/Language/Nock5K/Spec.hs
+++ b/Language/Nock5K/Spec.hs
@@ -1,59 +1,63 @@
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 module Language.Nock5K.Spec where
+import Control.Monad.Instances
 
 -- * Structures
-{-|
+{-| #spec-l3#
   A noun is an atom or a cell.  An atom is any natural number.
   A cell is an ordered pair of nouns.
 -}
-data Noun = Atom Integer | Noun :- Noun deriving (Eq)
+data Noun = Atom !Integer | !Noun :- !Noun deriving (Eq)
 
--- | Either a computed result or an error message.
--- E.g. Nock Noun is either a Noun or an error.
+-- | Monad representing either a computed result or an error message.
 type Nock = Either String
-instance Monad Nock where
-  return = Right
-  fail = Left
-  Right n >>= f = f n
-  Left e >>= _ = Left e
 
 -- * Reductions
-{-|@
+nock, wut, lus, tis, fas, tar :: Noun -> Nock Noun
+
+{-| #spec-l8#
+
+@
   nock(a)           *a
 @-}
 nock = tar
 
-{-
+{- spec-l9
   [a b c]           [a [b c]]
 -}
 infixr 1 :-
 
-nock, wut, lus, tis, fas, tar :: Noun -> Nock Noun
+{-| #spec-l11#
 
-{-|@
+@
   ?[a b]            0
   ?a                1
 @-}
 wut (a :- b)  = return $ Atom 0
 wut a         = return $ Atom 1
 
-{-|@
+{-| #spec-l13#
+
+@
   +[a b]            +[a b]
   +a                1 + a
 @-}
-lus (a :- b)  = fail "+[a b]"
+lus (a :- b)  = Left "+[a b]"
 lus (Atom a)  = return $ Atom (1 + a)
 
-{-|@
+{-| #spec-l15#
+
+@
   =[a a]            0
   =[a b]            1
   =a                =a
 @-}
 tis (a :- a') | a == a'  = return $ Atom 0
 tis (a :- b)             = return $ Atom 1
-tis a                    = fail "=a"
+tis a                    = Left "=a"
 
-{-|@
+{-| #spec-l19#
+
+@
   \/[1 a]            a
   \/[2 a b]          a
   \/[3 a b]          b
@@ -61,18 +65,16 @@
   \/[(a + a + 1) b]  \/[3 \/[a b]]
   \/a                \/a
 @-}
-fas (Atom 1 :- a)       = return a
-fas (Atom 2 :- a :- b)  = return a
-fas (Atom 3 :- a :- b)  = return b
-fas (Atom a :- b) | a > 2 && a `mod` 2 == 0 = do
-  x <- fas $ Atom (a `div` 2) :- b
-  fas $ Atom 2 :- x
-fas (Atom a :- b) | a > 3 && a `mod` 2 == 1 = do
-  x <- fas $ Atom (a `div` 2) :- b
-  fas $ Atom 3 :- x
-fas a                   = fail "/a"
+fas (Atom 1 :- a)          = return a
+fas (Atom 2 :- a :- b)     = return a
+fas (Atom 3 :- a :- b)     = return b
+fas (Atom a :- b) | a > 3  = do  x <- fas $ Atom (a `div` 2) :- b
+                                 fas $ Atom (2 + (a `mod` 2)) :- x
+fas a                      = Left "/a"
 
-{-|@
+{-| #spec-l26#
+
+@
   \*[a [b c] d]      [\*[a b c] \*[a d]]
 
 \  \*[a 0 b]          \/[b a]
@@ -120,4 +122,4 @@
                                             (Atom 0 :- Atom 3) :- d)
 tar (a :- Atom 10 :- b :- c)         = tar (a :- c)
 
-tar a                                = fail "*a"
+tar a                                = Left "*a"
diff --git a/hsnock.cabal b/hsnock.cabal
--- a/hsnock.cabal
+++ b/hsnock.cabal
@@ -1,5 +1,5 @@
 name                 : hsnock
-version              : 0.4.1
+version              : 0.5.0
 category             : Language
 license              : PublicDomain
 synopsis             : Nock 5K interpreter.
diff --git a/test.hs b/test.hs
--- a/test.hs
+++ b/test.hs
@@ -34,6 +34,12 @@
     ifs c = Atom a :- Atom 6 :- (Atom 1 :- c) :- (Atom 4 :- Atom 0 :- Atom 1) :- (Atom 1 :- b)
     a = abs a'
 
+prop_fas_induct a' b = fas (a + a) b == fasmn 2 a b && fas (a + a + 1) b == fasmn 3 a b
+  where fas c d = nock $ d :- Atom c
+        fasmn m n c = do x <- fas n c
+                         fas m x
+        a = abs a'
+
 test_hint_crash = assert $ nock bad == Left "/a"
   where bad = pn "[42 10 [0 0 2] 0 1]"
 
@@ -43,6 +49,7 @@
 tests = [ testProperty "parse.show"    prop_parse_show
         , testProperty "decrement"     prop_dec
         , testProperty "6_is_if"       prop_6_is_if
+        , testProperty "fas_induct"    prop_fas_induct
         , testCase     "10_hint_crash" test_hint_crash
         , testCase     "eval_strict"   test_eval_strict
         ]