diff --git a/src/UniqueLogic/ST/Duplicate.hs b/src/UniqueLogic/ST/Duplicate.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Duplicate.hs
@@ -0,0 +1,166 @@
+{- |
+This module provides several ways to cope with over-determined values.
+-}
+module UniqueLogic.ST.Duplicate (
+   C, accept,
+   Ignore(Ignore),
+   Forbid(Forbid),
+   Verify(Verify),
+   ) where
+
+
+class C a where
+   accept :: a -> a -> Bool
+
+instance (C a, C b) => C (a, b) where
+   accept (a0,b0) (a1,b1) =
+      accept a0 a1 && accept b0 b1
+
+instance (C a, C b, C c) => C (a, b, c) where
+   accept (a0,b0,c0) (a1,b1,c1) =
+      accept a0 a1 && accept b0 b1 && accept c0 c1
+
+
+{- |
+Ignore duplicate ways to determine a variable.
+The chosen value depends on the particular algorithm.
+-}
+newtype Ignore a = Ignore a deriving (Eq, Ord, Show)
+
+instance C (Ignore a) where accept _ _ = True
+
+ignore1 :: (a -> b) -> Ignore a -> Ignore b
+ignore1 f (Ignore x) = Ignore $ f x
+
+ignore2 :: (a -> b -> c) -> Ignore a -> Ignore b -> Ignore c
+ignore2 f (Ignore x) (Ignore y) = Ignore $ f x y
+
+instance Num a => Num (Ignore a) where
+   fromInteger = Ignore . fromInteger
+   (+) = ignore2 (+)
+   (-) = ignore2 (-)
+   (*) = ignore2 (*)
+   abs = ignore1 abs
+   signum = ignore1 signum
+
+instance Fractional a => Fractional (Ignore a) where
+   fromRational = Ignore . fromRational
+   (/) = ignore2 (/)
+
+instance Floating a => Floating (Ignore a) where
+   pi = Ignore pi
+   exp = ignore1 exp
+   sqrt = ignore1 sqrt
+   log = ignore1 log
+   (**) = ignore2 (**)
+   logBase = ignore2 logBase
+   sin = ignore1 sin
+   tan = ignore1 tan
+   cos = ignore1 cos
+   asin = ignore1 asin
+   atan = ignore1 atan
+   acos = ignore1 acos
+   sinh = ignore1 sinh
+   tanh = ignore1 tanh
+   cosh = ignore1 cosh
+   asinh = ignore1 asinh
+   atanh = ignore1 atanh
+   acosh = ignore1 acosh
+
+
+
+{- |
+Duplicate ways to determine a variable value
+are always considered an error.
+If you use @Rule@s or @Expression@s this is not a good idea,
+since every rule is over-determined.
+-}
+newtype Forbid a = Forbid a deriving (Eq, Ord, Show)
+
+instance C (Forbid a) where accept _ _ = False
+
+forbid1 :: (a -> b) -> Forbid a -> Forbid b
+forbid1 f (Forbid x) = Forbid $ f x
+
+forbid2 :: (a -> b -> c) -> Forbid a -> Forbid b -> Forbid c
+forbid2 f (Forbid x) (Forbid y) = Forbid $ f x y
+
+instance Num a => Num (Forbid a) where
+   fromInteger = Forbid . fromInteger
+   (+) = forbid2 (+)
+   (-) = forbid2 (-)
+   (*) = forbid2 (*)
+   abs = forbid1 abs
+   signum = forbid1 signum
+
+instance Fractional a => Fractional (Forbid a) where
+   fromRational = Forbid . fromRational
+   (/) = forbid2 (/)
+
+instance Floating a => Floating (Forbid a) where
+   pi = Forbid pi
+   exp = forbid1 exp
+   sqrt = forbid1 sqrt
+   log = forbid1 log
+   (**) = forbid2 (**)
+   logBase = forbid2 logBase
+   sin = forbid1 sin
+   tan = forbid1 tan
+   cos = forbid1 cos
+   asin = forbid1 asin
+   atan = forbid1 atan
+   acos = forbid1 acos
+   sinh = forbid1 sinh
+   tanh = forbid1 tanh
+   cosh = forbid1 cosh
+   asinh = forbid1 asinh
+   atanh = forbid1 atanh
+   acosh = forbid1 acosh
+
+
+{- |
+Duplicate ways to determine a variable value are allowed
+as long as every way yields the same result.
+\"Same\" is meant with respect to the 'Eq' class.
+-}
+newtype Verify a = Verify a deriving (Eq, Ord, Show)
+
+instance Eq a => C (Verify a) where accept (Verify x) (Verify y) = x==y
+
+verify1 :: (a -> b) -> Verify a -> Verify b
+verify1 f (Verify x) = Verify $ f x
+
+verify2 :: (a -> b -> c) -> Verify a -> Verify b -> Verify c
+verify2 f (Verify x) (Verify y) = Verify $ f x y
+
+instance Num a => Num (Verify a) where
+   fromInteger = Verify . fromInteger
+   (+) = verify2 (+)
+   (-) = verify2 (-)
+   (*) = verify2 (*)
+   abs = verify1 abs
+   signum = verify1 signum
+
+instance Fractional a => Fractional (Verify a) where
+   fromRational = Verify . fromRational
+   (/) = verify2 (/)
+
+instance Floating a => Floating (Verify a) where
+   pi = Verify pi
+   exp = verify1 exp
+   sqrt = verify1 sqrt
+   log = verify1 log
+   (**) = verify2 (**)
+   logBase = verify2 logBase
+   sin = verify1 sin
+   tan = verify1 tan
+   cos = verify1 cos
+   asin = verify1 asin
+   atan = verify1 atan
+   acos = verify1 acos
+   sinh = verify1 sinh
+   tanh = verify1 tanh
+   cosh = verify1 cosh
+   asinh = verify1 asinh
+   atanh = verify1 atanh
+   acosh = verify1 acosh
diff --git a/src/UniqueLogic/ST/Example/Expression.hs b/src/UniqueLogic/ST/Example/Expression.hs
--- a/src/UniqueLogic/ST/Example/Expression.hs
+++ b/src/UniqueLogic/ST/Example/Expression.hs
@@ -3,7 +3,7 @@
  where
 
 import qualified UniqueLogic.ST.Expression as Expr
-import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.System.Simple as Sys
 import UniqueLogic.ST.Expression ((=:=))
 
 import Control.Monad.ST (runST, )
diff --git a/src/UniqueLogic/ST/Example/Label.hs b/src/UniqueLogic/ST/Example/Label.hs
--- a/src/UniqueLogic/ST/Example/Label.hs
+++ b/src/UniqueLogic/ST/Example/Label.hs
@@ -2,9 +2,11 @@
 {-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
  where
 
+import qualified UniqueLogic.ST.Example.Term as Term
 import qualified UniqueLogic.ST.Expression as Expr
 import qualified UniqueLogic.ST.Rule as Rule
-import qualified UniqueLogic.ST.SystemLabel as Sys
+import qualified UniqueLogic.ST.System.Label as Sys
+import qualified UniqueLogic.ST.Duplicate as Duplicate
 import UniqueLogic.ST.Expression ((=:=))
 
 import qualified Control.Monad.Trans.Writer as MW
@@ -18,47 +20,21 @@
 
 
 
-data Assign = Assign Name Term
+data Assign = Assign Term.Name Term.T
    deriving (Show)
 
 type Assigns = [Assign]
 
-data Term =
-     Const Rational
-   | Var Name
-   | Max Term Term
-   | Add Term Term
-   | Sub Term Term
-   | Mul Term Term
-   | Div Term Term
-   | Abs Term
-   | Signum Term
-   deriving (Show)
-
-type Name = String
-
-
-instance Num Term where
-   fromInteger n = Const $ fromInteger n
-   (+) = Add
-   (-) = Sub
-   (*) = Mul
-   abs = Abs
-   signum = Signum
-
-instance Fractional Term where
-   fromRational x = Const x
-   (/) = Div
+type Variable s = Sys.Variable Assigns s (Duplicate.Ignore Term.T)
 
-globalVariable ::
-   Name -> ST s (Sys.Variable Assigns s Term)
+globalVariable :: Term.Name -> ST s (Variable s)
 globalVariable name =
    Sys.globalVariable $
-      \x -> writer (Var name, [Assign name x])
+      \(Duplicate.Ignore x) ->
+         writer (Duplicate.Ignore $ Term.Var name, [Assign name x])
 
-constant ::
-   Rational -> Sys.T Assigns s (Sys.Variable Assigns s Term)
-constant = Sys.constant . Const
+constant :: Rational -> Sys.T Assigns s (Variable s)
+constant = Sys.constant . fromRational
 
 
 {- |
@@ -70,7 +46,7 @@
 > y*z=6
 > z=3
 -}
-rule :: ((Maybe Term, Maybe Term, Maybe Term), Assigns)
+rule :: ((Maybe Term.T, Maybe Term.T, Maybe Term.T), Assigns)
 rule =
    runST (do
       x <- globalVariable "x"
@@ -85,11 +61,11 @@
             Rule.equ z c3
          MT.lift $ liftM3
             (,,)
-            (Sys.query x)
-            (Sys.query y)
-            (Sys.query z))
+            (Sys.queryIgnore x)
+            (Sys.queryIgnore y)
+            (Sys.queryIgnore z))
 
-expression :: ((Maybe Term, Maybe Term), Assigns)
+expression :: ((Maybe Term.T, Maybe Term.T), Assigns)
 expression =
    runST (do
       xv <- globalVariable "x"
@@ -101,5 +77,5 @@
             x*3 =:= y/2
             5 =:= 2+x
          MT.lift $ liftM2 (,)
-            (Sys.query xv)
-            (Sys.query yv))
+            (Sys.queryIgnore xv)
+            (Sys.queryIgnore yv))
diff --git a/src/UniqueLogic/ST/Example/Rule.hs b/src/UniqueLogic/ST/Example/Rule.hs
--- a/src/UniqueLogic/ST/Example/Rule.hs
+++ b/src/UniqueLogic/ST/Example/Rule.hs
@@ -3,7 +3,7 @@
  where
 
 import qualified UniqueLogic.ST.Rule as Rule
-import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.System.Simple as Sys
 
 import Control.Monad.ST (runST, )
 import Control.Monad (liftM4, )
diff --git a/src/UniqueLogic/ST/Example/Term.hs b/src/UniqueLogic/ST/Example/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Example/Term.hs
@@ -0,0 +1,32 @@
+{- |
+This module is intended for documentation purposes. Do not import it!
+-}
+module UniqueLogic.ST.Example.Term where
+
+
+data T =
+     Const Rational
+   | Var Name
+   | Max T T
+   | Add T T
+   | Sub T T
+   | Mul T T
+   | Div T T
+   | Abs T
+   | Signum T
+   deriving (Show)
+
+type Name = String
+
+
+instance Num T where
+   fromInteger n = Const $ fromInteger n
+   (+) = Add
+   (-) = Sub
+   (*) = Mul
+   abs = Abs
+   signum = Signum
+
+instance Fractional T where
+   fromRational x = Const x
+   (/) = Div
diff --git a/src/UniqueLogic/ST/Example/Verify.hs b/src/UniqueLogic/ST/Example/Verify.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Example/Verify.hs
@@ -0,0 +1,135 @@
+module UniqueLogic.ST.Example.Verify
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.Example.Term as Term
+import qualified UniqueLogic.ST.Expression as Expr
+import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.Duplicate as Duplicate
+import qualified UniqueLogic.ST.MonadTrans as UMT
+import UniqueLogic.ST.Expression ((=:=))
+
+import qualified Control.Monad.Exception.Synchronous as ME
+import qualified Control.Monad.Trans.Writer as MW
+import qualified Control.Monad.Trans.Class as MT
+import Control.Monad.Trans.Writer (writer, )
+import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT, )
+import Control.Monad.ST (ST, runST, )
+import Control.Monad (liftM, liftM2, ap, )
+import Control.Applicative (Applicative, pure, (<*>), )
+
+import qualified Prelude as P
+import Prelude hiding (max, log)
+
+
+
+data Assign = Assign Term.Name Term.T
+   deriving (Show)
+
+type Assigns = [Assign]
+
+data TrackedNumber a = TrackedNumber Term.T a
+   deriving (Show)
+
+tn1 :: (Term.T -> Term.T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b
+tn1 f g (TrackedNumber xt xn) = TrackedNumber (f xt) (g xn)
+
+tn2 :: (Term.T -> Term.T -> Term.T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c
+tn2 f g (TrackedNumber xt xn) (TrackedNumber yt yn) =
+   TrackedNumber (f xt yt) (g xn yn)
+
+instance Num a => Num (TrackedNumber a) where
+   fromInteger n = TrackedNumber (fromInteger n) (fromInteger n)
+   (+) = tn2 (+) (+)
+   (-) = tn2 (-) (-)
+   (*) = tn2 (*) (*)
+   abs = tn1 abs abs
+   signum = tn1 signum signum
+
+instance Fractional a => Fractional (TrackedNumber a) where
+   fromRational n = TrackedNumber (fromRational n) (fromRational n)
+   (/) = tn2 (/) (/)
+
+instance Eq a => Duplicate.C (TrackedNumber a) where
+   accept (TrackedNumber _ x) (TrackedNumber _ y)  =  x==y
+
+
+instance (Monad m) => Functor (Track m) where
+   fmap = liftM
+
+instance (Monad m) => Applicative (Track m) where
+   pure = return
+   (<*>) = ap
+
+instance (Monad m) => Monad (Track m) where
+   return = Track . UMT.point
+   x >>= k  =  Track $ UMT.bind (runTrack x) (runTrack . k)
+
+
+instance MT.MonadTrans Track where
+   lift = Track . MT.lift . MT.lift
+
+instance UMT.C Track where
+   point = return
+   bind = (>>=)
+
+instance Sys.C Track where
+   doUpdate =
+      Sys.updateAndCheck $ \_ _ ->
+         UMT.wrap $ Track $ ME.throwT AnonymousException
+
+
+newtype
+   Track m a =
+      Track {runTrack :: ME.ExceptionalT Exception (MW.WriterT Assigns m) a}
+
+data
+   Exception =
+        Exception Term.Name (TrackedNumber Rational) (TrackedNumber Rational)
+      | AnonymousException
+   deriving (Show)
+
+type Variable s = Sys.Variable Track s (TrackedNumber Rational)
+
+globalVariable :: Term.Name -> ST s (Variable s)
+globalVariable name =
+   Sys.globalVariable
+      (\al av -> Sys.updateAndCheck (inconsistency name) al av . update name)
+
+inconsistency ::
+   Monad m =>
+   Term.Name ->
+   TrackedNumber Rational ->
+   TrackedNumber Rational ->
+   UMT.Wrap Track m ()
+inconsistency name old new =
+   UMT.wrap $ Track $ ME.throwT $ Exception name old new
+
+update ::
+   Term.Name ->
+   MaybeT (ST s) (TrackedNumber a) ->
+   MaybeT (UMT.Wrap Track (ST s)) (TrackedNumber a)
+update name act = do
+   (TrackedNumber t x) <- mapMaybeT UMT.lift act
+   MT.lift $ UMT.wrap $ Track $ MT.lift $
+      writer (TrackedNumber (Term.Var name) x, [Assign name t])
+
+
+example ::
+   (ME.Exceptional Exception
+       (Maybe (TrackedNumber Rational),
+        Maybe (TrackedNumber Rational)),
+    Assigns)
+example =
+   runST (do
+      xv <- globalVariable "x"
+      yv <- globalVariable "y"
+      MW.runWriterT $ ME.runExceptionalT $ runTrack $ do
+         Sys.solve $ do
+            let x = Expr.fromVariable xv
+                y = Expr.fromVariable yv
+            x*3 =:= y/2
+            5 =:= 2+x
+         MT.lift $ liftM2 (,)
+            (Sys.query xv)
+            (Sys.query yv))
diff --git a/src/UniqueLogic/ST/Expression.hs b/src/UniqueLogic/ST/Expression.hs
--- a/src/UniqueLogic/ST/Expression.hs
+++ b/src/UniqueLogic/ST/Expression.hs
@@ -17,12 +17,11 @@
 
 import qualified UniqueLogic.ST.Rule as Rule
 import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.Duplicate as Duplicate
 
 import Control.Monad (ap, )
 import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )
 
-import Data.Monoid (Monoid, )
-
 -- import Control.Category ((.))
 -- import Data.Maybe (Maybe)
 
@@ -36,32 +35,32 @@
 and the variable at the top-level.
 The value of the expression equals the value of the top variable.
 -}
-newtype T var w s a = Cons (Sys.T w s (var w s a))
+newtype T w s a = Cons (Sys.T w s (Sys.Variable w s a))
 
 
 {- |
 Make a constant expression of a simple numeric value.
 -}
-constant :: (Sys.Var var, Monoid w) => a -> T var w s a
+constant :: (Sys.C w, Duplicate.C a) => a -> T w s a
 constant = Cons . Sys.constant
 
-fromVariable :: var w s a -> T var w s a
+fromVariable :: Sys.Variable w s a -> T w s a
 fromVariable = Cons . return
 
 
 fromRule1 ::
-   (Sys.Var var, Monoid w) =>
-   (var w s a -> Sys.T w s ()) ->
-   (T var w s a)
+   (Sys.C w, Duplicate.C a) =>
+   (Sys.Variable w s a -> Sys.T w s ()) ->
+   (T w s a)
 fromRule1 rule = Cons $ do
    xv <- Sys.localVariable
    rule xv
    return xv
 
 fromRule2, _fromRule2 ::
-   (Sys.Var var, Monoid w) =>
-   (var w s a -> var w s b -> Sys.T w s ()) ->
-   (T var w s a -> T var w s b)
+   (Sys.C w, Duplicate.C b) =>
+   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()) ->
+   (T w s a -> T w s b)
 fromRule2 rule (Cons x) = Cons $ do
    xv <- x
    yv <- Sys.localVariable
@@ -69,9 +68,9 @@
    return yv
 
 fromRule3, _fromRule3 ::
-   (Sys.Var var, Monoid w) =>
-   (var w s a -> var w s b -> var w s c -> Sys.T w s ()) ->
-   (T var w s a -> T var w s b -> T var w s c)
+   (Sys.C w, Duplicate.C c) =>
+   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()) ->
+   (T w s a -> T w s b -> T w s c)
 fromRule3 rule (Cons x) (Cons y) = Cons $ do
    xv <- x
    yv <- y
@@ -104,13 +103,13 @@
 than using auxiliary 'pair' rules!
 -}
 arg ::
-   T var w s a -> Apply w s (var w s a)
+   T w s a -> Apply w s (Sys.Variable w s a)
 arg (Cons x) = Apply x
 
 runApply ::
-   (Sys.Var var, Monoid w) =>
-   Apply w s (var w s a -> Sys.T w s ()) ->
-   T var w s a
+   (Sys.C w, Duplicate.C a) =>
+   Apply w s (Sys.Variable w s a -> Sys.T w s ()) ->
+   T w s a
 runApply (Apply rule) = Cons $ do
    f <- rule
    xv <- Sys.localVariable
@@ -124,7 +123,7 @@
 _fromRule3 rule x y = runApply $ liftA2 rule (arg x) (arg y)
 
 
-instance (P.Fractional a, Sys.Var var, Monoid w) => P.Num (T var w s a) where
+instance (Sys.C w, Duplicate.C a, P.Fractional a) => P.Num (T w s a) where
    fromInteger = constant . fromInteger
    (+) = fromRule3 Rule.add
    (-) = fromRule3 (\z x y -> Rule.add x y z)
@@ -132,20 +131,20 @@
    abs = fromRule2 (Sys.assignment2 abs)
    signum = fromRule2 (Sys.assignment2 signum)
 
-instance (P.Fractional a, Sys.Var var, Monoid w) => P.Fractional (T var w s a) where
+instance (Sys.C w, Duplicate.C a, P.Fractional a) => P.Fractional (T w s a) where
    fromRational = constant . fromRational
    (/) = fromRule3 (\z x y -> Rule.mul x y z)
 
-sqr :: (P.Floating a, Sys.Var var, Monoid w) => T var w s a -> T var w s a
+sqr :: (Sys.C w, Duplicate.C a, P.Floating a) => T w s a -> T w s a
 sqr = fromRule2 Rule.square
 
-sqrt :: (P.Floating a, Sys.Var var, Monoid w) => T var w s a -> T var w s a
+sqrt :: (Sys.C w, Duplicate.C a, P.Floating a) => T w s a -> T w s a
 sqrt = fromRule2 (flip Rule.square)
 
 
 infixl 4 =!=
 
-(=!=) :: (Sys.Var var, Monoid w) => T var w s a -> T var w s a -> T var w s a
+(=!=) :: (Sys.C w) => T w s a -> T w s a -> T w s a
 (=!=) (Cons x) (Cons y) = Cons $ do
    xv <- x
    yv <- y
@@ -154,7 +153,7 @@
 
 infix 0 =:=
 
-(=:=) :: (Sys.Var var, Monoid w) => T var w s a -> T var w s a -> Sys.T w s ()
+(=:=) :: (Sys.C w) => T w s a -> T w s a -> Sys.T w s ()
 (=:=) (Cons x) (Cons y) = do
    xv <- x
    yv <- y
@@ -166,15 +165,17 @@
 including Eq superclass and comparisons,
 but we need to compute maxima.
 -}
-max :: (Ord a, Sys.Var var, Monoid w) => T var w s a -> T var w s a -> T var w s a
+max :: (Sys.C w, Ord a, Duplicate.C a) => T w s a -> T w s a -> T w s a
 max = fromRule3 Rule.max
 
-maximum :: (Ord a, Sys.Var var, Monoid w) => [T var w s a] -> T var w s a
+maximum :: (Sys.C w, Ord a, Duplicate.C a) => [T w s a] -> T w s a
 maximum = foldl1 max
 
 
 {- |
 Construct or decompose a pair.
 -}
-pair :: (Sys.Var var, Monoid w) => T var w s a -> T var w s b -> T var w s (a,b)
+pair ::
+   (Sys.C w, Duplicate.C a, Duplicate.C b) =>
+   T w s a -> T w s b -> T w s (a,b)
 pair = fromRule3 Rule.pair
diff --git a/src/UniqueLogic/ST/MonadTrans.hs b/src/UniqueLogic/ST/MonadTrans.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/MonadTrans.hs
@@ -0,0 +1,68 @@
+{-
+This module could also be part of 'transformers'.
+-}
+module UniqueLogic.ST.MonadTrans where
+
+import qualified Control.Monad.Exception.Synchronous as E
+
+import qualified Control.Monad.Trans.Class as MT
+import qualified Control.Monad.Trans.Writer as MW
+import qualified Control.Monad.Trans.Maybe as MM
+import qualified Control.Monad.Trans.Identity as MI
+
+import Control.Applicative (Applicative, pure, (<*>), Const(Const))
+import Control.Monad (liftM, ap, )
+import Data.Monoid (Monoid, )
+
+
+{- |
+Provide the methods that make a transformed monad a monad.
+-}
+class MT.MonadTrans t => C t where
+   point :: Monad m => a -> t m a
+   bind :: Monad m => t m a -> (a -> t m b) -> t m b
+
+instance C MI.IdentityT where
+   point = return
+   bind = (>>=)
+
+instance (Monoid w) => C (MW.WriterT w) where
+   point = return
+   bind = (>>=)
+
+instance C (E.ExceptionalT e) where
+   point = return
+   bind = (>>=)
+
+instance C MM.MaybeT where
+   point = return
+   bind = (>>=)
+
+
+{- |
+Build a regular monad for generic monad transformer and monad.
+The 'Const' type allows us to force the kind (m :: * -> *)
+without using ExplicitKindSignatures.
+-}
+newtype Wrap t m a = Wrap (Const (t m a) (m a))
+
+wrap :: t m a -> Wrap t m a
+wrap = Wrap . Const
+
+unwrap :: Wrap t m a -> t m a
+unwrap (Wrap (Const m)) = m
+
+lift :: (C t, Monad m) => m a -> Wrap t m a
+lift = wrap . MT.lift
+
+
+instance (C t, Monad m) => Functor (Wrap t m) where
+   fmap = liftM
+
+instance (C t, Monad m) => Applicative (Wrap t m) where
+   pure = return
+   (<*>) = ap
+
+instance (C t, Monad m) => Monad (Wrap t m) where
+   return = wrap . point
+   x >>= k  =  wrap $ bind (unwrap x) (unwrap . k)
diff --git a/src/UniqueLogic/ST/Rule.hs b/src/UniqueLogic/ST/Rule.hs
--- a/src/UniqueLogic/ST/Rule.hs
+++ b/src/UniqueLogic/ST/Rule.hs
@@ -7,17 +7,16 @@
    ) where
 
 import qualified UniqueLogic.ST.System as Sys
-
-import Data.Monoid (Monoid, )
+import qualified UniqueLogic.ST.MonadTrans as UMT
 
 import qualified Prelude as P
 import Prelude hiding (max)
 
 
 generic2 ::
-   (Sys.Var var, Monoid w) =>
+   (UMT.C w) =>
    (b -> a) -> (a -> b) ->
-   var w s a -> var w s b -> Sys.T w s ()
+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()
 generic2 f g x y =
    sequence_ $
    Sys.assignment2 f y x :
@@ -25,9 +24,9 @@
    []
 
 generic3 ::
-   (Sys.Var var, Monoid w) =>
+   (UMT.C w) =>
    (b -> c -> a) -> (c -> a -> b) -> (a -> b -> c) ->
-   var w s a -> var w s b -> var w s c -> Sys.T w s ()
+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()
 generic3 f g h x y z =
    sequence_ $
    Sys.assignment3 f y z x :
@@ -37,13 +36,13 @@
 
 
 equ ::
-   (Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> Sys.T w s ()
+   (UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 equ = generic2 id id
 
 max ::
-   (Ord a, Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+   (Ord a, UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 max =
    Sys.assignment3 P.max
 
@@ -57,25 +56,25 @@
 This is the way, 'generic2' and 'generic3' work.
 -}
 pair ::
-   (Sys.Var var, Monoid w) =>
-   var w s a -> var w s b -> var w s (a,b) -> Sys.T w s ()
+   (UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s (a,b) -> Sys.T w s ()
 pair x y xy =
    Sys.assignment3 (,) x y xy >>
    Sys.assignment2 fst xy x >>
    Sys.assignment2 snd xy y
 
-add :: (Num a, Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+add :: (Num a, UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 add = generic3 subtract (-) (+)
 
-mul :: (Fractional a, Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+mul :: (Fractional a, UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 mul = generic3 (flip (/)) (/) (*)
 
-square :: (Floating a, Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> Sys.T w s ()
+square :: (Floating a, UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 square = generic2 sqrt (^(2::Int))
 
-pow :: (Floating a, Sys.Var var, Monoid w) =>
-   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+pow :: (Floating a, UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
 pow = generic3 (\x y -> y ** recip x) (flip logBase) (**)
diff --git a/src/UniqueLogic/ST/RuleLog.hs b/src/UniqueLogic/ST/RuleLog.hs
deleted file mode 100644
--- a/src/UniqueLogic/ST/RuleLog.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-module UniqueLogic.ST.RuleLog (
-   -- * Custom rules
-   generic2,
-   generic3,
-   ) where
-
-import qualified UniqueLogic.ST.SystemLog as Sys
-
-import Control.Monad.Trans.Writer (Writer, )
-import Data.Monoid (Monoid, )
-
-import qualified Prelude as P
-import Prelude hiding (max)
-
-
-generic2 ::
-   Monoid w =>
-   (b -> Writer w a) -> (a -> Writer w b) ->
-   Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()
-generic2 f g x y =
-   sequence_ $
-   Sys.assignment2 f y x :
-   Sys.assignment2 g x y :
-   []
-
-generic3 ::
-   Monoid w =>
-   (b -> c -> Writer w a) -> (c -> a -> Writer w b) -> (a -> b -> Writer w c) ->
-   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()
-generic3 f g h x y z =
-   sequence_ $
-   Sys.assignment3 f y z x :
-   Sys.assignment3 g z x y :
-   Sys.assignment3 h x y z :
-   []
diff --git a/src/UniqueLogic/ST/System.hs b/src/UniqueLogic/ST/System.hs
--- a/src/UniqueLogic/ST/System.hs
+++ b/src/UniqueLogic/ST/System.hs
@@ -1,69 +1,242 @@
 module UniqueLogic.ST.System (
    -- * Preparation
-   Var,
    Variable,
-   Sys.globalVariable,
-   plainVariable,
+   globalVariable,
+   -- * Handle duplicates
+   C, doUpdate,
+   simpleUpdate, -- should be private in future
+   updateIfNew, -- should be private or with special type
+   updateAndCheck,
+   Fragile(break),
    -- * Posing statements
    T,
    localVariable,
    constant,
    assignment2,
    assignment3,
-   Sys.Apply, arg, runApply,
+   Apply, arg, runApply,
    -- * Solution
    solve,
    query,
+   queryForbid,
+   queryIgnore,
+   queryVerify,
    ) where
 
-import qualified UniqueLogic.ST.SystemLog as Sys
-import UniqueLogic.ST.SystemLog (T, Variable)
-
+import qualified Control.Monad.Exception.Synchronous as E
 import qualified Control.Monad.Trans.Writer as MW
-import Control.Applicative (liftA, liftA2, )
+import qualified Control.Monad.Trans.Class  as MT
+import qualified UniqueLogic.ST.MonadTrans as UMT
+import qualified UniqueLogic.ST.Duplicate as Duplicate
+import qualified Data.Foldable as Fold
+import Control.Monad.Trans.Writer (WriterT, )
+import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, mapMaybeT, )
+import Control.Monad.Trans.Identity (IdentityT, )
 import Control.Monad.ST (ST, )
+import Control.Monad.HT (void, (<=<), )
+import Control.Monad (when, liftM2, ap, )
+import Control.Applicative (Applicative, pure, (<*>), )
+import Data.Functor.Compose (Compose(Compose))
 
+import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )
+import Data.Maybe (isNothing, )
 import Data.Monoid (Monoid, )
 
+import Prelude hiding (break)
 
-class Var var where
-   plainVariable :: var w s a -> Variable w s a
-   runApply ::
-      Monoid w =>
-      Sys.Apply w s a -> var w s a -> T w s ()
-   constant :: (Monoid w) => a -> T w s (var w s a)
-   localVariable :: (Monoid w) => T w s (var w s a)
 
-instance Var Variable where
-   plainVariable = id
-   runApply f = Sys.runApply (fmap return f)
-   constant = Sys.constant
-   localVariable = Sys.localVariable
+data Variable w s a =
+   Variable {
+      varUpdate :: MaybeT (ST s) a -> Update w s,
+      dependsRef :: STRef s [Update w s],
+      valueRef :: STRef s (Maybe a)
+   }
 
-arg :: (Var var, Monoid w) => var w s a -> Sys.Apply w s a
-arg = Sys.arg . plainVariable
+type Update w s = UMT.Wrap w (ST s) ()
 
+type Updater w s a =
+        STRef s [Update w s] -> STRef s (Maybe a) ->
+        MaybeT (UMT.Wrap w (ST s)) a -> Update w s
 
+type SimpleUpdater w s a =
+        STRef s [Update w s] -> STRef s (Maybe a) ->
+        MaybeT (ST s) a -> Update w s
+
+newtype T w s a =
+   Cons {run :: WriterT [STRef s [Update w s]] (ST s) a}
+
+instance Functor (T w s) where
+   fmap f (Cons x) = Cons (fmap f x)
+
+instance Applicative (T w s) where
+   pure = Cons . return
+   (<*>) = ap
+
+instance Monad (T w s) where
+   return = Cons . return
+   Cons x >>= k  = Cons $ run . k =<< x
+
+
+lift :: ST s a -> T w s a
+lift = Cons . MT.lift
+
+globalVariable ::
+   (UMT.C w, Duplicate.C a) =>
+   SimpleUpdater w s a -> ST s (Variable w s a)
+globalVariable update = object update Nothing
+
+localVariable :: (C w, Duplicate.C a) => T w s (Variable w s a)
+localVariable = lift $ globalVariable simpleUpdate
+
+constant ::
+   (C w, Duplicate.C a) =>
+   a -> T w s (Variable w s a)
+constant a =
+   do v <- lift $ object simpleUpdate $ Just a
+      Cons $ MW.tell [dependsRef v]
+      return v
+
+object ::
+   (STRef s [Update w s] -> STRef s (Maybe a) ->
+    MaybeT (ST s) a -> Update w s) ->
+   Maybe a -> ST s (Variable w s a)
+object updater ma = do
+   al <- newSTRef []
+   av <- newSTRef ma
+   return $ Variable (updater al av) al av
+
+resolve ::
+   UMT.C w =>
+   STRef s [Update w s] -> Update w s
+resolve =
+   sequence_ <=< UMT.lift . readSTRef
+
+solve ::
+   UMT.C w =>
+   T w s a -> w (ST s) a
+solve (Cons m) = UMT.unwrap $ do
+   (a,w) <- UMT.lift $ MW.runWriterT m
+   mapM_ resolve w
+   return a
+
+query :: Variable w s a -> ST s (Maybe a)
+query = readSTRef . valueRef
+
+queryForbid :: Variable w s (Duplicate.Forbid a) -> ST s (Maybe a)
+queryForbid = fmap (fmap (\(Duplicate.Forbid a) -> a)) . query
+
+queryIgnore :: Variable w s (Duplicate.Ignore a) -> ST s (Maybe a)
+queryIgnore = fmap (fmap (\(Duplicate.Ignore a) -> a)) . query
+
+queryVerify :: Variable w s (Duplicate.Verify a) -> ST s (Maybe a)
+queryVerify = fmap (fmap (\(Duplicate.Verify a) -> a)) . query
+
+
+updateIfNew :: (C w, Duplicate.C a) => Updater w s a
+updateIfNew al av act = do
+   as <- UMT.lift $ readSTRef av
+   when (isNothing as) $ void $ runMaybeT $ do
+      MT.lift . UMT.lift . writeSTRef av . Just =<< act
+      MT.lift $ resolve al
+
+
+class Inconsistency e where
+   inconsistency :: e
+
+instance
+   Inconsistency e =>
+      Fragile (E.ExceptionalT e) where
+   break =
+      UMT.wrap $ E.throwT inconsistency
+
+class C t => Fragile t where
+   break :: Monad m => UMT.Wrap t m a
+
+updateAndCheck ::
+   (UMT.C w, Duplicate.C a) =>
+   (a -> a -> UMT.Wrap w (ST s) ()) ->
+   Updater w s a
+updateAndCheck customBreak al av act = do
+   maold <- UMT.lift $ readSTRef av
+   manew <- runMaybeT act
+   Fold.forM_ manew $ \anew -> do
+      UMT.lift . writeSTRef av . Just $ anew
+      case maold of
+         Just aold ->
+            when (not $ Duplicate.accept aold anew) $
+               customBreak aold anew
+         Nothing -> resolve al
+
+
+class UMT.C w => C w where
+   doUpdate :: (Duplicate.C a) => Updater w s a
+
+instance C IdentityT where
+   doUpdate = updateIfNew
+
+instance (Monoid w) => C (MW.WriterT w) where
+   doUpdate = updateIfNew
+
+instance (Inconsistency e) => C (E.ExceptionalT e) where
+   doUpdate = updateAndCheck $ \_ _ -> break
+
+simpleUpdate :: (C w, Duplicate.C a) => SimpleUpdater w s a
+simpleUpdate al av = doUpdate al av . mapMaybeT UMT.lift
+
+
+readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a
+readSTRefM = MaybeT . readSTRef
+
+
 assignment2 ::
-   (Var var, Monoid w) =>
+   UMT.C w =>
    (a -> b) ->
-   var w s a -> var w s b ->
+   Variable w s a -> Variable w s b ->
    T w s ()
-assignment2 f a =
-   runApply $ liftA f (arg a)
+assignment2 f (Variable _ al av) b =
+   let update =
+          varUpdate b $ fmap f $ readSTRefM av
+   in  lift $
+       modifySTRef al (update :)
 
 assignment3 ::
-   (Var var, Monoid w) =>
+   UMT.C w =>
    (a -> b -> c) ->
-   var w s a -> var w s b -> var w s c ->
+   Variable w s a -> Variable w s b -> Variable w s c ->
    T w s ()
-assignment3 f a b =
-   runApply $ liftA2 f (arg a) (arg b)
+assignment3 f (Variable _ al av) (Variable _ bl bv) c =
+   let update =
+          varUpdate c $
+          liftM2 f (readSTRefM av) (readSTRefM bv)
+   in  lift $
+       modifySTRef al (update :) >>
+       modifySTRef bl (update :)
 
 
-solve :: T () s a -> ST s a
-solve = fmap fst . MW.runWriterT . Sys.solve
+newtype Apply w s a =
+   Apply (Compose (MW.Writer [STRef s [Update w s]]) (MaybeT (ST s)) a)
 
 
-query :: (Var var, Monoid w) => var w s a -> ST s (Maybe a)
-query = Sys.query . plainVariable
+{- |
+This function allows to generalize 'assignment2' and 'assignment3' to more arguments.
+You could achieve the same with nested applications of @assignment3 (,)@.
+-}
+arg :: Variable w s a -> Apply w s a
+arg (Variable _update al av) =
+   Apply $ Compose $ MW.writer (MaybeT $ readSTRef av, [al])
+
+instance Functor (Apply w s) where
+   fmap f (Apply a) = Apply $ fmap f a
+
+instance Applicative (Apply w s) where
+   pure a = Apply $ pure a
+   Apply f <*> Apply a = Apply $ f <*> a
+
+
+runApply ::
+   UMT.C w =>
+   Apply w s a -> Variable w s a -> T w s ()
+runApply (Apply (Compose w)) a =
+   case MW.runWriter w of
+      (f, refs) ->
+         lift $ Fold.forM_ refs $ flip modifySTRef (varUpdate a f :)
diff --git a/src/UniqueLogic/ST/System/Label.hs b/src/UniqueLogic/ST/System/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/System/Label.hs
@@ -0,0 +1,51 @@
+module UniqueLogic.ST.System.Label (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Posing statements
+   T,
+   Sys.localVariable,
+   Sys.constant,
+   Sys.assignment2,
+   Sys.assignment3,
+   Sys.Apply, Sys.arg, Sys.runApply,
+   -- * Solution
+   Sys.solve,
+   Sys.query,
+   Sys.queryForbid,
+   Sys.queryIgnore,
+   Sys.queryVerify,
+   ) where
+
+import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.MonadTrans as UMT
+import qualified UniqueLogic.ST.Duplicate as Duplicate
+
+import qualified Control.Monad.Trans.Writer as MW
+import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT, )
+import Control.Monad.ST (ST, )
+
+import Data.Monoid (Monoid, )
+import Data.Traversable (traverse, )
+
+import Prelude hiding (log, )
+
+
+type T w = Sys.T (MW.WriterT w)
+type Variable w = Sys.Variable (MW.WriterT w)
+
+globalVariable ::
+   (Monoid w, Duplicate.C a) =>
+   (a -> MW.Writer w a) -> ST s (Variable w s a)
+globalVariable log =
+   Sys.globalVariable
+      (\al av -> Sys.updateIfNew al av . wrap log)
+
+wrap ::
+   (Monoid w) =>
+   (a -> MW.Writer w b) ->
+   MaybeT (ST s) a -> MaybeT (UMT.Wrap (MW.WriterT w) (ST s)) b
+wrap log =
+   mapMaybeT $
+      UMT.wrap . MW.WriterT . fmap (MW.runWriter . traverse log)
+--      UMT.wrap . MW.writer . MW.runWriter . traverse log <=< UMT.lift
diff --git a/src/UniqueLogic/ST/System/Simple.hs b/src/UniqueLogic/ST/System/Simple.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/System/Simple.hs
@@ -0,0 +1,43 @@
+module UniqueLogic.ST.System.Simple (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Posing statements
+   T,
+   localVariable,
+   constant,
+   Sys.assignment2,
+   Sys.assignment3,
+   Sys.Apply, Sys.arg, Sys.runApply,
+   -- * Solution
+   solve,
+   query,
+   ) where
+
+import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.Duplicate as Duplicate
+
+import Control.Monad.Trans.Identity (IdentityT, runIdentityT, )
+import Control.Monad.ST (ST, )
+
+
+type T = Sys.T IdentityT
+
+type Variable s a = Sys.Variable IdentityT s (Duplicate.Ignore a)
+
+
+globalVariable :: ST s (Variable s a)
+globalVariable =
+   Sys.globalVariable Sys.simpleUpdate
+
+localVariable :: T s (Variable s a)
+localVariable = Sys.localVariable
+
+constant :: a -> T s (Variable s a)
+constant = Sys.constant . Duplicate.Ignore
+
+solve :: T s a -> ST s a
+solve = runIdentityT . Sys.solve
+
+query :: Variable s a -> ST s (Maybe a)
+query = fmap (fmap (\(Duplicate.Ignore a) -> a)) . Sys.query
diff --git a/src/UniqueLogic/ST/SystemLabel.hs b/src/UniqueLogic/ST/SystemLabel.hs
deleted file mode 100644
--- a/src/UniqueLogic/ST/SystemLabel.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-module UniqueLogic.ST.SystemLabel (
-   -- * Preparation
-   Variable,
-   globalVariable,
-   -- * Posing statements
-   Sys.T,
-   Sys.localVariable,
-   Sys.constant,
-   Sys.assignment2,
-   Sys.assignment3,
-   Sys.Apply, Sys.arg, Sys.runApply,
-   -- * Solution
-   solve,
-   Sys.query,
-   ) where
-
-import qualified UniqueLogic.ST.System as Sys
-import qualified UniqueLogic.ST.SystemLog as SysLog
-
-import qualified Control.Monad.Trans.Writer as MW
-import Control.Monad.Trans.Writer (Writer, )
-import Control.Monad.ST (ST, )
-
-import Data.Monoid (Monoid, )
-
-import Prelude hiding (log, )
-
-
-data Variable w s a =
-   Variable
-      (a -> Writer w a)
-      (SysLog.Variable w s a)
-
-instance Sys.Var Variable where
-   plainVariable (Variable _ v) = v
-   runApply f (Variable log v) = SysLog.runApply (fmap log f) v
-   constant = fmap (Variable return) . SysLog.constant
-   localVariable = fmap (Variable return) SysLog.localVariable
-
-
-globalVariable :: (a -> MW.Writer w a) -> ST s (Variable w s a)
-globalVariable log = fmap (Variable log) Sys.globalVariable
-
-
-solve :: (Monoid w) => Sys.T w s a -> MW.WriterT w (ST s) a
-solve = SysLog.solve
diff --git a/src/UniqueLogic/ST/SystemLog.hs b/src/UniqueLogic/ST/SystemLog.hs
deleted file mode 100644
--- a/src/UniqueLogic/ST/SystemLog.hs
+++ /dev/null
@@ -1,167 +0,0 @@
-module UniqueLogic.ST.SystemLog (
-   -- * Preparation
-   Variable,
-   globalVariable,
-   -- * Posing statements
-   T,
-   localVariable,
-   constant,
-   assignment2,
-   assignment3,
-   Apply, arg, runApply,
-   -- * Solution
-   solve,
-   query,
-   ) where
-
-import qualified Control.Monad.Trans.Writer as MW
-import qualified Control.Monad.Trans.Class  as MT
-import qualified Data.Foldable as Fold
-import Control.Monad.Trans.Writer (WriterT, Writer, )
-import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, mapMaybeT, )
-import Control.Monad.ST (ST, )
-import Control.Monad.HT ((<=<), )
-import Control.Monad (when, liftM2, ap, void, )
-import Control.Applicative (Applicative, pure, (<*>), )
-import Data.Functor.Compose (Compose(Compose))
-
-import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )
-import Data.Monoid (Monoid, )
-import Data.Maybe (isNothing, )
-
-
-data Variable w s a =
-   Variable {
-      dependsRef :: STRef s [Update w s],
-      valueRef :: STRef s (Maybe a)
-   }
-
-type Update w s = WriterT w (ST s) ()
-
-newtype T w s a =
-   Cons {run :: WriterT [STRef s [Update w s]] (ST s) a}
-
-instance Functor (T w s) where
-   fmap f (Cons x) = Cons (fmap f x)
-
-instance Applicative (T w s) where
-   pure = Cons . return
-   (<*>) = ap
-
-instance Monad (T w s) where
-   return = Cons . return
-   Cons x >>= k  = Cons $ run . k =<< x
-
-
-lift :: ST s a -> T w s a
-lift = Cons . MT.lift
-
-localVariable :: T w s (Variable w s a)
-localVariable = lift globalVariable
-
-globalVariable :: ST s (Variable w s a)
-globalVariable = object Nothing
-
-constant :: a -> T w s (Variable w s a)
-constant a =
-   do v <- lift $ object $ Just a
-      Cons $ MW.tell [dependsRef v]
-      return v
-
-object :: Maybe a -> ST s (Variable w s a)
-object ma =
-   liftM2 Variable (newSTRef []) (newSTRef ma)
-
-resolve ::
-   Monoid w =>
-   STRef s [Update w s] -> Update w s
-resolve =
-   sequence_ <=< MT.lift . readSTRef
-
-solve ::
-   Monoid w =>
-   T w s a -> WriterT w (ST s) a
-solve (Cons m) = do
-   (a,w) <- MT.lift $ MW.runWriterT m
-   mapM_ resolve w
-   return a
-
-query :: Variable w s a -> ST s (Maybe a)
-query = readSTRef . valueRef
-
-
-mw ::
-   (Monoid w, Monad st) =>
-   MaybeT st (Writer w a) -> MaybeT (WriterT w st) a
---   st (Maybe (Writer w a)) -> WriterT w st (Maybe a)
-mw act = do
-   mwa <- mapMaybeT MT.lift act
-   case MW.runWriter mwa of
-      (a,w) -> MT.lift $ MW.tell w >> return a
-
-updateIfNew ::
-   Monoid w =>
-   Variable w s a -> MaybeT (ST s) (Writer w a) -> Update w s
-updateIfNew (Variable al av) act = do
-   as <- MT.lift $ readSTRef av
-   when (isNothing as) $ void $ runMaybeT $ do
-      MT.lift . MT.lift . writeSTRef av . Just =<< mw act
-      MT.lift $ resolve al
-
-readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a
-readSTRefM = MaybeT . readSTRef
-
-
-assignment2 ::
-   Monoid w =>
-   (a -> Writer w b) ->
-   Variable w s a -> Variable w s b ->
-   T w s ()
-assignment2 f (Variable al av) b =
-   let update =
-          updateIfNew b $ fmap f $ readSTRefM av
-   in  lift $
-       modifySTRef al (update :)
-
-assignment3 ::
-   Monoid w =>
-   (a -> b -> Writer w c) ->
-   Variable w s a -> Variable w s b -> Variable w s c ->
-   T w s ()
-assignment3 f (Variable al av) (Variable bl bv) c =
-   let update =
-          updateIfNew c $
-          liftM2 f (readSTRefM av) (readSTRefM bv)
-   in  lift $
-       modifySTRef al (update :) >>
-       modifySTRef bl (update :)
-
-
-data Apply w s a =
-   Apply (Compose (MW.Writer [STRef s [Update w s]]) (MaybeT (ST s)) a)
-
-
-{- |
-This function allows to generalize 'assignment2' and 'assignment3' to more arguments.
-You could achieve the same with nested applications of @assignment3 (,)@.
--}
-arg :: Monoid w => Variable w s a -> Apply w s a
-arg (Variable al av) =
-   Apply $ Compose $ MW.writer (readSTRefM av, [al])
-
-
-instance Monoid w => Functor (Apply w s) where
-   fmap f (Apply a) = Apply $ fmap f a
-
-instance Monoid w => Applicative (Apply w s) where
-   pure a = Apply $ pure a
-   Apply f <*> Apply a = Apply $ f <*> a
-
-
-runApply ::
-   Monoid w =>
-   Apply w s (Writer w a) -> Variable w s a -> T w s ()
-runApply (Apply (Compose w)) a =
-   case MW.runWriter w of
-      (f, refs) ->
-         lift $ Fold.forM_ refs $ flip modifySTRef (updateIfNew a f :)
diff --git a/src/UniqueLogic/ST/Test.hs b/src/UniqueLogic/ST/Test.hs
--- a/src/UniqueLogic/ST/Test.hs
+++ b/src/UniqueLogic/ST/Test.hs
@@ -1,14 +1,17 @@
 module Main where
 
 import qualified UniqueLogic.ST.Expression as Expr
-import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.System.Simple as Sys
+import qualified UniqueLogic.ST.Duplicate as Duplicate
 import UniqueLogic.ST.Expression ((=:=))
 
 import qualified Control.Monad.Trans.Class as MT
 import qualified Control.Monad.Trans.Writer as MW
+import Control.Monad.Trans.Identity (IdentityT, )
 import Control.Monad.ST (ST, runST, )
 import Control.Monad (join, liftM2, )
 import Data.Monoid (Monoid(mempty, mappend))
+import Data.Semigroup (Semigroup((<>)), )
 
 import Data.List (sortBy, )
 import Data.Ord.HT (comparing, )
@@ -24,9 +27,12 @@
 
 newtype Check s = Check {runCheck :: ST s Bool}
 
+instance Semigroup (Check s) where
+   Check x <> Check y = Check $ liftM2 (&&) x y
+
 instance Monoid (Check s) where
    mempty = Check $ return True
-   mappend (Check x) (Check y) = Check $ liftM2 (&&) x y
+   mappend = (<>)
 
 {-
 Take a system of six equations and seven variables
@@ -40,10 +46,9 @@
    runST
       (join . fmap runCheck . Sys.solve $ MW.execWriterT $ do
          let variable ::
-                (Monoid w) =>
                 Int -> Rational ->
-                MW.WriterT (Check s) (Sys.T w s)
-                   (Expr.T Sys.Variable w s Rational)
+                MW.WriterT (Check s) (Sys.T s)
+                   (Expr.T IdentityT s (Duplicate.Ignore Rational))
              variable n x = do
                 v <-
                    MT.lift $
diff --git a/unique-logic.cabal b/unique-logic.cabal
--- a/unique-logic.cabal
+++ b/unique-logic.cabal
@@ -1,10 +1,10 @@
 Name:             unique-logic
-Version:          0.3
+Version:          0.4
 License:          BSD3
 License-File:     LICENSE
 Author:           Henning Thielemann
 Maintainer:       Henning Thielemann <haskell@henning-thielemann.de>
-Homepage:         http://code.haskell.org/~thielema/unique-logic/
+Homepage:         http://hub.darcs.net/thielema/unique-logic/
 Category:         Logic programming
 Synopsis:         Solve simple simultaneous equations
 Description:
@@ -16,8 +16,10 @@
   Only one solution is computed.
   Simultaneous equations with multiple solutions are not allowed.
   However, variables may remain undefined.
-  We do not even check for consistency,
-  since with floating point numbers even simple rules may not be consistent.
+  The solver may optionally check for consistency.
+  It does not do so by default
+  since with floating point numbers or symbolic expressions
+  even simple rules may not be consistent.
   .
   The modules ordered with respect to abstraction level are:
   .
@@ -38,8 +40,12 @@
     Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.
     For an executable example see "UniqueLogic.ST.Example.Expression".
   .
-  * "UniqueLogic.ST.SystemLabel":
-    Provides a new type for named variables.
+  * "UniqueLogic.ST.System.Simple":
+    Provides specialised functions from "UniqueLogic.ST.System"
+    for the case of a system without labels and consistency checks.
+  .
+  * "UniqueLogic.ST.System.Label":
+    Provides a custom constructor for variables.
     When creating a variable you decide whether and how
     an assignment to this variable shall be logged.
     There is an example that shows how to solve a logic system
@@ -47,52 +53,58 @@
     The naming and logging allows us to observe shared intermediate results.
     For an executable example see "UniqueLogic.ST.Example.Label".
   .
-  * "UniqueLogic.ST.SystemLog", "UniqueLogic.ST.RuleLog":
-    These modules allow to log an assignment
-    depending on the arguments to an assignment.
-    This is more general than "UniqueLogic.ST.SystemLabel"
-    which allows only dependencies on the result of an assignment.
+  * By using more sophisticated monad transformers,
+    we can check the equations for consistency,
+    report inconsistencies and how they arised.
+    We demonstrate that in "UniqueLogic.ST.Example.Verify".
+  .
+  The package is purely Haskell 98.
 Tested-With:       GHC==7.4.2
 Cabal-Version:     >=1.8
 Build-Type:        Simple
 
 Source-Repository this
-  Tag:         0.3
+  Tag:         0.4
   Type:        darcs
-  Location:    http://code.haskell.org/~thielema/unique-logic/
+  Location:    http://hub.darcs.net/thielema/unique-logic/
 
 Source-Repository head
   Type:        darcs
-  Location:    http://code.haskell.org/~thielema/unique-logic/
+  Location:    http://hub.darcs.net/thielema/unique-logic/
 
 Library
   Build-Depends:
-    transformers >=0.2 && <0.4,
-    utility-ht >=0.0.1 && <0.1,
+    explicit-exception >=0.1.7 && <0.2,
+    transformers >=0.2 && <0.6,
+    utility-ht >=0.0.9 && <0.1,
     base >= 4 && <5
   GHC-Options:      -Wall
   Hs-Source-Dirs:   src
 
   Exposed-Modules:
+    UniqueLogic.ST.MonadTrans
+    UniqueLogic.ST.Duplicate
     UniqueLogic.ST.System
-    UniqueLogic.ST.SystemLog
-    UniqueLogic.ST.SystemLabel
+    UniqueLogic.ST.System.Simple
+    UniqueLogic.ST.System.Label
     UniqueLogic.ST.Rule
-    UniqueLogic.ST.RuleLog
     UniqueLogic.ST.Expression
     -- example modules
     UniqueLogic.ST.Example.Rule
     UniqueLogic.ST.Example.Label
     UniqueLogic.ST.Example.Expression
+    UniqueLogic.ST.Example.Verify
+    UniqueLogic.ST.Example.Term
 
 Test-Suite test-unique-logic
   Type:    exitcode-stdio-1.0
   Main-Is: src/UniqueLogic/ST/Test.hs
   GHC-Options: -Wall
   Build-Depends:
-    QuickCheck >=2.4 && <2.6,
+    QuickCheck >=2.4 && <3,
     unique-logic,
-    non-empty >=0.0 && <0.1,
+    non-empty >=0.0 && <0.4,
+    semigroups >=0.1 && <1.0,
     transformers,
     utility-ht,
     base