diff --git a/Debug/Hoed/NoTrace.hs b/Debug/Hoed/NoTrace.hs
new file mode 100644
--- /dev/null
+++ b/Debug/Hoed/NoTrace.hs
@@ -0,0 +1,128 @@
+{-|
+Module      : Debug.Hoed.Notrace
+Description : Lighweight algorithmic debugging based on observing intermediate values.
+Copyright   : (c) 2016 Maarten Faddegon
+License     : BSD3
+Maintainer  : hoed@maartenfaddegon.nl
+Stability   : experimental
+Portability : POSIX
+
+Hoed is a tracer and debugger for the programming language Haskell.
+
+This is a drop-in replacement of the Debug.Hoed.Pure or Debug.Hoed.Stk modules and disables tracing (all functions are variations of id).
+
+Read more about Hoed on its project homepage <https://wiki.haskell.org/Hoed>.
+
+Papers on the theory behind Hoed can be obtained via <http://maartenfaddegon.nl/#pub>.
+
+I am keen to hear about your experience with Hoed: where did you find it useful and where would you like to see improvement? You can send me an e-mail at hoed@maartenfaddegon.nl, or use the github issue tracker <https://github.com/MaartenFaddegon/hoed/issues>.
+-}
+
+{-# LANGUAGE DefaultSignatures, CPP #-}
+
+module Debug.Hoed.NoTrace
+( observe
+, runO
+, printO
+, testO
+, observeBase
+, Observable(..)
+, Parent(..)
+, Generic(..)
+, send
+, ObserverM(..)
+, (<<)
+) where
+import GHC.Generics
+import System.IO.Unsafe
+import Control.Monad
+
+observe :: String -> a -> a
+observe _ = id
+
+runO :: IO a -> IO ()
+runO program = do
+  program
+  return ()
+
+printO :: (Show a) => a -> IO ()
+printO expr = print expr
+
+testO :: Show a => (a->Bool) -> a -> IO ()
+testO p x = putStrLn $ if (p x) then "Passed 1 test."
+                                else " *** Failed! Falsifiable: " ++ show x
+
+data Parent = Parent
+class Observable a where
+        observer  :: a -> Parent -> a 
+        default observer :: (Generic a) => a -> Parent -> a
+        observer x _ = x
+
+        constrain :: a -> a -> a
+        default constrain :: (Generic a) => a -> a -> a
+        constrain x _ = x
+
+observeBase :: a -> Parent -> a 
+observeBase x _ = x
+
+constrainBase :: a -> a -> a
+constrainBase x _ = x
+
+newtype ObserverM a = ObserverM { runMO :: Int -> Int -> (a,Int) }
+
+instance Functor ObserverM where
+    fmap  = liftM
+
+#if __GLASGOW_HASKELL__ >= 710
+instance Applicative ObserverM where
+    pure  = return
+    (<*>) = ap
+#endif
+
+instance Monad ObserverM where
+        return a = ObserverM (\ c i -> (a,i))
+        fn >>= k = ObserverM (\ c i ->
+                case runMO fn c i of
+                  (r,i2) -> runMO (k r) c i2
+                )
+
+(<<) :: (Observable a) => ObserverM (a -> b) -> a -> ObserverM b
+fn << a = do {fn' <- fn; return (fn' a)}
+
+send :: String -> ObserverM a -> Parent -> a
+send _ fn context =
+  unsafePerformIO $ do { let (r,portCount) = runMO fn 0 0
+                       ; return r
+                       }
+
+instance Observable Int where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable Bool where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable Integer where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable Float where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable Double where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable Char where
+  observer  = observeBase
+  constrain = constrainBase
+                                 
+instance Observable () where
+  observer  = observeBase
+  constrain = constrainBase
+
+instance (Observable a) => Observable [a] where
+  observer  = observeBase
+  constrain = constrainBase
diff --git a/Debug/Hoed/Pure.hs b/Debug/Hoed/Pure.hs
--- a/Debug/Hoed/Pure.hs
+++ b/Debug/Hoed/Pure.hs
@@ -102,14 +102,22 @@
 
   -- * Property-assisted algorithmic debugging
   , runOwp
+  , printOwp
   , testOwp
   , Propositions(..)
   , PropType(..)
   , Proposition(..)
+  , mkProposition
+  , ofType
+  , withSignature
+  , sizeHint
+  , withTestGen
+  , TestGen(..)
   , PropositionType(..)
   , Module(..)
   , Signature(..)
   , ParEq(..)
+  , (===)
   , runOstore
   , conAp
 
@@ -261,6 +269,10 @@
 printO :: (Show a) => a -> IO ()
 printO expr = runO (print expr)
 
+
+printOwp :: (Show a) => [Propositions] -> a -> IO ()
+printOwp ps expr = runOwp ps (print expr)
+
 -- | Only produces a trace. Useful for performance measurements.
 traceOnly :: IO a -> IO ()
 traceOnly program = do
@@ -306,7 +318,7 @@
   condPutStrLn verbose $ show n ++ " computation statements"
   condPutStrLn verbose $ show ((length . vertices $ ct) - 1) ++ " nodes + 1 virtual root node in the computation tree"
   condPutStrLn verbose $ show (length . arcs $ ct) ++ " edges in computation tree"
-  condPutStrLn verbose $ "computation tree has a branch factor of " ++ show b ++ "(i.e the average number of children of non-leaf nodes)"
+  condPutStrLn verbose $ "computation tree has a branch factor of " ++ show b ++ " (i.e the average number of children of non-leaf nodes)"
 
   condPutStrLn verbose "\n=== Debug Session ===\n"
   return (events, ti, ct, frt)
diff --git a/Debug/Hoed/Pure/CompTree.hs b/Debug/Hoed/Pure/CompTree.hs
--- a/Debug/Hoed/Pure/CompTree.hs
+++ b/Debug/Hoed/Pure/CompTree.hs
@@ -393,9 +393,17 @@
                                                    $ start e s
                                           False -> pause e s
 
+                        NoEnter{} -> if not . corToCons cs $ e then s else cpyTopLvlFun e
+                                     $ case loc of
+                                          True  -> addDependency e
+                                                   $ start e s
+                                          False -> pause e s
+
                         -- Span end
                         Cons{} ->  cpyTopLvlFun e
                                    . setLocation e (\_->loc)
                                    $ case loc of
                                        True  -> stop e s
                                        False -> resume e s
+
+                        evnt -> error $ "traceInfo.loop cannot handle " ++ show evnt
diff --git a/Debug/Hoed/Pure/DemoGUI.hs b/Debug/Hoed/Pure/DemoGUI.hs
--- a/Debug/Hoed/Pure/DemoGUI.hs
+++ b/Debug/Hoed/Pure/DemoGUI.hs
@@ -24,6 +24,7 @@
 import Data.IORef
 import Text.Regex.Posix
 import Text.Regex.Posix.String
+import Data.Time.Clock
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.List(findIndex,intersperse,nub,sort,sortBy
@@ -40,6 +41,8 @@
 sortOn' f = sortBy (\x y -> compare (f x) (f y))
 #endif
 
+type Next = CompTree -> (Vertex -> Judgement) -> Vertex
+
 --------------------------------------------------------------------------------
 -- The tabbed layout from which we select the different views
 
@@ -217,6 +220,7 @@
 guiAssisted traceRef ps compTreeRef currentVertexRef regexRef imgCountRef = do
 
        handlerRef <- UI.liftIO $ newIORef Bottom
+       nextRef <- UI.liftIO $ newIORef (next_step :: Next)
 
        -- Get a list of vertices from the computation tree
        tree <- UI.liftIO $ readIORef compTreeRef
@@ -230,82 +234,158 @@
        showStmt compStmt compTreeRef currentVertexRef 
 
        -- Buttons to judge the current statement
-       right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 30] # set UI.style [("margin-right","1em")]
-       wrong <- UI.button # set UI.text "wrong "    #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 30] # set UI.style [("margin-right","1em")]
-       let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef
+       right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 20] # set UI.style [("margin-right","1em")]
+       wrong <- UI.button # set UI.text "wrong "    #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 20] # set UI.style [("margin-right","1em")]
+       let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
        j right Right
        j wrong Wrong
-       testB  <- UI.button # set UI.text "test"                                                # set UI.height 30 # set UI.style [("margin-right","1em")]
-       -- testAllB  <- UI.button # set UI.text "test all"                                         # set UI.height 30 # set UI.style [("margin-right","1em")]
-       resetB <- UI.button # set UI.text "clear all judgements"                                # set UI.height 30
-       -- on UI.click testAllB $ \_ -> testAll compTreeRef traceRef ps status currentVertexRef compStmt handlerRef
-       on UI.click testB $ \_ -> testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef
-       on UI.click resetB $ \_ -> resetTree compTreeRef ps status currentVertexRef compStmt
+       let lightBulbs n = take n . repeat  $ UI.img # set UI.src "static/test.png" # set UI.height 20
 
-       -- MF TODO: remove radio buttons !?
-       -- Radio buttons to indicate how unevaluated expressions are handled
-       r1 <- UI.input # set UI.type_ "radio" # set UI.checked True
-       r2 <- UI.input # set UI.type_ "radio" # set UI.checked False
-       r3 <- UI.input # set UI.type_ "radio" # set UI.checked False
-       d1 <- UI.div #+ [return r1, UI.span # set UI.text "Abort when property depends on an unevaluated expression."]
-       d2 <- UI.div #+ [return r2, UI.span # set UI.text "Try to find counterexamples using randomly generated values for unevaluated parts of a computation statement."]
-       d3 <- UI.div #+ [return r3, UI.span # set UI.text "Accept specification without counter examples as enough to judge as right (use with caution)."]
-       radioButtons <- UI.div #+ map return [d1,d2,d3]
-       let onCheck r a b h = on UI.checkedChange r $ \_ -> do
-            UI.liftIO $ writeIORef handlerRef h
-            return a # set UI.checked False
-            return b # set UI.checked False
-       onCheck r1 r2 r3 Bottom
-       onCheck r2 r1 r3 Forall
-       -- onCheck r3 r1 r2 TrustForall
+       test1B   <- UI.button # set UI.text "test" #+ lightBulbs 1 # set UI.style [("margin-right","1em")]
+       testChB  <- UI.button # set UI.text "test" #+ lightBulbs 2 # set UI.style [("margin-right","1em")]
+       testAllB <- UI.button # set UI.text "test" #+ lightBulbs 3 # set UI.style [("margin-right","1em")]
+       resetB <- UI.button # set UI.text "clear all" # set UI.height 20
+       on UI.click test1B   $ \_ -> testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef
+       on UI.click testChB  $ \_ -> testCurrentAndChildren compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef
+       on UI.click testAllB $ \_ -> testAll compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef
+       on UI.click resetB   $ \_ -> resetTree compTreeRef ps status currentVertexRef compStmt nextRef
 
+       -- strategy buttons
+       singleStep  <- UI.input # set UI.type_ "radio" # set UI.checked True
+       divideQuery <- UI.input # set UI.type_ "radio" # set UI.checked False
+       on UI.checkedChange singleStep $ \_ -> do
+            return divideQuery # set UI.checked False
+            UI.liftIO $ writeIORef nextRef next_step
+            advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+       on UI.checkedChange divideQuery $ \_ -> do
+            return singleStep # set UI.checked False
+            UI.liftIO $ writeIORef nextRef next_daq
+            advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+
        -- Populate the main screen
-       top <- UI.center #+ [return status, UI.br, return right, return wrong, return testB{-, return testAllB-}, return resetB]
-       UI.div #+ [return top, return radioButtons, UI.hr, return compStmt]
+       top <- UI.center #+ [return status, UI.br, return right, return wrong, return test1B, return testChB, return testAllB, return resetB]
+       top2 <- UI.center #+ [ UI.span # set UI.text "strategy: " # set UI.style [("margin-right","1em")]
+                            , return singleStep, UI.span # set UI.text "single step" # set UI.style [("margin-right","1em")]
+                            , return divideQuery, UI.span # set UI.text "divide & query"]
+       UI.div #+ [return top, return top2, UI.hr, return compStmt]
 
-resetTree compTreeRef ps status currentVertexRef compStmt = do
+resetTree compTreeRef ps status currentVertexRef compStmt nextRef = do
   t <- UI.liftIO $ readIORef compTreeRef
   UI.liftIO $ writeIORef compTreeRef (mapGraph resetVertex t)
-  advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef
+  advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
   where resetVertex = flip setJudgement Unassessed
 
-{-
-testAll compTreeRef trace ps status currentVertexRef compStmt handlerRef = do
+testCurrent :: IORef CompTree -> IORef Trace -> [Propositions] -> UI.Element -> IORef Int -> UI.Element -> t -> IORef Next -> UI ()
+testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef= do
   return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]
-  UI.liftIO $ do
-    handler <- UI.liftIO $ readIORef handlerRef
-    compTree <- readIORef compTreeRef
-    compTree' <- Prop.judge handler trace ps compTree
-    writeIORef compTreeRef compTree'
-  advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef
--}
+  mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef
+  case mcv of
+    Nothing -> updateStatus status compTreeRef
+    (Just cv) -> do
+      time1 <- UI.liftIO getCurrentTime
+      test1 cv compTreeRef traceRef ps handlerRef (onNoProps cv) onJudge onTreeSwitch
+      time2 <- UI.liftIO getCurrentTime
+      UI.liftIO $ putStrLn ("tested computation statement in " ++ show (diffUTCTime time2 time1))
+  where
+  onNoProps cv = do
+    UI.element status # set UI.text ("Cannot test: no propositions associated with function " ++ (stmtLabel . vertexStmt) cv ++ "!")
+    return ()
+  onJudge =
+    advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+  onTreeSwitch :: CompTree -> Trace -> UI ()
+  onTreeSwitch newCompTree newTrace = do
+      UI.liftIO $ writeIORef compTreeRef newCompTree
+      UI.liftIO $ writeIORef traceRef newTrace 
+      advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+      return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]
+      return ()
 
-testCurrent compTreeRef traceRef ps status currentVertexRef compStmt handlerRef = do
+testCurrentAndChildren compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef = do
   return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]
   mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef
+  compTree <- UI.liftIO $ readIORef compTreeRef
   case mcv of
+    Nothing -> updateStatus status compTreeRef
     (Just cv) -> do
-      case lookupPropositions ps cv of 
-        Nothing  -> updateStatus status compTreeRef
+      let vs = cv : succs compTree cv
+      time1 <- UI.liftIO getCurrentTime
+      switchedTree <- testMany vs compTreeRef traceRef ps handlerRef
+      time2 <- UI.liftIO getCurrentTime
+      UI.liftIO $ putStrLn ("tested " ++ show (length vs) ++ " computation statements in " ++ show (diffUTCTime time2 time1))
+      advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+      if switchedTree 
+      then do
+        return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]
+        return ()
+      else
+        return ()
+
+testAll compTreeRef traceRef ps status currentVertexRef compStmt handlerRef nextRef = do
+  return status # UI.set UI.text "Evaluating propositions ..." #+ [UI.img # set UI.src "static/loading.gif" # set UI.height 30]
+  mcv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef
+  compTree <- UI.liftIO $ readIORef compTreeRef
+  let vs = vertices compTree
+  time1 <- UI.liftIO getCurrentTime
+  switchedTree <- testMany vs compTreeRef traceRef ps handlerRef
+  time2 <- UI.liftIO getCurrentTime
+  UI.liftIO $ putStrLn ("tested " ++ show (length vs) ++ " computation statements in " ++ show (diffUTCTime time2 time1))
+  advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
+  if switchedTree 
+  then do
+    return status # UI.set UI.text "Discovered and switched to a simpler computatation tree!" #+ [UI.img # set UI.src "static/test.png" # set UI.height 30]
+    return ()
+  else
+    return ()
+
+testMany :: [Vertex] -> IORef CompTree -> IORef Trace -> [Propositions] -> t -> UI Bool
+testMany vs compTreeRef traceRef ps handlerRef = case vs of
+  []      -> return False
+  (v:vs') -> do
+    continue <- test1 v compTreeRef traceRef ps handlerRef (onNoProps v) onJudge onTreeSwitch
+    if continue then testMany vs' compTreeRef traceRef ps handlerRef
+                else return True
+  where
+  onNoProps _ =
+    return True
+  onJudge = 
+    return True
+  onTreeSwitch newCompTree newTrace = do
+    UI.liftIO $ writeIORef compTreeRef newCompTree
+    UI.liftIO $ writeIORef traceRef newTrace 
+    UI.liftIO $ putStrLn $ "Switched to a simpler computation tree!"
+    return False
+
+test1 :: Vertex -> IORef CompTree -> IORef Trace -> [Propositions] -> t -> UI b -> UI b -> (CompTree -> Trace -> UI b) -> UI b
+test1 vertex compTreeRef traceRef ps handlerRef onNoProps onJudge onTreeSwitch = do
+  compTree <- UI.liftIO $ readIORef compTreeRef
+  mj <- test1' vertex compTree traceRef ps handlerRef
+  case mj of
+    Nothing  -> onNoProps
+    (Just j) -> case j of 
+      (Judge jmt) -> do
+        UI.liftIO $ putStrLn $ "conclusion: statement is " ++ show jmt
+        UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree (setJudgement vertex jmt))
+        onJudge
+      (AlternativeTree compTree' trace') -> do
+        onTreeSwitch compTree' trace'
+
+test1' :: Vertex -> CompTree -> IORef Trace -> [Propositions] -> t -> UI (Maybe Judge)
+test1' v compTree traceRef ps handlerRef = do
+      case lookupPropositions ps v of 
+        Nothing  ->
+          return Nothing
         (Just p) -> do
-          compTree <- UI.liftIO $ readIORef compTreeRef
           trace <- UI.liftIO $ readIORef traceRef
-          j <- UI.liftIO $ Prop.judge trace p cv unjudgedCharacterCount compTree
-          case j of 
-            (Judge jmt) -> 
-              UI.liftIO $ writeIORef compTreeRef (replaceVertex compTree (setJudgement cv jmt))
-            (AlternativeTree compTree' trace') -> do
-              UI.liftIO $ writeIORef compTreeRef compTree'
-              UI.liftIO $ writeIORef traceRef trace'
-              UI.liftIO $ putStrLn $ "Switched to a simpler computation tree!" -- MF TODO: need to properly tell (or better: ask) user
-          advance AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef
-    Nothing -> updateStatus status compTreeRef
+          j <- UI.liftIO $ Prop.judge trace p v unjudgedCharacterCount compTree
+          return (Just j)
 
+
 --------------------------------------------------------------------------------
 -- The Algorithmic Debugging GUI
 
 guiAlgoDebug :: IORef CompTree -> IORef Int -> IORef String -> IORef Int -> UI UI.Element
 guiAlgoDebug compTreeRef currentVertexRef regexRef imgCountRef = do
+       nextRef <- UI.liftIO $ newIORef (next_step :: Next)
 
        -- Get a list of vertices from the computation tree
        tree <- UI.liftIO $ readIORef compTreeRef
@@ -321,7 +401,7 @@
        -- Buttons to judge the current statement
        right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 30] # set UI.style [("margin-right","1em")]
        wrong <- UI.button # set UI.text "wrong "    #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 30]
-       let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef
+       let j = judge AdvanceToNext status compStmt Nothing Nothing currentVertexRef compTreeRef nextRef
        j right Right
        j wrong Wrong
 
@@ -336,8 +416,8 @@
 data Advance = AdvanceToNext | DoNotAdvance
 
 judge :: Advance -> UI.Element -> UI.Element -> Maybe UI.Element -> Maybe (UI.Element,IORef Int) 
-         -> IORef UID -> IORef CompTree -> UI.Element -> Judgement  -> UI ()
-judge adv status compStmt mMenu mImg currentVertexRef compTreeRef b j = 
+         -> IORef UID -> IORef CompTree -> IORef Next -> UI.Element -> Judgement  -> UI ()
+judge adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef b j = 
   on UI.click b $ \_ -> do
     mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef
     case mv of
@@ -348,21 +428,22 @@
   judge' v = do
       t' <- UI.liftIO $ readIORef compTreeRef
       UI.liftIO $ writeIORef compTreeRef (markNode t' v j)
-      advance adv status compStmt mMenu mImg currentVertexRef compTreeRef
+      advance adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef
 
 advance :: Advance -> UI.Element -> UI.Element -> Maybe UI.Element -> Maybe (UI.Element,IORef Int) 
-         -> IORef UID -> IORef CompTree -> UI ()
-advance adv status compStmt mMenu mImg currentVertexRef compTreeRef = do
+         -> IORef UID -> IORef CompTree -> IORef Next -> UI ()
+advance adv status compStmt mMenu mImg currentVertexRef compTreeRef nextRef = do
   mv <- UI.liftIO $ lookupCurrentVertex currentVertexRef compTreeRef
+  next <- UI.liftIO $ readIORef nextRef
   case mv of
     Nothing  -> do
       t <- UI.liftIO $ readIORef compTreeRef
-      case next_step t getJudgement of
+      case next t getJudgement of
         RootVertex -> return () -- when does this happen ... ?
         w          -> advanceTo w status compStmt mMenu mImg currentVertexRef compTreeRef
     (Just v) -> do
       t <- UI.liftIO $ readIORef compTreeRef
-      case (adv, next_step t getJudgement) of
+      case (adv, next t getJudgement) of
         (DoNotAdvance,_)           -> advanceTo v status compStmt mMenu mImg currentVertexRef compTreeRef
         (AdvanceToNext,RootVertex) -> advanceTo v status compStmt mMenu mImg currentVertexRef compTreeRef
         (AdvanceToNext,w)          -> advanceTo w status compStmt mMenu mImg currentVertexRef compTreeRef
@@ -409,7 +490,8 @@
        right <- UI.button # UI.set UI.text "right " #+ [UI.img # set UI.src "static/right.png" # set UI.height 20] # set UI.style [("margin-right","1em")]
        wrong <- UI.button # set UI.text "wrong "    #+ [UI.img # set UI.src "static/wrong.png" # set UI.height 20] # set UI.style [("margin-right","1em")]
 
-       let j = judge DoNotAdvance status compStmt (Just menu) (Just (img, imgCountRef)) currentVertexRef compTreeRef
+       nextRef <- UI.liftIO $ newIORef (next_step :: Next)
+       let j = judge DoNotAdvance status compStmt (Just menu) (Just (img, imgCountRef)) currentVertexRef compTreeRef nextRef
        j right Right
        j wrong Wrong
 
diff --git a/Debug/Hoed/Pure/Observe.lhs b/Debug/Hoed/Pure/Observe.lhs
--- a/Debug/Hoed/Pure/Observe.lhs
+++ b/Debug/Hoed/Pure/Observe.lhs
@@ -123,6 +123,7 @@
                 ) as Exception
 -}
 import Data.Dynamic ( Dynamic )
+
 \end{code}
 
 \begin{code}
@@ -150,7 +151,7 @@
 
 class GObservable f where
         gdmobserver :: f a -> Parent -> f a
-        gdmObserveChildren :: f a -> ObserverM (f a)
+        gdmObserveArgs :: f a -> ObserverM (f a)
         gdmShallowShow :: f a -> String
 
 constrainBase :: Eq a => a -> a -> a
@@ -184,54 +185,52 @@
 
 -- Meta: data types
 instance (GObservable a) => GObservable (M1 D d a) where
-        gdmobserver m@(M1 x) cxt = M1 (gdmobserver x cxt)
-        gdmObserveChildren = gthunk
-        gdmShallowShow = error "gdmShallowShow not defined on <<Meta: data types>>"
+ gdmobserver m@(M1 x) cxt = M1 (gdmobserver x cxt)
+ gdmObserveArgs = gthunk
+ gdmShallowShow = error "gdmShallowShow not defined on the <<data meta type>>"
 
 -- Meta: Selectors
 instance (GObservable a, Selector s) => GObservable (M1 S s a) where
-        gdmobserver m@(M1 x) cxt
-          = M1 (gdmobserver x cxt)
-          -- Uncomment next two lines to record selector names
-          --   selName m == "" = M1 (gdmobserver x cxt)
-          --   otherwise       = M1 (send (selName m ++ " =") (gdmObserveChildren x) cxt)
-        gdmObserveChildren  = gthunk
-        gdmShallowShow      = error "gdmShallowShow not defined on <<Meta: selectors>>"
+ gdmobserver (M1 x) cxt = M1 (gdmobserver x cxt)
+ gdmObserveArgs = gthunk
+ gdmShallowShow = error "gdmShallowShow not defined on the <<selector meta type>>"
 
 -- Meta: Constructors
 instance (GObservable a, Constructor c) => GObservable (M1 C c a) where
-        gdmobserver m1            = send (gdmShallowShow m1) (gdmObserveChildren m1)
-        gdmObserveChildren (M1 x) = do {x' <- gdmObserveChildren x; return (M1 x')}
-        gdmShallowShow            = conName
+ gdmobserver m1 = send (gdmShallowShow m1) (gdmObserveArgs m1)
+ gdmObserveArgs (M1 x) = do {x' <- gdmObserveArgs x; return (M1 x')}
+ gdmShallowShow = conName
 
 -- Unit: used for constructors without arguments
 instance GObservable U1 where
-        gdmobserver x _    = x
-        gdmObserveChildren = return
-        gdmShallowShow     = error "gdmShallowShow not defined on <<the unit type>>"
+ gdmobserver x _ = x
+ gdmObserveArgs = return
+ gdmShallowShow = error "gdmShallowShow not defined on <<the unit type>>"
 
 -- Sums: encode choice between constructors
 instance (GObservable a, GObservable b) => GObservable (a :+: b) where
-        gdmobserver (L1 x) = send (gdmShallowShow x) (gdmObserveChildren $ L1 x)
-        gdmobserver (R1 x) = send (gdmShallowShow x) (gdmObserveChildren $ R1 x)
-        gdmShallowShow (L1 x) = gdmShallowShow x
-        gdmShallowShow (R1 x) = gdmShallowShow x
-        gdmObserveChildren (L1 x) = do {x' <- gdmObserveChildren x; return (L1 x')}
-        gdmObserveChildren (R1 x) = do {x' <- gdmObserveChildren x; return (R1 x')}
+ gdmobserver (L1 x) = send (gdmShallowShow x) (gdmObserveArgs $ L1 x)
+ gdmobserver (R1 x) = send (gdmShallowShow x) (gdmObserveArgs $ R1 x)
+ gdmShallowShow (L1 x) = gdmShallowShow x
+ gdmShallowShow (R1 x) = gdmShallowShow x
+ gdmObserveArgs (L1 x) = do {x' <- gdmObserveArgs x; return (L1 x')}
+ gdmObserveArgs (R1 x) = do {x' <- gdmObserveArgs x; return (R1 x')}
 
 -- Products: encode multiple arguments to constructors
 instance (GObservable a, GObservable b) => GObservable (a :*: b) where
-        gdmobserver (a :*: b) cxt = (gdmobserver a cxt) :*: (gdmobserver b cxt)
-        gdmObserveChildren (a :*: b) = do a'  <- gdmObserveChildren a
-                                          b'  <- gdmObserveChildren b
-                                          return (a' :*: b')
-        gdmShallowShow = error "gdmShallowShow not defined on <<the product type>>"
+ gdmobserver (a :*: b) cxt = (gdmobserver a cxt) :*: (gdmobserver b cxt)
+ gdmObserveArgs (a :*: b) = do 
+   a'  <- gdmObserveArgs a
+   b'  <- gdmObserveArgs b
+   return (a' :*: b')
+ gdmShallowShow = error "gdmShallowShow not defined on <<the product type>>"
 
 -- Constants: additional parameters and recursion of kind *
 instance (Observable a) => GObservable (K1 i a) where
-        gdmobserver (K1 x) cxt = K1 $ observer x cxt
-        gdmObserveChildren = gthunk
-        gdmShallowShow = error "gdmShallowShow not defined on <<constant types>>"
+ gdmobserver (K1 x) cxt = K1 $ observer x cxt
+ gdmObserveArgs = gthunk
+ gdmShallowShow = error "gdmShallowShow not defined on <<the constant type>>"
+
 \end{code}
 
 Observing functions is done via the ad-hoc mechanism, because
@@ -547,11 +546,18 @@
 
 \begin{code}
 
+-- MF TODO: the eqType and isObservable' definitions feel a bit "hacky",
+-- can we do better?
 isObservable :: TyVarMap -> Type -> Type -> Q Bool
--- MF TODO: if s == t then return True else isObservable' bs t
+isObservable bs s t | s `eqType` t = return True 
 isObservable bs s t = isObservable' bs t
 
--- MF TODO this is a hack
+eqType (ForallT _ _ t1) t2 = t1 `eqType` t2
+eqType (AppT t1 s1) (AppT t2 s2) = (t1 `eqType` t2) && (s1 `eqType` s2)
+eqType (VarT _) (VarT _) = True -- dodgy ...
+eqType (ConT n1) (ConT n2) = n1 == n2
+eqType _ _ = False
+
 isObservable' bs (AppT ListT _)    = return True
 
 isObservable' bs (VarT n)      = case lookupBinding bs n of
diff --git a/Debug/Hoed/Pure/Prop.hs b/Debug/Hoed/Pure/Prop.hs
--- a/Debug/Hoed/Pure/Prop.hs
+++ b/Debug/Hoed/Pure/Prop.hs
@@ -1,6 +1,6 @@
 -- This file is part of the Haskell debugger Hoed.
 --
--- Copyright (c) Maarten Faddegon, 2015
+-- Copyright (c) Maarten Faddegon 2015-2016
 
 {-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP, DeriveGeneric #-}
 
@@ -8,7 +8,7 @@
 -- ( judge
 -- , Propositions(..)
 -- ) where
-import Debug.Hoed.Pure.Observe(Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate)
+import Debug.Hoed.Pure.Observe(Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate,eventParent,parentPosition)
 import Debug.Hoed.Pure.Render(CompStmt(..),noNewlines)
 import Debug.Hoed.Pure.CompTree(CompTree,Vertex(..),Graph(..),vertexUID,vertexRes,replaceVertex,getJudgement,setJudgement)
 import Debug.Hoed.Pure.EventForest(EventForest,mkEventForest,dfsChildren)
@@ -22,14 +22,16 @@
 import System.IO(hPutStrLn,stderr)
 import System.IO.Unsafe(unsafePerformIO)
 import Data.Char(isAlpha)
-import Data.Maybe(isNothing,fromJust)
-import Data.List(intersperse,isInfixOf)
+import Data.Maybe(isNothing,fromJust,isJust)
+import Data.List(intersperse,isInfixOf,foldl1)
 import GHC.Generics hiding (moduleName) --(Generic(..),Rep(..),from,(:+:)(..),(:*:)(..),U1(..),K1(..),M1(..))
 import Control.Monad(foldM)
 
 ------------------------------------------------------------------------------------------------------------------------
 
-data Propositions = Propositions { propositions :: [Proposition], propType :: PropType, funName :: String
+data Propositions = Propositions { propositions :: [Proposition]
+                                 , propType :: PropType
+                                 , funName :: String
                                  , extraModules :: [Module]
                                  }
 
@@ -39,10 +41,40 @@
   = Argument Int
   | SubjectFunction
   | Random
+  deriving (Show,Eq)
+
+data TestGen = TestGenQuickCheck | TestGenLegacyQuickCheck -- TestGenSmallCheck
   deriving Show
 
-type Proposition = (PropositionType,Module,String,[Signature])
+data Proposition = Proposition { propositionType :: PropositionType
+                               , propModule      :: Module
+                               , propName        :: String
+                               , signature       :: [Signature]
+                               , maxSize         :: Maybe Int
+                               , testgen         :: TestGen
+                               } deriving Show
 
+mkProposition :: Module -> String -> Proposition
+mkProposition m f = Proposition { propositionType = BoolProposition
+                                , propModule      = m
+                                , propName        = f
+                                , signature       = [SubjectFunction,Argument 0]
+                                , maxSize         = Nothing
+                                , testgen         = TestGenQuickCheck
+                                }
+
+ofType :: Proposition -> PropositionType -> Proposition
+ofType p t = p{propositionType = t}
+
+withSignature :: Proposition -> [Signature] -> Proposition
+withSignature p s = p{signature = s}
+
+sizeHint :: Proposition -> Int -> Proposition
+sizeHint p n = p{maxSize = Just n}
+
+withTestGen :: Proposition -> TestGen -> Proposition
+withTestGen p f = p{testgen=f}
+
 data PropositionType 
   = IOProposition
   | BoolProposition
@@ -61,18 +93,6 @@
   | DisproveBy Proposition [String] 
   deriving Show
 
-propositionType :: Proposition -> PropositionType
-propositionType (x,_,_,_) = x
-
-propName :: Proposition -> String
-propName (_,_,x,_) = x
-
-signature :: Proposition -> [Signature]
-signature (_,_,_,x) = x
-
-propModule :: Proposition -> Module
-propModule (_,x,_,_) = x
-
 ------------------------------------------------------------------------------------------------------------------------
 
 sourceFile   = ".Hoed/exe/Main.hs"
@@ -104,6 +124,7 @@
   | AlternativeTree CompTree Trace
     -- ^ Found counter example with simpler computation tree.
 
+-- TODO: review this function, not sure if complexity suggestion actually makes sense there...
 judgeAll :: UnevalHandler -> (CompTree -> Int) -> Trace -> [Propositions] -> CompTree -> IO CompTree
 judgeAll handler complexity trc ps compTree = foldM f compTree (vertices compTree)
   where
@@ -118,7 +139,7 @@
         putStrLn "*** no propositions"
         return curTree
       (Just p) -> do
-        j <- judge' Bottom trc p v complexity curTree
+        j <- judge' handler trc p v complexity curTree
         case j of
           (Judge jmt)            -> do
             putStrLn $ "*** judgement is " ++ show jmt
@@ -129,30 +150,39 @@
              putStrLn $ "*** " ++ msg
              return $ replaceVertex curTree (setJudgement v (Assisted [InconclusiveProperty msg]))
 
--- MF TODO. We should in function judge also try in between restricted and forall to use the unrestricted subject function with bottom for unevaluated expressions. Note that also in that case we need to switch trees if Wrong.
 
 -- |Use propositions to judge a computation statement.
 -- First tries restricted and bottom for unevaluated expressions,
--- then unrestricted and random values for unevaluated expressions.
+-- then unrestricted, and finally with randomly generated values 
+-- for unevaluated expressions.
 judge :: Trace -> Propositions -> Vertex -> (CompTree -> Int) -> CompTree -> IO Judge
 judge trc p v complexity curTree = do
   putStrLn $ take 50 (cycle "-")
   putStrLn $ "Evaluating properties to judge statement: " ++ vertexRes v
   putStrLn $ take 50 (cycle "-")
-  judgeBottom <- judge' Bottom trc p v complexity curTree
-  case judgeBottom of
-    (Judge (Assisted _)) -> judge' Forall trc p v complexity curTree
-    (Judge _)            -> return judgeBottom
+  putStrLn "### ATTEMPT 1: with a restricted subject function\n"
+  res1 <- judge' RestrictedBottom trc p v complexity curTree
+  case res1 of
+    (Judge (Assisted _)) -> do 
+      putStrLn "### ATTEMPT 2: with an unrestricted subject function\n"
+      res2 <- judge' Bottom trc p v complexity curTree
+      case res2 of
+        (Judge (Assisted _)) -> do 
+          putStrLn "### ATTEMPT 3: with randomly generated values\n"
+          judge' Forall trc p v complexity curTree
+        _                    -> return res2
+    (Judge _) -> return res1
+  return res1
 
-judge' Bottom trc p v complexity curTree = do
-  pas <- evalPropositions Bottom trc p v
+judge' RestrictedBottom trc p v complexity curTree = do
+  pas <- evalPropositions RestrictedBottom trc p v
   let j | propType p == Specify && all holds pas  = (Judge Right)
         | any disproves pas                       = (Judge Wrong)
         | otherwise                               = advice pas
   return j
 
-judge' Forall trc p v complexity curTree = do
-  pas <- evalPropositions Forall trc p v
+judge' handler trc p v complexity curTree = do
+  pas <- evalPropositions handler trc p v
   let j | propType p == Specify && all holds pas  = return (Judge Right)
         | any disproves pas                       = do 
             let curComplexity = complexity curTree
@@ -182,7 +212,7 @@
 -- Using the given complexity function, compare the computation trees of the list of
 -- property results and select the simplest tree.
 simplestTree :: (CompTree -> Int) -> [Module] -> [PropRes] -> (Int,CompTree,Trace) -> Trace -> Vertex -> IO (Int,CompTree,Trace)
-simplestTree complexity ms rs cur trc v = foldM (simple2 complexity trc v ms) cur (filter disprovesBy rs)
+simplestTree complexity ms rs cur trc v = foldM (simple2 complexity trc v ms) cur (filter disproves rs)
 
 -- Using the given complexity function, read the computation tree of the given property
 -- into memory and compare its complexity with the complexity of the currently best tree.
@@ -195,6 +225,8 @@
   case (maybeCandTree,maybeCandTrace) of
     (Just candTree, Just candTrace) -> do 
       let candComplexity = complexity candTree
+      putStrLn $ "Discovered new tree with complexity " ++ show candComplexity 
+                 ++ " (current tree is " ++ show curComplexity ++ ")"
       return $ if candComplexity < curComplexity 
                  then (candComplexity,candTree,candTrace)
                  else (curComplexity,curTree,curTrace)
@@ -216,14 +248,16 @@
 isError (Error _ _) = True
 isError _           = False
 
-data UnevalHandler = Bottom | Forall | FromList [String] deriving (Eq, Show)
+data UnevalHandler = RestrictedBottom | Bottom | Forall | FromList [String] deriving (Eq, Show)
 
 unevalHandler :: UnevalHandler -> PropVarGen String
-unevalHandler Bottom       = propVarError
-unevalHandler Forall       = propVarFresh
-unevalHandler (FromList _) = propVarFresh
+unevalHandler RestrictedBottom = propVarError
+unevalHandler Bottom           = propVarError
+unevalHandler Forall           = propVarFresh
+unevalHandler (FromList _)     = propVarFresh
 
 unevalState :: UnevalHandler -> PropVars
+unevalState RestrictedBottom  = propVars0
 unevalState Bottom            = propVars0
 unevalState Forall            = propVars0
 -- unevalState (FromList _)      = propVars0
@@ -246,6 +280,9 @@
 evalPropositions handler trc p v = mapM (evalProposition handler trc v (extraModules p)) (propositions p)
 
 evalProposition :: UnevalHandler -> Trace -> Vertex -> [Module] -> Proposition -> IO PropRes
+evalProposition RestrictedBottom trc v ms prop | not (SubjectFunction `elem` (signature prop)) = do
+  putStrLn $ "property " ++ propName prop ++ ": Cannot restrict subject function!"
+  return $ Error prop "Cannot restrict subject function!"
 evalProposition handler trc v ms prop = do
   putStrLn $ "property " ++ propName prop
   createDirectoryIfMissing True ".Hoed/exe"
@@ -266,11 +303,14 @@
 
 
 reEvalProposition :: PropRes -> Trace -> Vertex -> [Module] -> IO PropRes
+reEvalProposition (Disprove prop) _ _ _ = return (Disprove prop) -- no need to re-evaluate
 reEvalProposition (DisproveBy prop values) trc v ms = do
-  putStrLn $ "RE-EVALUATE with " ++ concat (intersperse " " values) ++ " {"
-  (Disprove p) <- evalProposition (FromList values) trc v ms prop
+  putStrLn $ "RE-EVALUATE with " ++ concat valuesInBrackets ++ " {"
+  (Disprove p) <- evalProposition (FromList valuesInBrackets) trc v ms prop
   putStrLn $ "} RE-EVALUATE"
   return (Disprove p)
+  where
+  valuesInBrackets = map (\s -> " (" ++ s ++ ") ") values
 
 clean = system $ "rm -f " ++ sourceFile ++ " " ++ exeFile ++ " " ++ buildFiles
 
@@ -347,9 +387,18 @@
 propVarBind :: UnevalHandler -> (String,PropVars) -> Proposition -> String
 propVarBind (FromList _) (propApp,_)       prop = generatePrint prop ++ propApp
 propVarBind _            (propApp,([],_))  prop = generatePrint prop ++ propApp
-propVarBind _            (propApp,(bvs,_)) prop = "quickCheck (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"
+propVarBind _            (propApp,(bvs,_)) prop = qc ++ " (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"
   where
   bvs' = concat (intersperse " " bvs)
+  qc = case (testgen prop, maxSize prop) of
+         (TestGenQuickCheck, Nothing) 
+           -> "quickCheckWith stdArgs{maxDiscardRatio=50}"
+         (TestGenQuickCheck, Just n)
+           -> "quickCheckWith stdArgs{maxDiscardRatio=50,maxSize=" ++ show n ++ "}"
+         (TestGenLegacyQuickCheck, Nothing)
+           ->  "check defaultConfig{configMaxFail=5000}"
+         (TestGenLegacyQuickCheck, Just n)
+           -> "check defaultConfig{configMaxFail=5000,configSize=(+" ++ show n ++ ") . (`div` 2)}"
 
 generatePrint :: Proposition -> String
 generatePrint p = case propositionType p of
@@ -409,50 +458,133 @@
     args = generateArgs (unevalHandler handler) trc getEvent i
 
     cf :: PropVarGen String
-    cf | handler == Bottom = foldl1 (liftPV $ \acc c -> acc ++ " " ++ c)
-                            [ propVarReturn $ "(" ++ genConAp (length args) f
-                            , generateRes (unevalHandler handler) trc getEvent i
-                            , propVarReturn $ ")"
-                            ]
+    cf | handler == RestrictedBottom 
+           = foldl1 (liftPV $ \acc c -> acc ++ " " ++ c)
+             [ propVarReturn $ "(" ++ genConAp (length args) f
+             , generateRes (unevalHandler handler) trc getEvent i
+             , propVarReturn $ ")"
+             ]
        | otherwise = propVarReturn f
 
 generateRes :: (PropVarGen String) -> Trace -> (UID -> Event) -> UID -> PropVarGen String
-generateRes unevalGen trc getEvent i = case dfsChildren frt e of
-  [_,_,_,Nothing] -> unevalGen
-  [_,_,_,mr]      -> generateRes' unevalGen trc getEvent mr
-  where
-  frt = (mkEventForest trc)
-  e   = getEvent i
+generateRes unevalGen trc getEvent i
+ | areFun mres = (propVarReturn " {- generateRes -} ") `pvCat`
+                 (generateRes unevalGen trc getEvent (eventUID . head . justFuns $ mres)) -- (*)
+ | otherwise   = case mres of [_,mr] -> generateRes' unevalGen trc getEvent mr
+ --
+ -- (*) MF TODO: can there be multiple funs in mres? what then?
+ --
+ where
+ mres = filter isJustRes children
+ mr = case mres of [_,e] -> e; _ -> Nothing
+ children = dfsChildren frt e
+ frt = (mkEventForest trc)
+ e   = getEvent i
 
 generateRes' :: PropVarGen String -> Trace -> (UID->Event) -> Maybe Event -> PropVarGen String
 generateRes' unevalGen trc getEvent Nothing = unevalGen
 generateRes' unevalGen trc getEvent (Just e)
-  | change e == Fun = case dfsChildren frt e of [_,_    ,_,mr] -> generateRes' unevalGen trc getEvent mr
-                                                [Nothing,_,mr] -> generateRes' unevalGen trc getEvent mr
-                                                as  -> error $ "generateRes': event " ++ show (eventUID e) ++ ":FUN has " 
-                                                               ++ show (length as) ++ " children!\nnamely: " ++ commas (map show as)
-  | otherwise       = generateExpr unevalGen frt (Just e)
-  where
-  frt = (mkEventForest trc)
+ | change e == Fun = 
+  case dfsChildren frt e of 
+   [_,_    ,_,mr] -> 
+    generateRes' unevalGen trc getEvent mr
+   [Nothing,_,mr] -> 
+    generateRes' unevalGen trc getEvent mr
+   as  -> 
+    error $ "generateRes': event " ++ show (eventUID e) 
+     ++ ":FUN has " ++ show (length as) ++ " children!\nnamely: " ++ commas (map show as)
+ | otherwise       = generateExpr unevalGen trc getEvent frt (Just e)
+ where
+ frt = (mkEventForest trc)
 
 generateArgs :: (PropVarGen String) -> Trace -> (UID -> Event) -> UID -> [PropVarGen String]
-generateArgs unevalGen trc getEvent i = case dfsChildren frt e of
-  [_,ma,_,mr]    -> generateExpr unevalGen frt ma : moreArgs unevalGen trc getEvent mr
-  [Nothing,_,mr] -> unevalGen                     : moreArgs unevalGen trc getEvent mr
-  xs             -> error ("generateArgs: dfsChildren (" ++ show e ++ ") = " ++ show xs)
-  where
-  frt = (mkEventForest trc)
-  e   = getEvent i
+generateArgs unevalGen trc getEvent i =
+ (propVarReturn " {- generateArgs -} ") `pvCat`
+ pvArg `pvCat` (propVarReturn $ " {- more: " ++ show mres ++ " -} ") 
+ : moreArgs unevalGen trc getEvent mr
+ where
+ pvArg | areFun marg = generateFunMap unevalGen trc getEvent (justFuns marg)
+       | otherwise   = case marg of
+         [Nothing] -> unevalGen
+         [_,ma]    -> generateExpr unevalGen trc getEvent frt ma
+ e   = getEvent i
+ marg = filter nothingOrArg children
+ mres = filter isJustRes children
+ mr = case mres of [_,e] -> e; _ -> Nothing
+ children = dfsChildren frt e
+ frt = (mkEventForest trc)
 
+nothingOrArg Nothing = True
+nothingOrArg (Just e) = isArg e
+
+noArg [Nothing] = True
+noArg _         = False
+
+areFun :: [Maybe Event] -> Bool
+areFun (_:e:_) = isJustFun e
+areFun _       = False
+
+justFuns :: [Maybe Event] -> [Event]
+justFuns = map fromJust . filter isJustFun 
+
+isJustFun :: Maybe Event -> Bool
+isJustFun (Just e) = change e == Fun
+isJustFun Nothing  = False
+
+generateFunMap :: (PropVarGen String) -> Trace -> (UID -> Event) -> [Event] -> PropVarGen String
+generateFunMap unevalGen trc getEvent funs 
+ | length funs > 0 = caseOf `pvCat` (pvConcat cases') `pvCat` esac
+ | otherwise       = propVarReturn "{- a fun without applications? -}"
+ where 
+ caseOf = propVarReturn $ " {- funmap with " ++ (show . length $ funs ) ++ " cases -} " 
+                          ++ "(\\y -> case y of "
+ esac   = propVarReturn ")"
+ cases, cases' :: [PropVarGen String]
+ cases  = map (\fun -> generateCase unevalGen trc getEvent fun) funs
+ cases' = intersperse (propVarReturn "; ") cases
+
+generateCase :: (PropVarGen String) -> Trace -> (UID -> Event) -> Event -> PropVarGen String
+generateCase unevalGen trc getEvent fun =
+ (propVarReturn $ " {- CASE " ++ show fun ++ " -} ") `pvCat`
+ case args of 
+  [] -> (propVarReturn "{- catchall -} _") --> res
+  _  -> (foldl1 (liftPV $ \acc c -> acc ++ " " ++ c) args) --> res
+ where
+ args :: [PropVarGen String]
+ args  = map (generateExpr (propVarReturn "_") trc getEvent frt)
+         . filter (\(Just e) -> isArg e) . filter isJust . dfsChildren frt $ fun
+ res :: PropVarGen String
+ res  = generateRes unevalGen trc getEvent (eventUID fun)
+ (-->) :: PropVarGen String -> PropVarGen String -> PropVarGen String 
+ (-->) = liftPV $ \x y -> x ++ " -> " ++ y
+ frt = mkEventForest trc -- MF TODO: create just once and share?
+
+isArg = hasParentPos 0
+
+isRes = hasParentPos 1
+
+isJustRes (Just e) = isRes e
+isJustRes Nothing  = False
+
+hasParentPos i = (==i) . parentPosition . eventParent
+
+pvCat :: PropVarGen String -> PropVarGen String -> PropVarGen String
+pvCat = liftPV (++)
+
+pvConcat :: [PropVarGen String] -> PropVarGen String
+pvConcat = foldl pvCat (propVarReturn "")
+
 moreArgs :: PropVarGen String -> Trace -> (UID->Event) -> Maybe Event -> [PropVarGen String]
 moreArgs _ trc getEvent Nothing = []
 moreArgs unevalGen trc getEvent (Just e)
   | change e == Fun = generateArgs unevalGen trc getEvent (eventUID e)
   | otherwise       = []
 
-generateExpr :: PropVarGen String -> EventForest -> Maybe Event -> PropVarGen String
-generateExpr unevalGen _ Nothing    = unevalGen
-generateExpr unevalGen frt (Just e) = case change e of
+generateExpr :: PropVarGen String -> Trace -> (UID -> Event) -> EventForest -> Maybe Event -> PropVarGen String
+generateExpr unevalGen _ _ _ Nothing    = unevalGen
+generateExpr unevalGen trc getEvent frt (Just e) = 
+  -- (propVarReturn $ "{- generateExpr " ++ show e ++ "-}") `pvCat` 
+  case change e of
   (Cons _ s) -> let s' = if isAlpha (head s) then s else "(" ++ s ++ ")"
                 in liftPV (++) ( foldl (liftPV $ \acc c -> acc ++ " " ++ c)
                                  (propVarReturn ("(" ++ s')) cs
@@ -460,30 +592,35 @@
                                ( propVarReturn ") "
                                )
   Enter      -> propVarReturn ""
-  _          -> propVarReturn "error \"cannot represent\""
+  -- Fun        -> generateFunMap unevalGen trc getEvent (justFuns xs)
+  evnt       -> propVarReturn $ "error \"cannot represent: " ++ show evnt ++ "\""
 
-  where cs :: [PropVarGen String]
-        cs = map (generateExpr unevalGen frt) (dfsChildren frt e)
+ where cs :: [PropVarGen String]
+       cs = map (generateExpr unevalGen trc getEvent frt) xs
+       xs = (dfsChildren frt e)
 
 
-------------------------------------------------------------------------------------------------------------------------
-
 -- only works if there is 1 argument
 conAp :: Observable b => (a -> b) -> b -> a -> b
 conAp f r x = constrain (f x) r
 
 genConAp :: Int -> String -> String
-genConAp n f = "(\\r " ++ args ++ " -> Hoed.constrain (" ++ f ++ " " ++ args ++ ") r)"
+genConAp n f | n > 0 = "(\\r " ++ args ++ " -> Hoed.constrain (" ++ f ++ " " ++ args ++ ") r)"
   where args = foldl1 (\a x -> a ++ " " ++ x) xs
         xs = map (\i -> "x" ++ show i) [1..n]
 
-------------------------------------------------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
 -- MF TODO: this should probably be part of the Observable class ...
 
+
+(===) :: ParEq a => a -> a -> Bool
+x === y = case parEq x y of (Just b) -> b
+                            Nothing  -> error "might be equal"
+
 class ParEq a where
-  (===) :: a -> a -> Maybe Bool
-  default (===) :: (Generic a, GParEq (Rep a)) => a -> a -> Maybe Bool
-  x === y = gParEq (from x) (from y)
+  parEq :: a -> a -> Maybe Bool
+  default parEq :: (Generic a, GParEq (Rep a)) => a -> a -> Maybe Bool
+  parEq x y = gParEq (from x) (from y)
 
 class GParEq rep where
   gParEq :: rep a -> rep a -> Maybe Bool
@@ -521,7 +658,7 @@
 -- Constants: additional parameters and recursion of kind *
 instance (ParEq a) => GParEq (K1 i a) where
   gParEq x y = let r = gParEq_ x y in r
-    where gParEq_ (K1 x) (K1 y) = x === y
+    where gParEq_ (K1 x) (K1 y) = x `parEq` y
 
 -- Meta: data types
 instance (GParEq a) => GParEq (M1 D d a) where
@@ -541,9 +678,9 @@
 instance (ParEq a)          => ParEq [a]
 instance (ParEq a, ParEq b) => ParEq (a,b)
 instance (ParEq a)          => ParEq (Maybe a)
-instance ParEq Int          where x === y = Just (x == y)
-instance ParEq Bool         where x === y = Just (x == y)
-instance ParEq Integer      where x === y = Just (x == y)
-instance ParEq Float        where x === y = Just (x == y)
-instance ParEq Double       where x === y = Just (x == y)
-instance ParEq Char         where x === y = Just (x == y)
+instance ParEq Int          where parEq x y = Just (x == y)
+instance ParEq Bool         where parEq x y = Just (x == y)
+instance ParEq Integer      where parEq x y = Just (x == y)
+instance ParEq Float        where parEq x y = Just (x == y)
+instance ParEq Double       where parEq x y = Just (x == y)
+instance ParEq Char         where parEq x y = Just (x == y)
diff --git a/Debug/Hoed/Pure/Render.hs b/Debug/Hoed/Pure/Render.hs
--- a/Debug/Hoed/Pure/Render.hs
+++ b/Debug/Hoed/Pure/Render.hs
@@ -66,6 +66,8 @@
 ------------------------------------------------------------------------
 -- Render equations from CDS set
 
+statementWidth = 110 -- 110 is good for papers (maybe make this configurable from the GUI?)
+
 renderCompStmts :: CDSSet -> [CompStmt]
 renderCompStmts = foldl (\acc set -> acc ++ renderCompStmt set) []
 
@@ -73,20 +75,22 @@
 -- is rendered to a computation statement
 
 renderCompStmt :: CDS -> [CompStmt]
-renderCompStmt (CDSNamed name dependsOn set)
+renderCompStmt (CDSNamed name uid set)
   = map mkStmt statements
   where statements :: [(String,UID)]
-        statements   = map (\(d,i) -> (pretty 70 d,i)) doc
-        doc          = foldl (\a b -> a ++ renderNamedTop name b) [] output
+        statements   = map (\(d,i) -> (pretty statementWidth d,i)) doc
+        doc          = foldl (\a b -> a ++ renderNamedTop name uid b) [] output
         output       = cdssToOutput set
 
         mkStmt :: (String,UID) -> CompStmt
         mkStmt (s,i) = CompStmt name i s
 
-renderNamedTop :: String -> Output -> [(Doc,UID)]
-renderNamedTop name (OutData cds)
-  =  map (\(args,res,Just i) -> (renderNamedFn name (args,res), i)) pairs
-  where pairs  = (nubSorted . sortOn argAndRes) pairs'
+renderNamedTop :: String -> UID -> Output -> [(Doc,UID)]
+renderNamedTop name observeUid(OutData cds)
+  =  map f pairs
+  where f (args,res,Just i) = (renderNamedFn name (args,res), i)
+        f (_,cons,Nothing)  = (renderNamedCons name cons, observeUid)
+        pairs  = (nubSorted . sortOn argAndRes) pairs'
         pairs' = findFn [cds]
         argAndRes (arg,res,_) = (arg,res)
 
@@ -226,6 +230,12 @@
                  text "-> " <> renderSet' 0 False res
                 )
                )
+
+renderNamedCons :: String -> CDSSet -> Doc
+renderNamedCons name cons
+  = text name <> nest 2
+     ( sep <> linebreak <> grp (text "= " <> renderSet' 0 False cons)
+     )
 
 renderNamedFn :: String -> ([CDSSet],CDSSet) -> Doc
 renderNamedFn name (args,res)
diff --git a/Debug/Hoed/Pure/TestParEq.hs b/Debug/Hoed/Pure/TestParEq.hs
--- a/Debug/Hoed/Pure/TestParEq.hs
+++ b/Debug/Hoed/Pure/TestParEq.hs
@@ -25,14 +25,14 @@
 t10 = pareq_equiv c c where c = (C (F 4 2))
 t11 = pareq_equiv c c where c = (C (F 4 2))
 
-s1 = ((G (error "oeps") D) === (G D (F 4 2))) == Just False
-s2 = ((G D (F 4 2) === (G (error "oeps") D))) == Just False
-s3 = ((G (error "oeps") D) === (G D D)) == Nothing
-s4 = (I D (E A A A) D) === (I (error "oeps") D D) == Just False
-s5 = (I D D (E A A A)) === (I D (error "oeps") D) == Just False
-s6 = (I (E A A A) D D) === (I D D (error "oeps")) == Just False
+s1 = ((G (error "oeps") D) === (G D (F 4 2))) == False
+s2 = ((G D (F 4 2) === (G (error "oeps") D))) == False
+s3 = ((G (error "oeps") D) `parEq` (G D D)) == Nothing
+s4 = (I D (E A A A) D) === (I (error "oeps") D D) == False
+s5 = (I D D (E A A A)) === (I D (error "oeps") D) == False
+s6 = (I (E A A A) D D) === (I D D (error "oeps")) == False
 
 -- pareq should be equivalent to normal equality when the
 -- latter is conclusive
 pareq_equiv x y = (x == y) == b
-  where (Just b) = x === y
+  where (Just b) = x `parEq` y
diff --git a/Debug/Hoed/Stk.hs b/Debug/Hoed/Stk.hs
--- a/Debug/Hoed/Stk.hs
+++ b/Debug/Hoed/Stk.hs
@@ -156,7 +156,7 @@
   hPutStrLn stderr $ show n ++ " computation statements"
   hPutStrLn stderr $ show ((length . vertices $ ct) - 1) ++ " nodes + 1 virtual root node in the computation tree"
   hPutStrLn stderr $ show (length . arcs $ ct) ++ " edges in computation tree"
-  hPutStrLn stderr $ "computation tree has a branch factor of " ++ show b ++ "(i.e the average number of children of non-leaf nodes)"
+  hPutStrLn stderr $ "computation tree has a branch factor of " ++ show b ++ " (i.e the average number of children of non-leaf nodes)"
 
   hPutStrLn stderr "\n=== Debug session === \n"
   -- hPutStrLn stderr (showWithStack eqs)
diff --git a/Debug/Hoed/Stk/Render.hs b/Debug/Hoed/Stk/Render.hs
--- a/Debug/Hoed/Stk/Render.hs
+++ b/Debug/Hoed/Stk/Render.hs
@@ -118,6 +118,9 @@
 --         Truncate -> nextStack_truncate
 nextStack = nextStack_truncate
 
+nextStackVertex (Vertex (c:_) _) = nextStack c
+vertexStack (Vertex (c:_) _) = equStack c
+
 -- Always push onto top of stack
 -- nextStack_vanilla :: CompStmt -> CallStack
 -- nextStack_vanilla (CompStmt cc _ _ _ _ ccs) = cc:ccs
@@ -161,19 +164,19 @@
 ------------------------------------------------------------------------
 -- Bags are collections of computation statements with the same stack
 
-data Bag = Bag {bagStack :: CallStack, bagStmts :: [CompStmt]}
+data Bag = Bag {bagStack :: CallStack, bagStmts :: [Vertex]}
 
 instance Eq  Bag where b1 == b2 = {-# SCC "Bag.==" #-} bagStack b1 == bagStack b2
 instance Ord Bag where compare b1 b2 = cmpStk (bagStack b1) (bagStack b2)
 
-bag :: (CompStmt -> CallStack) -> CompStmt -> Bag
+bag :: (Vertex -> CallStack) -> Vertex -> Bag
 bag s c = Bag (s c) [c]
 
-(+++) :: CompStmt -> Bag -> Bag
+(+++) :: Vertex -> Bag -> Bag
 c +++ b = b{bagStmts = c : bagStmts b}
 
 
-mkBags :: (CompStmt -> CallStack) -> [CompStmt] -> [Bag]
+mkBags :: (Vertex -> CallStack) -> [Vertex] -> [Bag]
 mkBags _ []  = []
 mkBags s cs = mkBags' (bag s fc) [] ocs
 
@@ -189,12 +192,11 @@
 
 type Tree = RBTree Bag
 
-mkTree :: (CompStmt -> CallStack) -> [CompStmt] -> Tree
+mkTree :: (Vertex -> CallStack) -> [Vertex] -> Tree
 mkTree s cs = foldl insertOrd emptyRB (mkBags s cs)
 
-mkTrees :: [CompStmt] -> (Tree,Tree)
-mkTrees cs = (mkTree equStack cs, mkTree nextStack cs)
-
+mkTrees :: [Vertex] -> (Tree,Tree)
+mkTrees cs = (mkTree vertexStack cs, mkTree nextStackVertex cs)
 
 cmpStk :: CallStack -> CallStack -> Ordering
 cmpStk [] [] = EQ
@@ -202,7 +204,7 @@
                 EQ  -> compare (head s1) (head s2)
                 ord -> ord
 
-lookup :: Tree -> CallStack -> [CompStmt]
+lookup :: Tree -> CallStack -> [Vertex]
 lookup t s = case search (\s b -> cmpStk s (bagStack b)) t s of
                (Just b) -> bagStmts b
                Nothing  -> []
@@ -210,7 +212,7 @@
 ------------------------------------------------------------------------
 -- Inverse call
 
-stmts :: Tree -> (CallStack,CallStack) -> [(CompStmt,CompStmt)]
+stmts :: Tree -> (CallStack,CallStack) -> [(Vertex,Vertex)]
 stmts t (s1,s2) = flattenStmts (lookup t s1, lookup t s2)
 
 flattenStmts :: ([a],[b]) -> [(a,b)]
@@ -252,53 +254,38 @@
 isRoot Root = True
 isRoot _    = False
 
-pushDeps :: (Tree,Tree) -> [CompStmt] -> [Arc CompStmt ()]
+pushDeps :: (Tree,Tree) -> [Vertex] -> [Arc Vertex ()]
 pushDeps ts cs = concat (map (pushArcs ts) cs)
 
-pushArcs :: (Tree,Tree) -> CompStmt -> [Arc CompStmt ()]
+pushArcs :: (Tree,Tree) -> Vertex -> [Arc Vertex ()]
 pushArcs t p = map (\c -> p ==> c) (pushers t p)
   where src ==> tgt = Arc src tgt ()
 
-pushers :: (Tree,Tree) -> CompStmt -> [CompStmt]
-pushers (ts,tn) c = lookup ts (nextStack c)
+pushers :: (Tree,Tree) -> Vertex -> [Vertex]
+pushers (ts,tn) c = lookup ts (nextStackVertex c)
 
-callDeps :: (Tree,Tree) -> [CompStmt] -> [Arc CompStmt ()]
+callDeps :: (Tree,Tree) -> [Vertex] -> [Arc Vertex ()]
 callDeps (_,t) cs = concat (map (callDep t) cs)
 
-callDep :: Tree -> CompStmt -> [Arc CompStmt ()]
+callDep :: Tree -> Vertex -> [Arc Vertex ()]
 callDep t c3 = foldl (\as (c2,c1) -> c1 ==> c2 : c2 ==> c3 : as) []
-                          (concat (map (stmts t) (lacc $ equStack c3)))
+                          (concat (map (stmts t) (lacc $ vertexStack c3)))
   where src ==> tgt = Arc src tgt ()
 
 mkGraph :: [CompStmt] -> CompGraph
 mkGraph cs =  (dagify merge)
               . addRoot
-              . toVertices 
-              -- . sameThread 
-              -- . filterDependsJustOn
-              -- . addSequenceDependencies
               . nubArcs
               $ g
-  where g :: Graph CompStmt ()
-        g = let ts = mkTrees cs in Graph (head' msg cs) cs (pushDeps ts cs ++ callDeps ts cs)
+  where g :: Graph Vertex ()
+        g = Graph (head' msg vs) vs (pushDeps ts vs ++ callDeps ts vs)
         msg = "mkGraph: No computation statements to construct graph from!"
 
-        nubArcs :: Graph CompStmt () -> Graph CompStmt ()
-        nubArcs (Graph r vs as) = Graph r vs (nub as)
-
-        -- sameThread :: Graph CompStmt () -> Graph CompStmt ()
-        -- sameThread (Graph r vs as) = Graph r vs (filter (sameThread') as)
-        -- sameThread' (Arc v w _)
-        --   | equThreadId v == ThreadIdUnknown 
-        --     || equThreadId w == ThreadIdUnknown
-        --     || equThreadId v == equThreadId w   = True
-        --   | otherwise                           = False
+        ts = mkTrees vs
+        vs = mergeEquivalent cs
 
-        -- filterDependsJustOn :: Graph CompStmt () -> Graph CompStmt ()
-        -- filterDependsJustOn (Graph r vs as) = Graph r vs (filter (filterDependsJustOn') as)
-        -- filterDependsJustOn' (Arc v w _) = case equDependsOn w of
-        --   (DependsJustOn i) -> i == equIdentifier v
-        --   _                 -> True
+        nubArcs :: Graph Vertex () -> Graph Vertex ()
+        nubArcs (Graph r vs as) = Graph r vs (nub as)
 
         addSequenceDependencies :: Graph CompStmt () -> Graph CompStmt ()
         addSequenceDependencies (Graph r vs as) = Graph r vs (seqDeps vs ++ as)
@@ -307,9 +294,6 @@
           (InSequenceAfter i) -> i == equIdentifier v
           _                     -> False
 
-        toVertices :: Graph CompStmt () -> CompGraph
-        toVertices = mapGraph (\s->Vertex [s] Unassessed)
-
         addRoot :: CompGraph -> CompGraph
         addRoot (Graph _ vs as) =
                 let rs = filter (\(Vertex (s:_) _) -> equStack s == []) vs
@@ -322,6 +306,17 @@
         msgvs = "mkGraph.merge: No vertices to merge."
 
         src ==> tgt = Arc src tgt ()
+
+mergeEquivalent :: [CompStmt] -> [Vertex]
+mergeEquivalent [] = []
+mergeEquivalent (c:cs) = mkVertex (c:e) : mergeEquivalent n
+  where
+  equivalent x y = equLabel x == equLabel y && equStack x == equStack y
+  (e,n) = partition (equivalent c) cs
+
+mkVertex :: [CompStmt] -> Vertex
+mkVertex s = Vertex s Unassessed
+
 
 -- %************************************************************************
 -- %*                                                                   *
diff --git a/Hoed.cabal b/Hoed.cabal
--- a/Hoed.cabal
+++ b/Hoed.cabal
@@ -1,5 +1,5 @@
 name:                Hoed
-version:             0.3.5
+version:             0.3.6
 synopsis:            Lightweight algorithmic debugging.
 description:
     Hoed is a tracer and debugger for the programming language Haskell.
@@ -20,6 +20,11 @@
 extra-source-files:  changelog, README.md, configure.Demo, configure.Generic, configure.Profiling, configure.Prop, configure.Pure, configure.Stk, run, test.Generic, test.Pure, test.Stk
 data-files:          img/*.png, img/*.gif
 
+
+flag buildPropExamples
+  description: Build example executables.
+  default: False
+
 flag buildExamples
   description: Build example executables.
   default: False
@@ -47,6 +52,7 @@
 library
   exposed-modules:     Debug.Hoed.Stk
                        , Debug.Hoed.Pure
+                       , Debug.Hoed.NoTrace
   other-modules:       Debug.Hoed.Stk.Observe
                        , Debug.Hoed.Stk.Render
                        , Debug.Hoed.Stk.DemoGUI
@@ -62,15 +68,16 @@
                        , template-haskell
                        , array, containers
                        , process
-                       , threepenny-gui == 0.6.*
+                       , threepenny-gui == 0.6.0.5
                        , filepath
-                       , libgraph == 1.10
+                       , libgraph == 1.11
                        , RBTree == 0.0.5
                        , regex-posix
                        , mtl
                        , directory
                        , FPretty
                        , cereal, bytestring
+                       , time
   default-language:    Haskell2010
   -- Enable to get some extra warnings.
   --   ghc-options:         -fwarn-unused-binds
@@ -87,11 +94,31 @@
 --
 ---------------------------------------------------------------------------
 
+Executable hoed-examples-Raincat
+  if flag(buildExamples)
+    build-depends:      base >= 3 && < 5,
+                        containers,
+                        extensible-exceptions,
+                        mtl,
+                        random,
+                        time,
+                        GLUT,
+                        OpenGL,
+                        SDL,
+                        SDL-image,
+                        SDL-mixer,
+                        Hoed
+  else
+    buildable: False
+  main-is:             Main.hs
+  hs-source-dirs:      examples/Raincat/src
+  default-language:    Haskell2010
+
 Executable hoed-examples-FPretty_indents_too_much
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
                          , containers
                          , deepseq
@@ -106,7 +133,7 @@
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
                          , containers
                          , deepseq
@@ -134,15 +161,31 @@
 --   hs-source-dirs:      examples/FPretty__with_properties
 --   default-language:    Haskell2010
 
-Executable hoed-examples-Queens__with_properties
+Executable hoed-examples-Stern-Brocot
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
                          , containers
                          , deepseq
                          , array
+  else
+    buildable: False
+  main-is:             SternBrocot.lhs
+  hs-source-dirs:      examples/
+  default-language:    Haskell2010
+
+Executable hoed-examples-Queens_v1__with_properties
+  -- if flag(buildExamples) ||
+  if flag (buildPropExamples)
+    build-depends:       base >= 4 && < 5
+                         , Hoed
+                         , threepenny-gui == 0.6.0.5
+                         , filepath
+                         , containers
+                         , deepseq
+                         , array
                          , QuickCheck
                          , mtl
   else
@@ -151,11 +194,80 @@
   hs-source-dirs:      examples/Queens__with_properties
   default-language:    Haskell2010
 
+Executable hoed-examples-Queens_v2__with_properties
+  if flag(buildPropExamples)
+    build-depends:       base >= 4 && < 5
+                         , Hoed
+                         , threepenny-gui == 0.6.0.5
+                         , filepath
+                         , containers
+                         , deepseq
+                         , array
+                         , QuickCheck
+                         , mtl
+  else
+    buildable: False
+  main-is:             Main2.hs
+  hs-source-dirs:      examples/Queens__with_properties
+  default-language:    Haskell2010
+
+Executable hoed-examples-Queens_v3__with_properties
+  if flag(buildPropExamples)
+    build-depends:       base >= 4 && < 5
+                         , Hoed
+                         , threepenny-gui == 0.6.0.5
+                         , filepath
+                         , containers
+                         , deepseq
+                         , array
+                         , QuickCheck
+                         , mtl
+  else
+    buildable: False
+  main-is:             Main3.hs
+  hs-source-dirs:      examples/Queens__with_properties
+  default-language:    Haskell2010
+
+Executable hoed-examples-Queens_v4_defect_in_filter__with_properties
+  if flag(buildPropExamples)
+    build-depends:       base >= 4 && < 5
+                         , Hoed
+                         , threepenny-gui == 0.6.0.5
+                         , filepath
+                         , containers
+                         , deepseq
+                         , array
+                         , QuickCheck
+                         , mtl
+  else
+    buildable: False
+  main-is:             Main.hs
+  hs-source-dirs:      examples/Queens_defective_filter__with_properties
+  default-language:    Haskell2010
+
+Executable hoed-examples-filter__with_properties
+  if flag(buildPropExamples)
+    build-depends:       base >= 4 && < 5
+                         , Hoed
+                         , threepenny-gui == 0.6.0.5
+                         , filepath
+                         , containers
+                         , deepseq
+                         , array
+                         , QuickCheck
+                         , mtl
+  else
+    buildable: False
+  main-is:             Main.hs
+  hs-source-dirs:      examples/filter__with_properties
+  default-language:    Haskell2010
+
+
 Executable hoed-examples-Rot13
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -167,7 +279,7 @@
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -177,7 +289,7 @@
 
 Executable hoed-examples-ZLang_Defect-1
   if flag(buildExamples)
-    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
+    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
   else
     buildable: False
   main-is:             Main.hs
@@ -186,7 +298,7 @@
 
 Executable hoed-examples-ZLang_Defect-2
   if flag(buildExamples)
-    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
+    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
   else
     buildable: False
   main-is:             Main.hs
@@ -195,7 +307,7 @@
 
 Executable hoed-examples-ZLang_Defect-3
   if flag(buildExamples)
-    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
+    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck, mtl, monad-loops, transformers, containers, parsec, indents, adjunctions
   else
     buildable: False
   main-is:             Main.hs
@@ -203,8 +315,8 @@
   default-language:    Haskell2010
 
 Executable hoed-examples-Nub-defective-sort__with_properties
-  if flag(buildExamples)
-    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui, filepath, QuickCheck
+  if flag(buildPropExamples)
+    build-depends:     base >= 4 && < 5, Hoed, threepenny-gui == 0.6.0.5, filepath, QuickCheck
   else
     buildable: False
   main-is:             Main.hs
@@ -215,7 +327,7 @@
   if flag(buildExamples)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -236,6 +348,19 @@
   hs-source-dirs:      examples/XMonad_changing_focus_duplicates_windows
   default-language:    Haskell2010
 
+Executable hoed-examples-XMonad_changing_focus_duplicates_windows__test_only
+  if flag(buildExamples)
+    build-depends:     base >= 4 && < 5, Hoed, 
+                       X11>=1.5 && < 1.7, mtl, unix,
+                       utf8-string,
+                       extensible-exceptions, random,
+                       containers, filepath, process, directory
+  else
+    buildable: False
+  main-is:             Main.hs
+  hs-source-dirs:      examples/XMonad_changing_focus_duplicates_windows__test_only
+  default-language:    Haskell2010
+
 Executable hoed-examples-XMonad_changing_focus_duplicates_windows__CC
   if flag(buildExamples)
     build-depends:     base >= 4 && < 5, Hoed, 
@@ -250,7 +375,8 @@
   default-language:    Haskell2010
 
 Executable hoed-examples-XMonad_changing_focus_duplicates_windows__with_properties
-  if flag(buildExamples)
+  --if flag(buildExamples)
+  if flag (buildPropExamples)
     build-depends:     base >= 4 && < 5, Hoed, 
                        X11>=1.5 && < 1.7, mtl, unix,
                        utf8-string,
@@ -277,7 +403,7 @@
   default-language:    Haskell2010
 
 Executable hoed-examples-SummerSchool_compiler_does_not_terminate__with_properties
-  if flag(buildExamples)
+  if flag(buildPropExamples)
     build-depends:     base >= 4 && < 5, Hoed, 
                        X11>=1.5 && < 1.7, mtl, unix,
                        utf8-string,
@@ -291,7 +417,7 @@
   default-language:    Haskell2010
 
 Executable hoed-examples-CNF_unsound_de_Morgan__with_properties
-  if flag(buildExamples)
+  if flag(buildPropExamples)
     build-depends:     base >= 4 && < 5, Hoed
   else
     buildable: False
@@ -300,7 +426,7 @@
   default-language:    Haskell2010
 
 Executable hoed-examples-Digraph_not_data_invariant__with_properties
-  if flag(buildExamples)
+  if flag(buildPropExamples)
     build-depends:     base >= 4 && < 5, Hoed, lazysmallcheck
   else
     buildable: False
@@ -732,18 +858,19 @@
   hs-source-dirs:      tests/Prop/t4
   default-language:    Haskell2010
 
--- Executable hoed-tests-Prop-t5
---   if flag(validateProp)
---     build-depends:     base >= 4 && < 5, Hoed, 
---                        X11>=1.5 && < 1.7, mtl, unix,
---                        utf8-string >= 0.3 && < 0.4,
---                        extensible-exceptions, random,
---                        containers, filepath, process, directory
---   else
---     buildable: False
---   main-is:             Main.hs
---   hs-source-dirs:      tests/Prop/t5
---   default-language:    Haskell2010
+Executable hoed-tests-Prop-t5
+  if flag(validateProp)
+    build-depends:     base >= 4 && < 5, Hoed, 
+                       X11>=1.5 && < 1.7, mtl, unix,
+                       utf8-string,
+                       extensible-exceptions, random,
+                       containers, filepath, process, directory,
+                       QuickCheck
+  else
+    buildable: False
+  main-is:             Main.hs
+  hs-source-dirs:      tests/Prop/t5
+  default-language:    Haskell2010
 
 ---------------------------------------------------------------------------
 -- Validate derivation of Observable and ParEq for Generic types
@@ -757,9 +884,9 @@
                          , template-haskell
                          , array, containers
                          , process
-                         , threepenny-gui == 0.6.*
+                         , threepenny-gui == 0.6.0.5
                          , filepath
-                         , libgraph == 1.10
+                         , libgraph == 1.11
                          , RBTree == 0.0.5
                          , regex-posix
                          , mtl
@@ -925,7 +1052,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
                          , network
   else
@@ -939,7 +1066,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -952,7 +1079,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -965,7 +1092,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -978,7 +1105,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
@@ -991,7 +1118,7 @@
   if flag(validateStk)
     build-depends:       base >= 4 && < 5
                          , Hoed
-                         , threepenny-gui
+                         , threepenny-gui == 0.6.0.5
                          , filepath
   else
     buildable: False
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,11 @@
-# Hoed - A Lightweight Haskell Tracer and Debugger [![Build Status](https://travis-ci.org/MaartenFaddegon/Hoed.svg?branch=master)](https://travis-ci.org/MaartenFaddegon/Hoed)
+# Hoed - A Lightweight Haskell Tracer and Debugger 
 
 Hoed is a tracer and debugger for the programming language Haskell. To locate a defect with Hoed you annotate suspected functions and compile as usual. Then you run your program, information about the annotated functions is collected. Finally you connect to a debugging session using a webbrowser. See the
 
   [**Project homepage**](http://wiki.haskell.org/Hoed)
 
 for more information on what it does and how you can use it to find bugs in your code.
+
+Submit feature requests or contribute code on the
+
+  [**Github projectpage**](https://github.com/MaartenFaddegon/Hoed) [![Build Status](https://travis-ci.org/MaartenFaddegon/Hoed.svg?branch=master)](https://travis-ci.org/MaartenFaddegon/Hoed)
diff --git a/examples/CNF_unsound_demorgan__with_properties/Main.hs b/examples/CNF_unsound_demorgan__with_properties/Main.hs
--- a/examples/CNF_unsound_demorgan__with_properties/Main.hs
+++ b/examples/CNF_unsound_demorgan__with_properties/Main.hs
@@ -4,8 +4,13 @@
 
 main = runOwp properties $ print (prop_negin_correct negin eg)
   where
-  properties = [Propositions [ (BoolProposition,cnfModule,"prop_negin_complete",[Argument (-1),Argument 0])
-                             , (BoolProposition,cnfModule,"prop_negin_sound",[Argument (-1),Argument 0])]
-                             Specify "negin" []
+  properties = [Propositions 
+                  [ mkProposition cnfModule "prop_negin_complete"
+                     `ofType` BoolProposition
+                     `withSignature` [SubjectFunction,Argument 0]
+                  , mkProposition cnfModule "prop_negin_sound"
+                     `ofType` BoolProposition
+                     `withSignature` [SubjectFunction,Argument 0]
+                  ] Specify "negin" []
                ]
   cnfModule     = Module "CNF" "../examples/CNF_unsound_demorgan__with_properties/"
diff --git a/examples/Digraph_not_data_invariant__with_properties/Main.hs b/examples/Digraph_not_data_invariant__with_properties/Main.hs
--- a/examples/Digraph_not_data_invariant__with_properties/Main.hs
+++ b/examples/Digraph_not_data_invariant__with_properties/Main.hs
@@ -4,11 +4,11 @@
 
 main = runOwp properties $ print (prop_assoc1toNdigraph eg)
   where
-  properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[Argument 0])]
+  properties = [ Propositions [mkProposition digraphModule "prop_assoc1toNdigraph" `ofType` BoolProposition `withSignature` [Argument 0]]
                    Specify "assoc1toNdigraph" []
-               , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[Argument 0])]
+               , Propositions [mkProposition digraphModule "prop_mergeAndSortTargets" `ofType` BoolProposition `withSignature` [Argument 0]]
                    Specify "mergeAndSortTargets" []
-               , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[Argument 0])]
+               , Propositions [mkProposition digraphModule "prop_addMissingSources" `ofType` BoolProposition `withSignature` [Argument 0]]
                    Specify "addMissingSources" []
                ]
   digraphModule = Module "Digraph" "../examples/Digraph_not_data_invariant__with_properties/"
diff --git a/examples/ExpressionSimplifier/Main2.hs b/examples/ExpressionSimplifier/Main2.hs
--- a/examples/ExpressionSimplifier/Main2.hs
+++ b/examples/ExpressionSimplifier/Main2.hs
@@ -6,8 +6,11 @@
 -- main = quickcheck prop_idemSimplify
 main = testOwp properties prop_idemSimplify (Mul (Const 1) (Const 2))
   where
-  properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[Argument 0])]      PropertiesOf "one" []
-               , Propositions [(BoolProposition,myModule,"prop_idemZero",[Argument 0])]     PropertiesOf "zero" []
-               , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[Argument 0])] PropertiesOf "simplify" []
+  properties = [ Propositions [mkProposition myModule "prop_idemOne" `ofType` BoolProposition `withSignature` [Argument 0]
+                              ] PropertiesOf "one" []
+               , Propositions [ mkProposition myModule "prop_idemZero" `ofType` BoolProposition `withSignature` [Argument 0]
+                              ] PropertiesOf "zero" []
+               , Propositions [ mkProposition myModule "prop_idemSimplify" `ofType` BoolProposition `withSignature` [Argument 0]
+                              ] PropertiesOf "simplify" []
                ]
   myModule = Module "MyModule" "../examples/ExpressionSimplifier"
diff --git a/examples/Nubsort/Main.hs b/examples/Nubsort/Main.hs
--- a/examples/Nubsort/Main.hs
+++ b/examples/Nubsort/Main.hs
@@ -3,16 +3,32 @@
 
 main = testOwp ps prop_nub_idempotent [2,1,1]
   where
-  ps = [ Propositions [ (BoolProposition,nubsortModule,"prop_nub_idempotent",[Argument 0])
-                      , (BoolProposition,nubsortModule,"prop_nub_unique",[Argument 0])
-                      , (BoolProposition,nubsortModule,"prop_nub_complete",[Argument 0])
+  ps = [ Propositions [ mkProposition nubsortModule "prop_nub_idempotent" 
+                          `ofType` BoolProposition 
+                          `withSignature`[Argument 0]
+                      , mkProposition nubsortModule "prop_nub_unique"
+                          `ofType` BoolProposition 
+                          `withSignature`[Argument 0]
+                      , mkProposition nubsortModule "prop_nub_complete"
+                          `ofType` BoolProposition 
+                          `withSignature`[Argument 0]
                       ] PropertiesOf "nub" []
-       , Propositions [ (QuickCheckProposition,nubsortModule,"prop_nubord'_idempotent",[Argument 1,Argument 0])
-                      , (QuickCheckProposition,nubsortModule,"prop_nubord'_unique",[Argument 1,Argument 0])
-                      , (QuickCheckProposition,nubsortModule,"prop_nubord'_complete",[Argument 1,Argument 0])
+       , Propositions [ mkProposition nubsortModule "prop_nubord'_idempotent"
+                          `ofType` QuickCheckProposition
+                          `withSignature`[Argument 1, Argument 0]
+                      , mkProposition nubsortModule "prop_nubord'_unique"
+                          `ofType` QuickCheckProposition
+                          `withSignature`[Argument 1, Argument 0]
+                      , mkProposition nubsortModule "prop_nubord'_complete"
+                          `ofType` QuickCheckProposition
+                          `withSignature`[Argument 1, Argument 0]
                       ] PropertiesOf "nubord'" [modQuickCheck]
-       , Propositions [ (QuickCheckProposition,nubsortModule,"prop_insert_ordered",[Argument 1,Argument 0])
-                      , (QuickCheckProposition,nubsortModule,"prop_insert_complete",[Argument 1,Argument 0])
+       , Propositions [ mkProposition nubsortModule "prop_insert_ordered"
+                          `ofType` QuickCheckProposition
+                          `withSignature`[Argument 1, Argument 0]
+                      , mkProposition nubsortModule "prop_insert_complete"
+                          `ofType` QuickCheckProposition
+                          `withSignature`[Argument 1, Argument 0]
                       ] PropertiesOf "insert" [modQuickCheck]
        ]
   nubsortModule = Module "Nubsort" "../examples/Nubsort/"
diff --git a/examples/Queens__with_properties/Main2.hs b/examples/Queens__with_properties/Main2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens__with_properties/Main2.hs
@@ -0,0 +1,3 @@
+import Queens
+
+main = doit2
diff --git a/examples/Queens__with_properties/Main3.hs b/examples/Queens__with_properties/Main3.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens__with_properties/Main3.hs
@@ -0,0 +1,3 @@
+import Queens3
+
+main = doit
diff --git a/examples/Queens_defective_filter__with_properties/Main.hs b/examples/Queens_defective_filter__with_properties/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens_defective_filter__with_properties/Main.hs
@@ -0,0 +1,3 @@
+import Queens
+
+main = doit
diff --git a/examples/Raincat/src/Main.hs b/examples/Raincat/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/Raincat/src/Main.hs
@@ -0,0 +1,30 @@
+module Main (main) where
+
+import Graphics.UI.GLUT
+import System.Exit
+import Game.GameInput
+import Game.GameInit
+import World.World
+import Settings.DisplaySettings as DisplaySettings
+import qualified Nxt.Graphics as NG
+import Data.IORef
+import Program.Program
+import Debug.Hoed.Pure
+
+main :: IO ()
+main = runO $ do
+    NG.initWindow screenRes "Raincat"
+    NG.initGraphics screenResWidth screenResHeight
+
+    worldState <- gameInit
+    worldStateRef <- newIORef worldState
+
+    displayCallback $= programDraw worldStateRef
+
+    keyboardMouseCallback $= Just (gameInput (keysStateRef worldState))
+    motionCallback $= Just (gameMotion (mousePosRef worldState))
+    passiveMotionCallback $= Just (gameMotion (mousePosRef worldState))
+
+    addTimerCallback 1 (programMain worldStateRef)
+
+    mainLoop
diff --git a/examples/SternBrocot.lhs b/examples/SternBrocot.lhs
new file mode 100644
--- /dev/null
+++ b/examples/SternBrocot.lhs
@@ -0,0 +1,97 @@
+We need the Template Haskell extension to splice in the generated
+Observable instances. We need the Rank2Types extionsion to be able
+to specify parametrized types such as 'Tree a' with forall a.
+
+> {-# LANGUAGE TemplateHaskell, Rank2Types #-}
+
+We need the Derive Generic extention to derive the Generic representation
+used for the non spliced in observe (see the Cache data type).
+
+> {-# LANGUAGE DeriveGeneric #-}
+
+> import Debug.Hoed.Pure
+
+We use the Stern–Brocot tree as example. The Stern-Brocot tree is a
+binary tree containing all rational numbers. The tree is infinit and
+is therefore a nice example to demonstrate how laziness is handled.
+
+To store the tree we use the following datatype, note that because
+our definition is endless we do not actually use Leaf.
+
+> data Tree a = Node a (Tree a) (Tree a) deriving Generic
+
+The values in the tree will be fractional numbers:
+
+> data Frac = Frac Int Int deriving (Show,Generic)
+
+We use cache to store what the last seen up and to the left, and up and
+to the right values are.
+
+> data Cache = Cache { v :: Frac
+>                    , l :: Frac
+>                    , r :: Frac
+>                    } deriving Generic
+
+Make Cache and Frac Observable for gdmobserve.
+
+> instance Observable Cache
+> instance Observable Frac
+
+The mediant is used to find which new number to insert between 2 exisiting
+numbers.
+
+> mediant :: Frac -> Frac -> Frac
+> mediant (Frac p1 q1) (Frac p2 q2) = Frac (p1+p2) (q1+q2)
+
+Definition of the sternbrocot tree:
+
+> sternbrocot :: Tree Frac
+> sternbrocot = sternbrocot' mediant
+>
+> sternbrocot' :: (Frac -> Frac -> Frac) -> Tree Frac
+> sternbrocot' m = w_sternbrocot m Cache{v=(Frac 1 1), l=(Frac 0 1), r=(Frac 1 0)}
+>
+> w_sternbrocot :: (Frac -> Frac -> Frac) -> Cache -> Tree Frac
+> w_sternbrocot m cache
+>  = let Cache{v=v, l=l, r=r} = cache -- observe "cache" cache
+>    in  Node v (w_sternbrocot m Cache{v=m v l, l=l, r=v})
+>               (w_sternbrocot m Cache{v=m v r, l=v, r=r})
+
+The Stern-Brocot tree is sorted: all values in the left subtree are
+smaller than the value of the current node and all values in the right subtree
+are greater than the value in the current node.
+This can be used to approximate a Float value by doing a binary search where
+each next rational number is a better aproximation of the Float.
+
+> toFrac :: Float -> Tree Frac -> Frac
+> toFrac val (Node frac@(Frac p q) left right)
+>  = case compare ((fromIntegral p) / (fromIntegral q)) val of
+>       LT -> toFrac val right 
+>       GT -> toFrac val left
+>       EQ -> frac
+
+We use template-haskell to observe Tree and the values stored in Tree.
+
+> $(observedTypes "sternbrocot1" [ [t| forall a . Observable a => Tree a |]
+>                                , [t| Frac |]
+>                                ]
+>  )
+>
+> frac1 = toFrac 0.6 ($(observeTempl "sternbrocot1") sternbrocot)
+
+Or to only observe which part of the tree is walked while ignoring
+the values stored in the tree.
+
+> $(observedTypes "sternbrocot2" [ [t| forall a . Tree a |]])
+>
+> frac2 = toFrac 0.6 ($(observeTempl "sternbrocot2") sternbrocot)
+
+> instance (Observable a) => Observable (Tree a)
+>
+> frac3 = toFrac 0.6 (observe "sternbrocot3" sternbrocot)
+
+Example main function:
+
+> main = runO $ do -- print frac1
+>                  -- print frac2
+>                  print frac3
diff --git a/examples/XMonad_changing_focus_duplicates_windows__test_only/Main.hs b/examples/XMonad_changing_focus_duplicates_windows__test_only/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/XMonad_changing_focus_duplicates_windows__test_only/Main.hs
@@ -0,0 +1,171 @@
+import Properties
+import Debug.Hoed.NoTrace
+import System.Environment
+import Text.Printf
+import Control.Monad
+import System.Random
+import Test.QuickCheck
+import Data.Maybe
+import XMonad.StackSet
+import qualified Data.Map as M
+
+myStackSet :: T
+myStackSet = StackSet {current = Screen {workspace = Workspace {tag = NonNegative 2, layout = -2, stack = Just (Stack {focus = 'c', up = "", down = "z"})}, screen = 2, screenDetail = 1}, visible = [Screen {workspace = Workspace {tag = NonNegative 0, layout = -2, stack = Just (Stack {focus = 'd', up = "", down = ""})}, screen = 1, screenDetail = -2},Screen {workspace = Workspace {tag = NonNegative 3, layout = -2, stack = Just (Stack {focus = 'v', up = "", down = ""})}, screen = 3, screenDetail = -1},Screen {workspace = Workspace {tag = NonNegative 4, layout = -2, stack = Just (Stack {focus = 'w', up = "", down = "i"})}, screen = 0, screenDetail = -2}], hidden = [Workspace {tag = NonNegative 1, layout = -2, stack = Just (Stack {focus = 'n', up = "", down = ""})},Workspace {tag = NonNegative 0, layout = -2, stack = Nothing},Workspace {tag = NonNegative 4, layout = -2, stack = Nothing}], floating = M.fromList []}
+
+
+
+main = do
+    args <- fmap (drop 1) getArgs
+    let n = if null args then 100 else read (head args)
+    (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-40s: " s >> a n) tests
+    printf "Passed %d tests!\n" (sum passed)
+    when (not . and $ results) $ fail "Not all tests passed!"
+
+    where
+
+    tests = zipWith (\(name,test) number -> (show number ++ ": " ++ name,test)) tests' [1..]
+
+    tests' =
+        [("prop_invariant" , mytest prop_invariant)
+
+        ,("prop_empty_I"    , mytest prop_empty_I)
+        ,("prop_empty"      , mytest prop_empty)
+        ,("prop_empty_current"     , mytest prop_empty_current)
+        ,("prop_member_empty"      , mytest prop_member_empty)
+
+        ,("prop_view_I"    , mytest prop_view_I)
+        ,("prop_view_current"   , mytest prop_view_current)
+        ,("prop_view_idem"     , mytest prop_view_idem)
+        ,("prop_view_reversible"    , mytest prop_view_reversible)
+        ,("prop_view_local"       , mytest prop_view_local)
+
+        ,("prop_view_greedyView_I"    , mytest prop_greedyView_I)
+        ,("prop_greedyView_current"   , mytest prop_greedyView_current)
+        ,("prop_greedyView_current_id"   ,   mytest prop_greedyView_current_id)
+        ,("prop_greedyView_idem"     , mytest prop_greedyView_idem)
+        ,("prop_greedyView_reversible"     , mytest prop_greedyView_reversible)
+        ,("prop_greedyView_local"       , mytest prop_greedyView_local)
+
+        ,("prop_member_peek"        , mytest prop_member_peek)
+
+        ,("prop_index_length"        , mytest prop_index_length)
+
+        ,("prop_focusUp_I", mytest prop_focusUp_I)
+        ,("prop_focusMaster_I", mytest prop_focusMaster_I)
+        ,("prop_focusDown_I", mytest prop_focusDown_I)
+        ,("prop_focus_I", mytest prop_focus_I)
+        ,("prop_focus_left_master"   , mytest prop_focus_left_master)
+        ,("prop_focus_right_master"  , mytest prop_focus_right_master)
+        ,("prop_focus_master_master"  , mytest prop_focus_master_master)
+        ,("prop_focusWindow_master"  , mytest prop_focusWindow_master)
+        ,("prop_focus_left"    , mytest prop_focus_left)
+        ,("prop_focus_right"    , mytest prop_focus_right)
+        ,("prop_focus_all_l"    , mytest prop_focus_all_l)
+        ,("prop_focus_all_r"    , mytest prop_focus_all_r)
+        ,("prop_focus_down_local"      , mytest prop_focus_down_local)
+        ,("prop_focus_up_local"      , mytest prop_focus_up_local)
+        ,("prop_focus_master_local"      , mytest prop_focus_master_local)
+        ,("prop_focusMaster_idem"  , mytest prop_focusMaster_idem)
+
+        ,("prop_focusWindow_local", mytest prop_focusWindow_local)
+        ,("prop_focusWindow_works"   , mytest prop_focusWindow_works)
+        ,("prop_focusWindow_identity", mytest prop_focusWindow_identity)
+
+        ,("prop_findIndex"           , mytest prop_findIndex)
+        ,("prop_allWindowsMember"   , mytest prop_allWindowsMember)
+        ,("prop_currentTag"          , mytest prop_currentTag)
+
+        ,("prop_insertUp_I"   , mytest prop_insertUp_I)
+        ,("prop_insert_empty/new"          , mytest prop_insert_empty)
+        ,("prop_insert_idem", mytest prop_insert_idem)
+        ,("prop_insert_delete", mytest prop_insert_delete)
+        ,("prop_insert_local"     , mytest prop_insert_local)
+        ,("prop_insert_duplicate"   , mytest prop_insert_duplicate)
+        ,("prop_insert_peek"        , mytest prop_insert_peek)
+        ,("prop_size_insert"         , mytest prop_size_insert)
+
+        ,("prop_delete_I"   , mytest prop_delete_I)
+        ,("prop_empty"        , mytest prop_empty)
+        ,("prop_delete"       , mytest prop_delete)
+        ,("prop_delete_insert", mytest prop_delete_insert)
+        ,("prop_delete_local"     , mytest prop_delete_local)
+        ,("prop_delete_focus"        , mytest prop_delete_focus)
+        ,("prop_delete_focus_end", mytest prop_delete_focus_end)
+        ,("prop_delete_focus_not_end", mytest prop_delete_focus_not_end)
+
+        ,("prop_filter_order", mytest prop_filter_order)
+
+        ,("prop_swap_master_I", mytest prop_swap_master_I)
+        ,("prop_swap_left_I" , mytest prop_swap_left_I)
+        ,("prop_swap_right_I", mytest prop_swap_right_I)
+        ,("prop_swap_master_focus", mytest prop_swap_master_focus)
+        ,("prop_swap_left_focus", mytest prop_swap_left_focus)
+        ,("prop_swap_right_focus", mytest prop_swap_right_focus)
+        ,("prop_swap_master_idempotent", mytest prop_swap_master_idempotent)
+        ,("prop_swap_all_l"     , mytest prop_swap_all_l)
+        ,("prop_swap_all_r"     , mytest prop_swap_all_r)
+        ,("prop_swap_master_local" , mytest prop_swap_master_local)
+        ,("prop_swap_left_local"   , mytest prop_swap_left_local)
+        ,("prop_swap_right_local"  , mytest prop_swap_right_local)
+
+        ,("prop_shift_master_focus", mytest prop_shift_master_focus)
+        ,("prop_shift_master_local", mytest prop_shift_master_local)
+        ,("prop_shift_master_idempotent", mytest prop_shift_master_idempotent)
+        ,("prop_shift_master_ordering", mytest prop_shift_master_ordering)
+
+        ,("prop_shift_I"    , mytest prop_shift_I)
+        ,("prop_shift_reversible" , mytest prop_shift_reversible)
+        ,("prop_shift_win_I" , mytest prop_shift_win_I)
+        ,("prop_shift_win_focus" , mytest prop_shift_win_focus)
+        ,("prop_shift_win_fix_current" , mytest prop_shift_win_fix_current)
+
+        ,("prop_float_reversible" , mytest prop_float_reversible)
+        ,("prop_float_geometry" , mytest prop_float_geometry)
+        ,("prop_float_delete", mytest prop_float_delete)
+        ,("prop_screens", mytest prop_screens)
+
+        ,("prop_differentiate", mytest prop_differentiate)
+        ,("prop_lookup_current", mytest prop_lookup_current)
+        ,("prop_lookup_visible", mytest prop_lookup_visible)
+        ,("prop_screens_works",      mytest prop_screens_works)
+        ,("prop_rename1",     mytest prop_rename1)
+        ,("prop_ensure",     mytest prop_ensure)
+        ,("prop_ensure_append",     mytest prop_ensure_append)
+
+        ,("prop_mapWorkspaceId", mytest prop_mapWorkspaceId)
+        ,("prop_mapWorkspaceInverse", mytest prop_mapWorkspaceInverse)
+        ,("prop_mapLayoutId", mytest prop_mapLayoutId)
+        ,("prop_mapLayoutInverse", mytest prop_mapLayoutInverse)
+
+        -- testing for failure:
+        ,("prop_abort",            mytest prop_abort)
+        ,("prop_new_abort",   mytest prop_new_abort)
+        ,("prop_shift_win_indentity",      mytest prop_shift_win_indentity)
+
+        -- tall layout
+
+        ,("prop_tile_fullscreen", mytest prop_tile_fullscreen)
+        ,("prop_tile_non_overlap",    mytest prop_tile_non_overlap)
+        ,("prop_split_hoziontal",     mytest prop_split_hoziontal)
+        ,("prop_splitVertically",       mytest prop_splitVertically)
+
+        ,("prop_purelayout_tall",       mytest prop_purelayout_tall)
+        ,("prop_shrink_tall",    mytest prop_shrink_tall)
+        ,("prop_expand_tall",    mytest prop_expand_tall)
+        ,("prop_incmaster_tall",    mytest prop_incmaster_tall)
+
+        -- full layout
+
+        ,("prop_purelayout_full",       mytest prop_purelayout_full)
+        ,("prop_sendmsg_full",      mytest prop_sendmsg_full)
+        ,("prop_desc_full",          mytest prop_desc_full)
+
+        ,("prop_desc_mirror",        mytest prop_desc_mirror)
+
+        -- resize hints
+        ,("prop_resize_inc",      mytest prop_resize_inc)
+        ,("prop_resize_inc_extra",  mytest prop_resize_inc_extra)
+        ,("prop_resize_max",      mytest prop_resize_max)
+        ,("prop_resize_max_extra", mytest prop_resize_max_extra)
+
+        ]
diff --git a/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs b/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs
--- a/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs
+++ b/examples/XMonad_changing_focus_duplicates_windows__using_properties/Main.hs
@@ -13,213 +13,81 @@
 myStackSet = StackSet {current = Screen {workspace = Workspace {tag = NonNegative 2, layout = -2, stack = Just (Stack {focus = 'c', up = "", down = "z"})}, screen = 2, screenDetail = 1}, visible = [Screen {workspace = Workspace {tag = NonNegative 0, layout = -2, stack = Just (Stack {focus = 'd', up = "", down = ""})}, screen = 1, screenDetail = -2},Screen {workspace = Workspace {tag = NonNegative 3, layout = -2, stack = Just (Stack {focus = 'v', up = "", down = ""})}, screen = 3, screenDetail = -1},Screen {workspace = Workspace {tag = NonNegative 4, layout = -2, stack = Just (Stack {focus = 'w', up = "", down = "i"})}, screen = 0, screenDetail = -2}], hidden = [Workspace {tag = NonNegative 1, layout = -2, stack = Just (Stack {focus = 'n', up = "", down = ""})},Workspace {tag = NonNegative 0, layout = -2, stack = Nothing},Workspace {tag = NonNegative 4, layout = -2, stack = Nothing}], floating = M.fromList []}
 
 
-
-{- Running all tests
-main = do
-    args <- fmap (drop 1) getArgs
-    let n = if null args then 100 else read (head args)
-    (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-40s: " s >> a n) tests
-    printf "Passed %d tests!\n" (sum passed)
-    when (not . and $ results) $ fail "Not all tests passed!"
--}
-
 main :: IO ()
 main = runOwp propositions $ do
   g <- newStdGen
-  print . fromJust . ok . (generate 1 g) . evaluate $  prop_shift_win_I 1 'd' myStackSet
+  print . fromJust . ok . (generate 1 g) . evaluate $  prop_shift_win_I shiftWin 1 'd' myStackSet
   where
     propositions =
-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])
-                      ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[Argument 0])
+        [ Propositions [mkProposition module_Properties "prop_shift_win_I"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [SubjectFunction, Argument 0, Argument 1, Argument 2]
+                          `withTestGen` TestGenLegacyQuickCheck
+                       ]
+                       PropertiesOf "shiftWin" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
+        , Propositions [mkProposition module_Properties "prop_focus_all_l"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
+                          `withTestGen` TestGenLegacyQuickCheck
+                      ,mkProposition module_Properties "prop_focus_all_l_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
+                          `withTestGen` TestGenLegacyQuickCheck
                       ]
                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[Argument 1,Argument 0])
+        , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                          `withTestGen` TestGenLegacyQuickCheck
                        ] 
                        PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 0,Argument 1])
+        , Propositions [ mkProposition module_Properties "prop_view_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                          `withTestGen` TestGenLegacyQuickCheck
+                         , mkProposition module_Properties "prop_view_I"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [SubjectFunction, Argument 0, Argument 1]
+                          `withTestGen` TestGenLegacyQuickCheck
+                         , mkProposition module_Properties "prop_view_current"
+                            `ofType` LegacyQuickCheckProposition
+                            `withSignature` [Argument 1, Argument 0]
+                            `withTestGen` TestGenLegacyQuickCheck
+                         , mkProposition module_Properties "prop_view_idem"
+                            `ofType` LegacyQuickCheckProposition
+                            `withSignature` [Argument 1, Argument 0]
+                            `withTestGen` TestGenLegacyQuickCheck
+                         , mkProposition module_Properties "prop_view_local"
+                            `ofType` LegacyQuickCheckProposition
+                            `withSignature` [Argument 1, Argument 0]
+                            `withTestGen` TestGenLegacyQuickCheck
                        ] 
                        PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])
+        , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                          `withTestGen` TestGenLegacyQuickCheck
+                       , mkProposition module_Properties "prop_greedyView_idem"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                          `withTestGen` TestGenLegacyQuickCheck
                        ] 
                        PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
+        , Propositions [ mkProposition module_Properties "prop_findIndex"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1]
+                          `withTestGen` TestGenLegacyQuickCheck
+                       ]
+                       PropertiesOf "findTag" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
         ]
 
-    module_Properties = Module "Properties"              "../examples/XMonad_changing_focus_duplicates_windows/"
-    module_StackSet   = Module "XMonad.StackSet"         "../examples/XMonad_changing_focus_duplicates_windows/"
-    module_QuickCheck = Module "Test.QuickCheck"         "../examples/XMonad_changing_focus_duplicates_windows/"
+    module_Properties = Module "Properties"              "../examples/XMonad_changing_focus_duplicates_windows__using_properties/"
+    module_StackSet   = Module "XMonad.StackSet"         "../examples/XMonad_changing_focus_duplicates_windows__using_properties/"
+    module_QuickCheck = Module "Test.QuickCheck"         "../examples/XMonad_changing_focus_duplicates_windows__using_properties/"
     module_Map        = Module "qualified Data.Map as M" ""
     module_Random     = Module "System.Random"           ""
     module_Maybe      = Module "Data.Maybe"              ""
-
-    tests =
-        [("shiftMaster id on focus", mytest prop_shift_master_focus)
-        -- ,("shiftMaster is local", mytest prop_shift_master_local)
-        -- ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent)
-        -- ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering)
-
-        -- ,("shift: invariant"    , mytest prop_shift_I)
-        -- ,("shift is reversible" , mytest prop_shift_reversible)
-        ,("shiftWin: invariant" , mytest prop_shift_win_I)
-        ,("shiftWin is shift on focus" , mytest prop_shift_win_focus)
-        ,("shiftWin fix current" , mytest prop_shift_win_fix_current)
-        ]
-
-{-
-        [("StackSet invariants" , mytest prop_invariant)
-
-        ,("empty: invariant"    , mytest prop_empty_I)
-        ,("empty is empty"      , mytest prop_empty)
-        ,("empty / current"     , mytest prop_empty_current)
-        ,("empty / member"      , mytest prop_member_empty)
-
-        ,("view : invariant"    , mytest prop_view_I)
-        ,("view sets current"   , mytest prop_view_current)
-        ,("view idempotent"     , mytest prop_view_idem)
-        ,("view reversible"    , mytest prop_view_reversible)
---      ,("view / xinerama"     , mytest prop_view_xinerama)
-        ,("view is local"       , mytest prop_view_local)
-
-        ,("greedyView : invariant"    , mytest prop_greedyView_I)
-        ,("greedyView sets current"   , mytest prop_greedyView_current)
-        ,("greedyView is safe "   ,   mytest prop_greedyView_current_id)
-        ,("greedyView idempotent"     , mytest prop_greedyView_idem)
-        ,("greedyView reversible"     , mytest prop_greedyView_reversible)
-        ,("greedyView is local"       , mytest prop_greedyView_local)
---
---      ,("valid workspace xinerama", mytest prop_lookupWorkspace)
-
-        ,("peek/member "        , mytest prop_member_peek)
-
-        ,("index/length"        , mytest prop_index_length)
-
-        ,("focus left : invariant", mytest prop_focusUp_I)
-        ,("focus master : invariant", mytest prop_focusMaster_I)
-        ,("focus right: invariant", mytest prop_focusDown_I)
-        ,("focusWindow: invariant", mytest prop_focus_I)
-        ,("focus left/master"   , mytest prop_focus_left_master)
-        ,("focus right/master"  , mytest prop_focus_right_master)
-        ,("focus master/master"  , mytest prop_focus_master_master)
-        ,("focusWindow master"  , mytest prop_focusWindow_master)
-        ,("focus left/right"    , mytest prop_focus_left)
-        ,("focus right/left"    , mytest prop_focus_right)
-        ,("focus all left  "    , mytest prop_focus_all_l)
-        ,("focus all right "    , mytest prop_focus_all_r)
-        ,("focus down is local"      , mytest prop_focus_down_local)
-        ,("focus up is local"      , mytest prop_focus_up_local)
-        ,("focus master is local"      , mytest prop_focus_master_local)
-        ,("focus master idemp"  , mytest prop_focusMaster_idem)
-
-        ,("focusWindow is local", mytest prop_focusWindow_local)
-        ,("focusWindow works"   , mytest prop_focusWindow_works)
-        ,("focusWindow identity", mytest prop_focusWindow_identity)
-
-        ,("findTag"           , mytest prop_findIndex)
-        ,("allWindows/member"   , mytest prop_allWindowsMember)
-        ,("currentTag"          , mytest prop_currentTag)
-
-        ,("insert: invariant"   , mytest prop_insertUp_I)
-        ,("insert/new"          , mytest prop_insert_empty)
-        ,("insert is idempotent", mytest prop_insert_idem)
-        ,("insert is reversible", mytest prop_insert_delete)
-        ,("insert is local"     , mytest prop_insert_local)
-        ,("insert duplicates"   , mytest prop_insert_duplicate)
-        ,("insert/peek "        , mytest prop_insert_peek)
-        ,("insert/size"         , mytest prop_size_insert)
-
-        ,("delete: invariant"   , mytest prop_delete_I)
-        ,("delete/empty"        , mytest prop_empty)
-        ,("delete/member"       , mytest prop_delete)
-        ,("delete is reversible", mytest prop_delete_insert)
-        ,("delete is local"     , mytest prop_delete_local)
-        ,("delete/focus"        , mytest prop_delete_focus)
-        ,("delete  last/focus up", mytest prop_delete_focus_end)
-        ,("delete ~last/focus down", mytest prop_delete_focus_not_end)
-
-        ,("filter preserves order", mytest prop_filter_order)
-
-        ,("swapMaster: invariant", mytest prop_swap_master_I)
-        ,("swapUp: invariant" , mytest prop_swap_left_I)
-        ,("swapDown: invariant", mytest prop_swap_right_I)
-        ,("swapMaster id on focus", mytest prop_swap_master_focus)
-        ,("swapUp id on focus", mytest prop_swap_left_focus)
-        ,("swapDown id on focus", mytest prop_swap_right_focus)
-        ,("swapMaster is idempotent", mytest prop_swap_master_idempotent)
-        ,("swap all left  "     , mytest prop_swap_all_l)
-        ,("swap all right "     , mytest prop_swap_all_r)
-        ,("swapMaster is local" , mytest prop_swap_master_local)
-        ,("swapUp is local"   , mytest prop_swap_left_local)
-        ,("swapDown is local"  , mytest prop_swap_right_local)
-
-        ,("shiftMaster id on focus", mytest prop_shift_master_focus)
-        ,("shiftMaster is local", mytest prop_shift_master_local)
-        ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent)
-        ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering)
-
-        ,("shift: invariant"    , mytest prop_shift_I)
-        ,("shift is reversible" , mytest prop_shift_reversible)
-        ,("shiftWin: invariant" , mytest prop_shift_win_I)
-        ,("shiftWin is shift on focus" , mytest prop_shift_win_focus)
-        ,("shiftWin fix current" , mytest prop_shift_win_fix_current)
-
-        ,("floating is reversible" , mytest prop_float_reversible)
-        ,("floating sets geometry" , mytest prop_float_geometry)
-        ,("floats can be deleted", mytest prop_float_delete)
-        ,("screens includes current", mytest prop_screens)
-
-        ,("differentiate works", mytest prop_differentiate)
-        ,("lookupTagOnScreen", mytest prop_lookup_current)
-        ,("lookupTagOnVisbleScreen", mytest prop_lookup_visible)
-        ,("screens works",      mytest prop_screens_works)
-        ,("renaming works",     mytest prop_rename1)
-        ,("ensure works",     mytest prop_ensure)
-        ,("ensure hidden semantics",     mytest prop_ensure_append)
-
-        ,("mapWorkspace id", mytest prop_mapWorkspaceId)
-        ,("mapWorkspace inverse", mytest prop_mapWorkspaceInverse)
-        ,("mapLayout id", mytest prop_mapLayoutId)
-        ,("mapLayout inverse", mytest prop_mapLayoutInverse)
-
-        -- testing for failure:
-        ,("abort fails",            mytest prop_abort)
-        ,("new fails with abort",   mytest prop_new_abort)
-        ,("shiftWin identity",      mytest prop_shift_win_indentity)
-
-        -- tall layout
-
-        ,("tile 1 window fullsize", mytest prop_tile_fullscreen)
-        ,("tiles never overlap",    mytest prop_tile_non_overlap)
-        ,("split hozizontally",     mytest prop_split_hoziontal)
-        ,("split verticalBy",       mytest prop_splitVertically)
-
-        ,("pure layout tall",       mytest prop_purelayout_tall)
-        ,("send shrink    tall",    mytest prop_shrink_tall)
-        ,("send expand    tall",    mytest prop_expand_tall)
-        ,("send incmaster tall",    mytest prop_incmaster_tall)
-
-        -- full layout
-
-        ,("pure layout full",       mytest prop_purelayout_full)
-        ,("send message full",      mytest prop_sendmsg_full)
-        ,("describe full",          mytest prop_desc_full)
-
-        ,("describe mirror",        mytest prop_desc_mirror)
-
-        -- resize hints
-        ,("window hints: inc",      mytest prop_resize_inc)
-        ,("window hints: inc all",  mytest prop_resize_inc_extra)
-        ,("window hints: max",      mytest prop_resize_max)
-        ,("window hints: max all ", mytest prop_resize_max_extra)
-
-        ]
--}
-
-
diff --git a/examples/afp02Exercises/Compiler__with_properties/Main.hs b/examples/afp02Exercises/Compiler__with_properties/Main.hs
--- a/examples/afp02Exercises/Compiler__with_properties/Main.hs
+++ b/examples/afp02Exercises/Compiler__with_properties/Main.hs
@@ -14,7 +14,10 @@
   putStrLn "compiled:"
   print (exec (compile prog))
   where
-  properties = [Propositions [(BoolProposition,modInterpreter,"prop_ifT",[Argument 1,Argument 0])] PropertiesOf "run" [modSyntax,modValue,modQuickCheck]
+  properties = [Propositions [mkProposition modInterpreter "prop_ifT"
+                                `ofType` BoolProposition 
+                                `withSignature`[Argument 1, Argument 0]
+                ]PropertiesOf "run" [modSyntax,modValue,modQuickCheck]
                ]
   modInterpreter = Module "Interpreter" "../examples/afp02Exercises/Compiler__with_properties/"
   modValue = Module "Value" "../examples/afp02Exercises/Compiler__with_properties/"
diff --git a/examples/filter__with_properties/Main.hs b/examples/filter__with_properties/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/filter__with_properties/Main.hs
@@ -0,0 +1,3 @@
+import Even
+
+main = doit
diff --git a/img/test.png b/img/test.png
new file mode 100644
Binary files /dev/null and b/img/test.png differ
diff --git a/run b/run
--- a/run
+++ b/run
@@ -42,6 +42,9 @@
 # else
 # ../dist/build/$EXE/$EXE +RTS -p -h -L80
 # fi
+
 eval ../dist/build/$EXE/$EXE
 
+# profile ....
+#../dist/build/$EXE/$EXE +RTS -hd -L80
 
diff --git a/test.Generic b/test.Generic
--- a/test.Generic
+++ b/test.Generic
@@ -3,12 +3,11 @@
 TESTS="0 1 2 3"
 FAIL=0
 
-
+echo
 echo "Testing parallel equality for Generic types"
 echo
 
 x=`./dist/build/hoed-tests-ParEq/hoed-tests-ParEq`
-echo "x is $x"
 if [ $x = "True" ]; then
     echo -n "[OK"
 else
@@ -19,7 +18,7 @@
 fi
   echo "] Generic.ParEq"
 
-
+echo
 echo "Testing events produced for Observable derived for Generic types"
 echo
 
diff --git a/tests/Prop/t0/Main.hs b/tests/Prop/t0/Main.hs
--- a/tests/Prop/t0/Main.hs
+++ b/tests/Prop/t0/Main.hs
@@ -6,8 +6,14 @@
 -- main = quickcheck prop_idemSimplify
 main = logOwp Bottom "hoed-tests-Prop-t0.graph" properties $ print $ prop_idemSimplify (Mul (Const 1) (Const 2))
   where
-  properties = [ Propositions [(BoolProposition,myModule,"prop_idemOne",[Argument 0])]      PropertiesOf "one" []
-               , Propositions [(BoolProposition,myModule,"prop_idemZero",[Argument 0])]     PropertiesOf "zero" []
-               , Propositions [(BoolProposition,myModule,"prop_idemSimplify",[Argument 0])] PropertiesOf "simplify" []
+  properties = [ Propositions [mkProposition myModule "prop_idemOne"
+                                `ofType` BoolProposition
+                                `withSignature` [Argument 0]] PropertiesOf "one" []
+               , Propositions [mkProposition myModule "prop_idemZero"
+                                `ofType` BoolProposition
+                                `withSignature` [Argument 0]] PropertiesOf "zero" []
+               , Propositions [mkProposition myModule "prop_idemSimplify"
+                                `ofType` BoolProposition
+                                `withSignature` [Argument 0]] PropertiesOf "simplify" []
                ]
   myModule = Module "MyModule" "../Prop/t0/"
diff --git a/tests/Prop/t1/Main.hs b/tests/Prop/t1/Main.hs
--- a/tests/Prop/t1/Main.hs
+++ b/tests/Prop/t1/Main.hs
@@ -6,6 +6,11 @@
 main = logOwp Bottom "hoed-tests-Prop-t1.graph" properties $ print (prop_negin_correct eg)
 -- main = logOwp "hoed-tests-Prop-t1.graph" properties $ print (negin eg, prop_negin_correct eg)
   where
-  properties = [Propositions [(BoolProposition,cnfModule,"prop_negin_complete",[Argument 0]), (BoolProposition,cnfModule,"prop_negin_sound",[Argument 0])] Specify "negin" []
+  properties = [Propositions 
+                 [ mkProposition cnfModule "prop_negin_complete"
+                   `ofType` BoolProposition `withSignature` [Argument 0]
+                 , mkProposition cnfModule "prop_negin_sound"
+                   `ofType` BoolProposition `withSignature` [Argument 0]
+                 ] Specify "negin" []
                ]
   cnfModule  = Module "CNF" "../Prop/t1/"
diff --git a/tests/Prop/t2/Main.hs b/tests/Prop/t2/Main.hs
--- a/tests/Prop/t2/Main.hs
+++ b/tests/Prop/t2/Main.hs
@@ -5,8 +5,11 @@
 -- main = quickcheck prop_idem_negin_sound
 main = logOwp Bottom "hoed-tests-Prop-t2.graph" properties $ print (prop_assoc1toNdigraph eg)
   where
-  properties = [ Propositions [(BoolProposition,digraphModule,"prop_assoc1toNdigraph",[Argument 0])]    Specify "assoc1toNdigraph" []
-               , Propositions [(BoolProposition,digraphModule,"prop_mergeAndSortTargets",[Argument 0])] Specify "mergeAndSortTargets" []
-               , Propositions [(BoolProposition,digraphModule,"prop_addMissingSources",[Argument 0])]   Specify "addMissingSources" []
+  properties = [ Propositions [mkProposition digraphModule "prop_assoc1toNdigraph"    
+                                 `ofType` BoolProposition `withSignature` [Argument 0]] Specify "assoc1toNdigraph" []
+               , Propositions [mkProposition digraphModule "prop_mergeAndSortTargets"
+                                 `ofType` BoolProposition `withSignature` [Argument 0]] Specify "mergeAndSortTargets" []
+               , Propositions [mkProposition digraphModule "prop_addMissingSources" 
+                                 `ofType` BoolProposition `withSignature` [Argument 0]] Specify "addMissingSources" []
                ]
   digraphModule = Module "Digraph" "../Prop/t2/"
diff --git a/tests/Prop/t3/Main.hs b/tests/Prop/t3/Main.hs
--- a/tests/Prop/t3/Main.hs
+++ b/tests/Prop/t3/Main.hs
@@ -39,21 +39,45 @@
 
  where
     propositions =
-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])
-                      ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_generic",[Argument 0])
-                      -- ,(QuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])
+        [Propositions [mkProposition module_Properties "prop_focus_all_l"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
+                      ,mkProposition module_Properties "prop_focus_all_l_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
                       ]
                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 0,Argument 1])
+        , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
                        ] 
+                       PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
+
+        , Propositions [ mkProposition module_Properties "prop_view_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_I"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_current"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_idem"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                       , mkProposition module_Properties "prop_view_local"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                       ] 
                        PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])
+
+        , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_greedyView_idem"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
                        ] 
                        PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
diff --git a/tests/Prop/t4/Main.hs b/tests/Prop/t4/Main.hs
--- a/tests/Prop/t4/Main.hs
+++ b/tests/Prop/t4/Main.hs
@@ -29,25 +29,45 @@
   print . fromJust . ok . (generate 1 g) . evaluate $  prop_shift_win_I 1 'd' myStackSet
   where
     propositions =
-        [Propositions [(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l",[Argument 0])
-                      -- ,(LegacyQuickCheckProposition,module_Properties,"prop_focus_all_l_weak",[0])
+        [Propositions [mkProposition module_Properties "prop_focus_all_l"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
+                      ,mkProposition module_Properties "prop_focus_all_l_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0]
                       ]
                       PropertiesOf "focusUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        -- , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_insert_duplicate_weak",[1,0])
-        --                ] 
-        --                PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
+        , Propositions [ mkProposition module_Properties "prop_insert_duplicate_weak"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       ] 
+                       PropertiesOf "insertUp" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_view_reversible",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_I",[Argument 0,Argument 1])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_current",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_idem",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_view_local",[Argument 1,Argument 0])
+        , Propositions [ mkProposition module_Properties "prop_view_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_I"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_current"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_view_idem"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
+                       , mkProposition module_Properties "prop_view_local"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
                        ] 
                        PropertiesOf "view" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
-        , Propositions [ (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_reversible",[Argument 1,Argument 0])
-                       , (LegacyQuickCheckProposition,module_Properties,"prop_greedyView_idem",[Argument 0,Argument 1])
+        , Propositions [ mkProposition module_Properties "prop_greedyView_reversible"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 1, Argument 0]
+                       , mkProposition module_Properties "prop_greedyView_idem"
+                          `ofType` LegacyQuickCheckProposition
+                          `withSignature` [Argument 0, Argument 1]
                        ] 
                        PropertiesOf "greedyView" [module_StackSet, module_QuickCheck, module_Map, module_Random, module_Maybe]
 
diff --git a/tests/Prop/t5/Main.hs b/tests/Prop/t5/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Prop/t5/Main.hs
@@ -0,0 +1,3 @@
+import Even
+
+main = doit