diff --git a/examples/Build.hs b/examples/Build.hs
index 14c0dcb..2a667c2 100644
--- a/examples/Build.hs
+++ b/examples/Build.hs
@@ -105,7 +105,9 @@ fetch key = liftSelect $ Fetch key id
 -- | Analyse a build task via free selective functors.
 --
 -- @
--- runBuild (fromJust $ cyclic "B1") == [Fetch "C1" (const ()),Fetch "B2",Fetch "A2"]
+-- runBuild (fromJust $ cyclic "B1") == [ Fetch "C1" (const ())
+--                                      , Fetch "B2" (const ())
+--                                      , Fetch "A2" (const ()) ]
 -- @
 runBuild :: Task k v -> [Fetch k v ()]
 runBuild task = getEffects (run task fetch)
diff --git a/examples/Processor.hs b/examples/Processor.hs
index 00a40c1..fa3813a 100644
--- a/examples/Processor.hs
+++ b/examples/Processor.hs
@@ -4,6 +4,7 @@ module Processor where
 import Control.Selective
 import Control.Selective.Rigid.Free
 import Data.Functor
+import Data.Bool
 import Data.Int (Int16)
 import Data.Word (Word8)
 import Data.Map.Strict (Map)
@@ -32,16 +33,10 @@ fromBool False = 0
 type Value = Int16
 
 -- | The processor has four registers.
-data Reg = R0 | R1 | R2 | R3 deriving (Show, Eq, Ord)
-
-r0, r1, r2, r3 :: Key
-r0 = Reg R0
-r1 = Reg R1
-r2 = Reg R2
-r3 = Reg R3
+data Register = R0 | R1 | R2 | R3 deriving (Show, Eq, Ord)
 
 -- | The register bank maps registers to values.
-type RegisterBank = Map Reg Value
+type RegisterBank = Map Register Value
 
 -- | The address space is indexed by one byte.
 type Address = Word8
@@ -55,7 +50,7 @@ data Flag = Zero     -- ^ tracks if the result of the last arithmetical operatio
     deriving (Show, Eq, Ord)
 
 -- | A flag assignment.
-type Flags = Map.Map Flag Value
+type Flags = Map Flag Value
 
 -- | Address in the program memory.
 type InstructionAddress = Value
@@ -77,7 +72,7 @@ data State = State { registers :: RegisterBank
                    , log       :: Log Key Value}
 
 -- | Various elements of the processor state.
-data Key = Reg Reg | Cell Address | Flag Flag | PC deriving Eq
+data Key = Reg Register | Cell Address | Flag Flag | PC deriving Eq
 
 instance Show Key where
     show (Reg r)  = show r
@@ -99,8 +94,7 @@ instance Show (RW a) where
     show (Write k _        _) = "Write " ++ show k
 
 logEntry :: MonadState State m => LogEntry Key Value -> m ()
-logEntry item = S.modify $ \s ->
-    s {log = log s ++ [item] }
+logEntry item = S.modify $ \s -> s { log = log s ++ [item] }
 
 -- | Interpret the base functor in a 'MonadState'.
 toState :: MonadState State m => RW a -> m a
@@ -146,51 +140,31 @@ read k = liftSelect (Read k id)
 write :: Key -> Program Value -> Program Value
 write k fv = liftSelect (Write k fv id)
 
--- --------------------------------------------------------------------------------
--- -------- Instructions ----------------------------------------------------------
--- --------------------------------------------------------------------------------
-
-------------
--- Add -----
-------------
+--------------------------------------------------------------------------------
+-------- Instructions ----------------------------------------------------------
+--------------------------------------------------------------------------------
 
--- | Read the values @x@ and @y@ and write the sum into @z@. If the sum is zero,
--- set the 'Zero' flag, otherwise reset it.
---
--- This implementation looks intuitive, but is incorrect, since the two write
--- operations are independent and the effects required for computing the sum,
--- i.e. @read x <*> read y@ will be executed twice. Consequently:
---   * the value written into @z@ is not guaranteed to be the same as the one
---     which was compared to zero,
---   * the static analysis of the computations would report more dependencies
---     than one might expect.
-addNaive :: Key -> Key -> Key -> Program Value
-addNaive x y z =
-    let sum    = (+)   <$> read x <*> read y
-        isZero = (==0) <$> sum
-    in write (Flag Zero) (ifS isZero (pure 1) (pure 0)) *> write z sum
-
--- | This implementation of addition executes the effects associated with 'sum'
--- only once and then reuses it without triggering the effects again.
-add :: Key -> Key -> Key -> Program Value
-add x y z =
-    let sum    = (+)   <$> read x <*> read y
-        isZero = (==0) <$> write z sum
-    in write (Flag Zero) (fromBool <$> isZero)
-
------------------
--- jumpZero -----
------------------
+-- | The addition instruction, which reads the summands from a 'Register' and a
+-- memory 'Address', adds them, writes the result back into the same register,
+-- and also updates the state of the 'Zero' flag to indicate whether the
+-- resulting 'Value' is zero.
+add :: Register -> Address -> Program Value
+add reg addr = let arg1   = read (Reg reg)
+                   arg2   = read (Cell addr)
+                   result = (+)   <$> arg1 <*> arg2
+                   isZero = (==0) <$> write (Reg reg) result
+               in write (Flag Zero) (bool 0 1 <$> isZero)
+
+-- | A conditional branching instruction that performs a jump if the result of
+-- the previous operation was zero.
 jumpZero :: Value -> Program ()
-jumpZero offset =
-    let pc       = read PC
-        zeroSet  = (==1) <$> read (Flag Zero)
-        modifyPC = void $ write PC ((+offset) <$> pc)
-    in whenS zeroSet modifyPC
+jumpZero offset = let zeroSet  = (==1) <$> read (Flag Zero)
+                      modifyPC = void $ write PC ((+offset) <$> read PC)
+                  in whenS zeroSet modifyPC
 
--- A block of instructions.
+-- | A simple block of instructions.
 addAndJump :: Program ()
-addAndJump = add (Reg R1) (Reg R2) (Reg R3) *> jumpZero 42
+addAndJump = add R0 1 *> jumpZero 42
 
 -----------------------------------
 -- Add with overflow tracking -----
@@ -241,9 +215,6 @@ willOverflowPure x y =
 -- overflow detection, lift all the pure operations into 'Applicative'. This
 -- forces the semantics to read the input variables more times than
 -- 'addOverflow' does (@x@ is read 3x times, and @y@ is read 5x times).
---
--- It is not clear at the moment what to do with this. Should we just avoid this
--- style? Or could it sometimes be useful?
 addOverflowNaive :: Key -> Key -> Key -> Program Value
 addOverflowNaive x y z =
     let arg1   = read x
@@ -293,13 +264,10 @@ boot mem = State { registers = emptyRegisters
                  , pc = 0
                  , flags = emptyFlags
                  , memory = mem
-                 , log   = []
-                 }
+                 , log   = [] }
 
 twoAdds :: Program Value
-twoAdds = add r0 (Cell 0) r0
-          *>
-          add r0 (Cell 0) r0
+twoAdds = add R0 0 *> add R0 0
 
 addExample :: IO ()
 addExample = do
diff --git a/examples/Teletype.hs b/examples/Teletype.hs
index 90133f5..2a5b3a4 100644
--- a/examples/Teletype.hs
+++ b/examples/Teletype.hs
@@ -38,7 +38,9 @@ getLine = liftSelect (Read id)
 putStrLn :: String -> Teletype ()
 putStrLn s = liftSelect (Write s ())
 
--- | The example from the paper's intro implemented using the free selective.
+-- | The ping-pong example from the introduction section of the paper
+-- implemented using free selective functors.
+--
 -- It can be statically analysed for effects:
 --
 -- @
@@ -64,11 +66,13 @@ pingPongS :: Teletype ()
 pingPongS = whenS (fmap ("ping"==) getLine) (putStrLn "pong")
 
 ------------------------------- Ping-pong example ------------------------------
--- | Monadic ping-pong. Can be executed, but cannot be statically analysed.
+-- | Monadic ping-pong, which has the desired behaviour, but cannot be
+-- statically analysed.
 pingPongM :: IO ()
 pingPongM = IO.getLine >>= \s -> if s == "ping" then IO.putStrLn "pong" else pure ()
 
--- | Applicative ping-pong. Cannot be executed, but can be statically analysed.
+-- | Applicative ping-pong, which always executes both effect, but can be
+-- statically analysed.
 pingPongA :: IO ()
 pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
 
diff --git a/examples/Teletype/Rigid.hs b/examples/Teletype/Rigid.hs
index 1fe3eee..1134896 100644
--- a/examples/Teletype/Rigid.hs
+++ b/examples/Teletype/Rigid.hs
@@ -38,8 +38,8 @@ getLine = liftSelect (Read id)
 putStrLn :: String -> Teletype ()
 putStrLn s = liftSelect (Write s ())
 
--- | The example from the paper's intro implemented using the free selective.
--- It can be statically analysed for effects:
+-- | The ping-pong example from the introduction section of the paper
+-- implemented using free selective functors.
 --
 -- @
 -- > getEffects pingPongS
@@ -59,11 +59,13 @@ pingPongS :: Teletype ()
 pingPongS = whenS (fmap ("ping"==) getLine) (putStrLn "pong")
 
 ------------------------------- Ping-pong example ------------------------------
--- | Monadic ping-pong. Can be executed, but cannot be statically analysed.
+-- | Monadic ping-pong, which has the desired behaviour, but cannot be
+-- statically analysed.
 pingPongM :: IO ()
 pingPongM = IO.getLine >>= \s -> if s == "ping" then IO.putStrLn "pong" else pure ()
 
--- | Applicative ping-pong. Cannot be executed, but can be statically analysed.
+-- | Applicative ping-pong, which always executes both effect, but can be
+-- statically analysed.
 pingPongA :: IO ()
 pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
 
diff --git a/paper/5-free.tex b/paper/5-free.tex
index a430085..9981e19 100644
--- a/paper/5-free.tex
+++ b/paper/5-free.tex
@@ -374,10 +374,10 @@ \subsubsection{Example 1. Addition}
 \vspace{1mm}
 \begin{minted}[xleftmargin=10pt]{haskell}
 add :: Register -> Address -> Program Value
-add reg addr = let arg1     = read (Reg reg)
-                   arg2     = read (Cell addr)
-                   result   = (+)   <$> arg1 <*> arg2
-                   isZero   = (==0) <$> write (Reg reg) result
+add reg addr = let arg1   = read (Reg reg)
+                   arg2   = read (Cell addr)
+                   result = (+)   <$> arg1 <*> arg2
+                   isZero = (==0) <$> write (Reg reg) result
                in write (Flag Zero) (bool 0 1 <$> isZero)
 \end{minted}
 \vspace{1mm}