diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2013, Henning Thielemann
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * The names of contributors may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#! /usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/src/UniqueLogic/ST/TF/Example/Expression.hs b/src/UniqueLogic/ST/TF/Example/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Example/Expression.hs
@@ -0,0 +1,26 @@
+module UniqueLogic.ST.TF.Example.Expression
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.TF.Expression as Expr
+import qualified UniqueLogic.ST.TF.System.Simple as Sys
+import UniqueLogic.ST.TF.Expression ((=:=))
+
+import Control.Monad.ST (runST, )
+import Control.Monad (liftM2, )
+
+
+example :: (Maybe Double, Maybe Double)
+example =
+   runST (do
+      xv <- Sys.globalVariable
+      yv <- Sys.globalVariable
+      Sys.solve $ do
+         let x = Expr.fromVariable xv
+             y = Expr.fromVariable yv
+         x*3 =:= y/2
+         5 =:= 2+x
+      liftM2
+         (,)
+         (Sys.query xv)
+         (Sys.query yv))
diff --git a/src/UniqueLogic/ST/TF/Example/Label.hs b/src/UniqueLogic/ST/TF/Example/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Example/Label.hs
@@ -0,0 +1,79 @@
+module UniqueLogic.ST.TF.Example.Label
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.TF.Example.Term as Term
+import qualified UniqueLogic.ST.TF.Expression as Expr
+import qualified UniqueLogic.ST.TF.Rule as Rule
+import qualified UniqueLogic.ST.TF.System.Label as Sys
+import UniqueLogic.ST.TF.Expression ((=:=))
+
+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.ST (ST, runST, )
+import Control.Monad (liftM2, liftM3, )
+
+import qualified Prelude as P
+import Prelude hiding (max, log)
+
+
+
+data Assign = Assign Term.Name Term.T
+   deriving (Show)
+
+type Assigns = [Assign]
+
+type Variable s = Sys.Variable Assigns s Term.T
+
+globalVariable :: Term.Name -> ST s (Variable s)
+globalVariable name =
+   Sys.globalVariable $
+      \x -> writer (Term.Var name, [Assign name x])
+
+constant :: Rational -> Sys.T Assigns s (Variable s)
+constant = Sys.constant . fromRational
+
+
+{- |
+> x=1
+> y=2
+> z=3
+
+> x+y=3
+> y*z=6
+> z=3
+-}
+rule :: ((Maybe Term.T, Maybe Term.T, Maybe Term.T), Assigns)
+rule =
+   runST (do
+      x <- globalVariable "x"
+      y <- globalVariable "y"
+      z <- globalVariable "z"
+      MW.runWriterT $ do
+         Sys.solve $ do
+            c3 <- constant 3
+            c6 <- constant 6
+            Rule.add x y c3
+            Rule.mul y z c6
+            Rule.equ z c3
+         MT.lift $ liftM3
+            (,,)
+            (Sys.query x)
+            (Sys.query y)
+            (Sys.query z))
+
+expression :: ((Maybe Term.T, Maybe Term.T), Assigns)
+expression =
+   runST (do
+      xv <- globalVariable "x"
+      yv <- globalVariable "y"
+      MW.runWriterT $ 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/TF/Example/Rule.hs b/src/UniqueLogic/ST/TF/Example/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Example/Rule.hs
@@ -0,0 +1,46 @@
+module UniqueLogic.ST.TF.Example.Rule
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.TF.Rule as Rule
+import qualified UniqueLogic.ST.TF.System.Simple as Sys
+
+import Control.Monad.ST (runST, )
+import Control.Monad (liftM4, )
+
+import qualified Prelude as P
+import Prelude hiding (max)
+
+
+{- |
+> x=1
+> y=2
+> z=3
+> w=3
+
+> x+y=3
+> y*z=6
+> z=3
+> y^w=8
+-}
+example :: (Maybe Double, Maybe Double, Maybe Double, Maybe Double)
+example =
+   runST (do
+      x <- Sys.globalVariable
+      y <- Sys.globalVariable
+      z <- Sys.globalVariable
+      w <- Sys.globalVariable
+      Sys.solve $ do
+         c3 <- Sys.constant 3
+         c6 <- Sys.constant 6
+         c8 <- Sys.constant 8
+         Rule.add x y c3
+         Rule.mul y z c6
+         Rule.equ z c3
+         Rule.pow y w c8
+      liftM4
+         (,,,)
+         (Sys.query x)
+         (Sys.query y)
+         (Sys.query z)
+         (Sys.query w))
diff --git a/src/UniqueLogic/ST/TF/Example/Term.hs b/src/UniqueLogic/ST/TF/Example/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Example/Term.hs
@@ -0,0 +1,32 @@
+{- |
+This module is intended for documentation purposes. Do not import it!
+-}
+module UniqueLogic.ST.TF.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/TF/Example/Verify.hs b/src/UniqueLogic/ST/TF/Example/Verify.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Example/Verify.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+module UniqueLogic.ST.TF.Example.Verify
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.TF.Example.Term as Term
+import qualified UniqueLogic.ST.TF.Expression as Expr
+import qualified UniqueLogic.ST.TF.System as Sys
+import qualified UniqueLogic.ST.TF.MonadTrans as UMT
+import UniqueLogic.ST.TF.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, when, )
+import Control.Applicative (Applicative, pure, (<*>), )
+
+import qualified Prelude as P
+import Prelude hiding (max, log)
+
+
+
+data Assign = Assign Term.Name (TrackedNumber Rational)
+   deriving (Show)
+
+type Assigns = [Assign]
+
+data TrackedNumber a = TrackedNumber Term.T a
+   deriving (Show)
+
+instance Functor TrackedNumber where
+   fmap f (TrackedNumber term a) = TrackedNumber term $ f a
+
+
+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 (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 = (>>=)
+
+class ToTrackedNumber a where
+   toTrackedNumber :: a -> TrackedNumber Rational
+
+instance (Real a) => ToTrackedNumber (TrackedNumber a) where
+   toTrackedNumber (TrackedNumber term a) =
+      TrackedNumber term $ toRational a
+
+instance (ToTrackedNumber tn) => Sys.Value Track tn where
+   data ValueConstraint Track tn =
+           (ToTrackedNumber tn) => VerifyConstraint
+   valueConstraint _ _ = VerifyConstraint
+
+instance Sys.C Track where
+   update al av act =
+      case Sys.valueConstraint al av of
+         VerifyConstraint ->
+            Sys.updateAndCheck
+               (\old new ->
+                  inconsistency Nothing (toTrackedNumber old) (toTrackedNumber new))
+               al av act
+
+
+newtype
+   Track m a =
+      Track {runTrack :: ME.ExceptionalT Exception (MW.WriterT Assigns m) a}
+
+data
+   Exception =
+      Exception (Maybe Term.Name) (TrackedNumber Rational) (TrackedNumber Rational)
+   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 $ Just name) al av . logUpdate name)
+
+
+match :: (Eq a) => TrackedNumber a -> TrackedNumber a -> Bool
+match (TrackedNumber _ x) (TrackedNumber _ y)  =  x==y
+
+inconsistency ::
+   Monad m =>
+   Maybe Term.Name ->
+   TrackedNumber Rational ->
+   TrackedNumber Rational ->
+   UMT.Wrap Track m ()
+inconsistency name old new =
+   when (not $ match old new) $
+   UMT.wrap $ Track $ ME.throwT $ Exception name old new
+
+logUpdate ::
+   (Real a) =>
+   Term.Name ->
+   MaybeT (ST s) (TrackedNumber a) ->
+   MaybeT (UMT.Wrap Track (ST s)) (TrackedNumber a)
+logUpdate name act = do
+   tn@(TrackedNumber _ x) <- mapMaybeT UMT.lift act
+   MT.lift $ UMT.wrap $ Track $ MT.lift $
+      writer (TrackedNumber (Term.Var name) x, [Assign name $ fmap toRational tn])
+
+
+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/TF/Expression.hs b/src/UniqueLogic/ST/TF/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Expression.hs
@@ -0,0 +1,181 @@
+{-# LANGUAGE FlexibleContexts #-}
+module UniqueLogic.ST.TF.Expression (
+   T,
+   -- * Construct primitive expressions
+   constant, fromVariable,
+   -- * Operators from rules with small numbers of arguments
+   fromRule1, fromRule2, fromRule3,
+   -- * Operators from rules with any number of arguments
+   Apply, arg, runApply,
+   -- * Predicates on expressions
+   (=:=),
+   -- * Common operators (see also 'Num' and 'Fractional' instances)
+   (=!=),
+   sqr, sqrt,
+   max, maximum,
+   pair,
+   ) where
+
+import qualified UniqueLogic.ST.TF.Rule as Rule
+import qualified UniqueLogic.ST.TF.System as Sys
+
+import Control.Monad (ap, )
+import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )
+
+-- import Control.Category ((.))
+-- import Data.Maybe (Maybe)
+
+-- import Prelude (Double, Eq, Ord, (+), (*), (/))
+import qualified Prelude as P
+import Prelude hiding (max, maximum, sqrt)
+
+
+{- |
+An expression is defined by a set of equations
+and the variable at the top-level.
+The value of the expression equals the value of the top variable.
+-}
+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.C w, Sys.Value w a) => a -> T w s a
+constant = Cons . Sys.constant
+
+fromVariable :: Sys.Variable w s a -> T w s a
+fromVariable = Cons . return
+
+
+fromRule1 ::
+   (Sys.C w, Sys.Value w 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.C w, Sys.Value w 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
+   rule xv yv
+   return yv
+
+fromRule3, _fromRule3 ::
+   (Sys.C w, Sys.Value w 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
+   zv <- Sys.localVariable
+   rule xv yv zv
+   return zv
+
+
+newtype Apply w s f = Apply (Sys.T w s f)
+
+instance Functor (Apply w s) where
+   fmap f (Apply a) = Apply $ fmap f a
+
+instance Applicative (Apply w s) where
+   pure a = Apply $ return a
+   Apply f <*> Apply a = Apply $ ap f a
+
+
+{- |
+This function allows to generalize 'fromRule2' and 'fromRule3' to more arguments
+using 'Applicative' combinators.
+
+Example:
+
+> fromRule3 rule x y
+>    = runApply $ liftA2 rule (arg x) (arg y)
+>    = runApply $ pure rule <*> arg x <*> arg y
+
+Building rules with 'arg' provides more granularity
+than using auxiliary 'pair' rules!
+-}
+arg ::
+   T w s a -> Apply w s (Sys.Variable w s a)
+arg (Cons x) = Apply x
+
+runApply ::
+   (Sys.C w, Sys.Value w 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
+   f xv
+   return xv
+
+{-
+examples of how to use 'arg' and 'runApply'
+-}
+_fromRule2 rule x = runApply $ liftA rule $ arg x
+_fromRule3 rule x y = runApply $ liftA2 rule (arg x) (arg y)
+
+
+instance (Sys.C w, Sys.Value w 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)
+   (*) = fromRule3 Rule.mul
+   abs = fromRule2 (Sys.assignment2 abs)
+   signum = fromRule2 (Sys.assignment2 signum)
+
+instance (Sys.C w, Sys.Value w a, P.Fractional a) => P.Fractional (T w s a) where
+   fromRational = constant . fromRational
+   (/) = fromRule3 (\z x y -> Rule.mul x y z)
+
+sqr :: (Sys.C w, Sys.Value w a, P.Floating a) => T w s a -> T w s a
+sqr = fromRule2 Rule.square
+
+sqrt :: (Sys.C w, Sys.Value w a, P.Floating a) => T w s a -> T w s a
+sqrt = fromRule2 (flip Rule.square)
+
+
+infixl 4 =!=
+
+(=!=) :: (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
+   Rule.equ xv yv
+   return xv
+
+infix 0 =:=
+
+(=:=) :: (Sys.C w) => T w s a -> T w s a -> Sys.T w s ()
+(=:=) (Cons x) (Cons y) = do
+   xv <- x
+   yv <- y
+   Rule.equ xv yv
+
+
+{- |
+We are not able to implement a full Ord instance
+including Eq superclass and comparisons,
+but we need to compute maxima.
+-}
+max :: (Sys.C w, Ord a, Sys.Value w a) => T w s a -> T w s a -> T w s a
+max = fromRule3 Rule.max
+
+maximum :: (Sys.C w, Ord a, Sys.Value w a) => [T w s a] -> T w s a
+maximum = foldl1 max
+
+
+{- |
+Construct or decompose a pair.
+-}
+pair ::
+   (Sys.C w, Sys.Value w a, Sys.Value w b, Sys.Value w (a,b)) =>
+   T w s a -> T w s b -> T w s (a,b)
+pair = fromRule3 Rule.pair
diff --git a/src/UniqueLogic/ST/TF/MonadTrans.hs b/src/UniqueLogic/ST/TF/MonadTrans.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/MonadTrans.hs
@@ -0,0 +1,68 @@
+{-
+This module could also be part of 'transformers'.
+-}
+module UniqueLogic.ST.TF.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/TF/Rule.hs b/src/UniqueLogic/ST/TF/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Rule.hs
@@ -0,0 +1,80 @@
+module UniqueLogic.ST.TF.Rule (
+   -- * Custom rules
+   generic2,
+   generic3,
+   -- * Common rules
+   equ, pair, max, add, mul, square, pow,
+   ) where
+
+import qualified UniqueLogic.ST.TF.System as Sys
+import qualified UniqueLogic.ST.TF.MonadTrans as UMT
+
+import qualified Prelude as P
+import Prelude hiding (max)
+
+
+generic2 ::
+   (UMT.C w) =>
+   (b -> a) -> (a -> 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 ::
+   (UMT.C w) =>
+   (b -> c -> a) -> (c -> a -> b) -> (a -> b -> 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 :
+   []
+
+
+equ ::
+   (UMT.C w) =>
+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()
+equ = generic2 id id
+
+max ::
+   (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
+
+{- |
+You might be tempted to use the 'pair' rule to collect parameters
+for rules with more than three arguments.
+This is generally not a good idea since this way you lose granularity.
+For building rules with more than three arguments,
+please build according assignments with 'Sys.arg' and 'Sys.runApply'
+and bundle these assignments to rules.
+This is the way, 'generic2' and 'generic3' work.
+-}
+pair ::
+   (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, 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, 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, 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, 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/TF/System.hs b/src/UniqueLogic/ST/TF/System.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/System.hs
@@ -0,0 +1,280 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+module UniqueLogic.ST.TF.System (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Handle duplicates
+   C, update,
+   simpleUpdate, -- should be private in future
+   updateIfNew, -- should be private or with special type
+   updateAndCheck,
+   Fragile(break),
+   Value, ValueConstraint, valueConstraint,
+   -- * Posing statements
+   T,
+   localVariable,
+   constant,
+   assignment2,
+   assignment3,
+   Apply, arg, runApply,
+   -- * Solution
+   solve, solveDepthFirst, solveBreadthFirst,
+   query,
+   ) where
+
+import qualified Control.Monad.Exception.Synchronous as E
+import qualified Control.Monad.Trans.Writer as MW
+import qualified Control.Monad.Trans.Class  as MT
+import qualified UniqueLogic.ST.TF.MonadTrans as UMT
+import qualified Data.Sequence as Seq
+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 (when, liftM2, ap, guard, )
+import Control.Applicative (Applicative, pure, (<*>), )
+import Data.Sequence (Seq, (|>), ViewL((:<)), )
+import Data.Functor.Compose (Compose(Compose))
+
+import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )
+import Data.Maybe (isNothing, )
+import Data.Monoid (Monoid, mempty, mappend, mconcat, )
+
+import Prelude hiding (break)
+
+
+data Variable w s a =
+   Variable {
+      varUpdate :: MaybeT (ST s) a -> Update w s,
+      dependsRef :: STRef s (Updates w s),
+      valueRef :: STRef s (Maybe a)
+   }
+
+type Update w s = UMT.Wrap w (ST s) (Updates w s)
+newtype Updates w s = Updates {unpackUpdates :: Seq (Update w s)}
+
+instance Monoid (Updates w s) where
+   mempty = Updates Seq.empty
+   mappend (Updates x) (Updates y) = Updates $ mappend x y
+
+addUpdate :: Update w s -> Updates w s -> Updates w s
+addUpdate x (Updates xs) = Updates $ xs |> x
+
+
+type Updater w s a =
+        STRef s (Updates w s) -> STRef s (Maybe a) ->
+        MaybeT (UMT.Wrap w (ST s)) a -> Update w s
+
+type SimpleUpdater w s a =
+        STRef s (Updates w s) -> STRef s (Maybe a) ->
+        MaybeT (ST s) a -> Update w s
+
+newtype T w s a =
+   Cons {run :: WriterT [STRef s (Updates 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, Value w a) =>
+   SimpleUpdater w s a -> ST s (Variable w s a)
+globalVariable triggerUpdate = object triggerUpdate Nothing
+
+localVariable :: (C w, Value w a) => T w s (Variable w s a)
+localVariable = lift $ globalVariable simpleUpdate
+
+constant ::
+   (C w, Value w 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 ::
+   SimpleUpdater w s a ->
+   Maybe a -> ST s (Variable w s a)
+object updater ma = do
+   al <- newSTRef mempty
+   av <- newSTRef ma
+   return $ Variable (updater al av) al av
+
+
+solve, solveDepthFirst, solveBreadthFirst ::
+   UMT.C w =>
+   T w s a -> w (ST s) a
+solve = solveDepthFirst
+
+data Order = DepthFirst | BreadthFirst
+   deriving (Eq, Enum)
+
+solveDepthFirst   = solveOrder DepthFirst
+solveBreadthFirst = solveOrder BreadthFirst
+
+solveOrder ::
+   UMT.C w =>
+   Order -> T w s a -> w (ST s) a
+solveOrder order (Cons m) = UMT.unwrap $ do
+   let resolve updates =
+          case Seq.viewl updates of
+             Seq.EmptyL -> return ()
+             currentUpdate :< remUpdates -> do
+                Updates newUpdates <- currentUpdate
+                resolve $
+                   case order of
+                      DepthFirst -> mappend newUpdates remUpdates
+                      BreadthFirst -> mappend remUpdates newUpdates
+
+   (a, w) <- UMT.lift $ MW.runWriterT m
+   resolve . unpackUpdates . mconcat =<< mapM (UMT.lift . readSTRef) w
+   return a
+
+query :: Variable w s a -> ST s (Maybe a)
+query = readSTRef . valueRef
+
+
+updateIfNew :: (C w) => Updater w s a
+updateIfNew al av act = do
+   as <- UMT.lift $ readSTRef av
+   fmap Fold.fold $ runMaybeT $ do
+      guard $ isNothing as
+      MT.lift . UMT.lift . writeSTRef av . Just =<< act
+      MT.lift $ UMT.lift $ readSTRef 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) =>
+   (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
+   case manew of
+      Nothing -> return mempty
+      Just anew -> do
+         UMT.lift . writeSTRef av . Just $ anew
+         case maold of
+            Just aold -> customBreak aold anew >> return mempty
+            Nothing -> UMT.lift $ readSTRef al
+
+
+class C w => Value w a where
+   data ValueConstraint w a :: *
+   valueConstraint ::
+      STRef s (Updates w s) -> STRef s (Maybe a) -> ValueConstraint w a
+
+class UMT.C w => C w where
+   update :: (Value w a) => Updater w s a
+
+instance Value IdentityT a where
+   data ValueConstraint IdentityT a = IdentityConstraint
+   valueConstraint _ _ = IdentityConstraint
+
+instance C IdentityT where
+   update = updateIfNew
+
+instance (Monoid w) => Value (MW.WriterT w) a where
+   data ValueConstraint (MW.WriterT w) a = WriterConstraint
+   valueConstraint _ _ = WriterConstraint
+
+instance (Monoid w) => C (MW.WriterT w) where
+   update = updateIfNew
+
+instance (Inconsistency e, Eq a) => Value (E.ExceptionalT e) a where
+   data ValueConstraint (E.ExceptionalT e) a =
+           Eq a => ExceptionConstraint
+   valueConstraint _ _ = ExceptionConstraint
+
+instance (Inconsistency e) => C (E.ExceptionalT e) where
+   update al av act =
+      case valueConstraint al av of
+         ExceptionConstraint ->
+            updateAndCheck (\aold anew -> when (aold /= anew) break) al av act
+
+simpleUpdate :: (C w, Value w a) => SimpleUpdater w s a
+simpleUpdate al av = update al av . mapMaybeT UMT.lift
+
+
+readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a
+readSTRefM = MaybeT . readSTRef
+
+
+assignment2 ::
+   UMT.C w =>
+   (a -> b) ->
+   Variable w s a -> Variable w s b ->
+   T w s ()
+assignment2 f (Variable _ al av) b =
+   let triggerUpdate =
+          varUpdate b $ fmap f $ readSTRefM av
+   in  lift $
+       modifySTRef al (addUpdate triggerUpdate)
+
+assignment3 ::
+   UMT.C w =>
+   (a -> b -> 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 triggerUpdate =
+          varUpdate c $
+          liftM2 f (readSTRefM av) (readSTRefM bv)
+   in  lift $
+       modifySTRef al (addUpdate triggerUpdate) >>
+       modifySTRef bl (addUpdate triggerUpdate)
+
+
+newtype Apply w s a =
+   Apply (Compose (MW.Writer [STRef s (Updates 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 :: 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 (addUpdate $ varUpdate a f)
diff --git a/src/UniqueLogic/ST/TF/System/Label.hs b/src/UniqueLogic/ST/TF/System/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/System/Label.hs
@@ -0,0 +1,47 @@
+module UniqueLogic.ST.TF.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,
+   ) where
+
+import qualified UniqueLogic.ST.TF.System as Sys
+import qualified UniqueLogic.ST.TF.MonadTrans as UMT
+
+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) =>
+   (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/TF/System/Simple.hs b/src/UniqueLogic/ST/TF/System/Simple.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/System/Simple.hs
@@ -0,0 +1,42 @@
+module UniqueLogic.ST.TF.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.TF.System as Sys
+
+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 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
+
+solve :: T s a -> ST s a
+solve = runIdentityT . Sys.solve
+
+query :: Variable s a -> ST s (Maybe a)
+query = Sys.query
diff --git a/src/UniqueLogic/ST/TF/Test.hs b/src/UniqueLogic/ST/TF/Test.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/TF/Test.hs
@@ -0,0 +1,78 @@
+module Main where
+
+import qualified UniqueLogic.ST.TF.Expression as Expr
+import qualified UniqueLogic.ST.TF.System.Simple as Sys
+import UniqueLogic.ST.TF.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.List (sortBy, )
+import Data.Ord.HT (comparing, )
+
+import qualified Data.NonEmpty as NonEmpty
+import qualified Test.QuickCheck as QC
+
+
+shuffle :: NonEmpty.T [] Int -> [a] -> [a]
+shuffle order =
+   map snd . sortBy (comparing fst) .
+   zip (NonEmpty.flatten $ NonEmpty.cycle order)
+
+newtype Check s = Check {runCheck :: ST s Bool}
+
+instance Monoid (Check s) where
+   mempty = Check $ return True
+   mappend (Check x) (Check y) = Check $ liftM2 (&&) x y
+
+{-
+Take a system of six equations and seven variables
+where one variable is randomly chosen and initialized with the correct value.
+The other six variables must be determined by the solver.
+Then we pose the six equations and
+finally check whether all variables got the right value.
+-}
+example :: Int -> NonEmpty.T [] Int -> Bool
+example var order =
+   runST
+      (join . fmap runCheck . Sys.solve $ MW.execWriterT $ do
+         let variable ::
+                Int -> Rational ->
+                MW.WriterT (Check s) (Sys.T s)
+                   (Expr.T IdentityT s Rational)
+             variable n x = do
+                v <-
+                   MT.lift $
+                   if mod var 7 == n
+                     then Sys.constant x
+                     else Sys.localVariable
+                MW.tell $ Check $ fmap (Just x ==) $ Sys.query v
+                return $ Expr.fromVariable v
+
+         c  <- variable 0 1
+         x0 <- variable 1 2
+         x1 <- variable 2 3
+         y0 <- variable 3 4
+         y1 <- variable 4 5
+         z0 <- variable 5 6
+         z1 <- variable 6 7
+
+         MT.lift $ sequence_ $ shuffle order $
+            (c+1 =:= x0) :
+            (x1*2 =:= x0*3) :
+            (2*c + y0/2 =:= 4) :
+            (y0 =:= subtract 1 y1) :
+            (c =:= z0/6) :
+            (z0*z1 =:= 42) :
+            [] )
+
+
+tests :: [(String, IO ())]
+tests = [("example", QC.quickCheck example)]
+
+main :: IO ()
+main = mapM_ (\(msg, test) -> putStr (msg ++ " ") >> test) tests
diff --git a/unique-logic-tf.cabal b/unique-logic-tf.cabal
new file mode 100644
--- /dev/null
+++ b/unique-logic-tf.cabal
@@ -0,0 +1,109 @@
+Name:             unique-logic-tf
+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-tf/
+Category:         Logic programming
+Synopsis:         Solve simple simultaneous equations
+Description:
+  Solve a number of equations simultaneously.
+  This is not Computer Algebra,
+  better think of a kind of type inference algorithm
+  or logic programming with only one allowed solution.
+  .
+  Only one solution is computed.
+  Simultaneous equations with multiple solutions are not allowed.
+  However, variables may remain undefined.
+  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:
+  .
+  * "UniqueLogic.ST.TF.System":
+    Construct and solve sets of functional dependencies.
+    Example: @assignment3 (+) a b c@ meaning dependency @a+b -> c@.
+  .
+  * "UniqueLogic.ST.TF.Rule":
+    Combine functional dependencies to rules
+    that can apply in multiple directions.
+    Example: @add a b c@ means relation @a+b = c@
+    which resolves to dependencies @a+b -> c, c-a -> b, c-b -> a@.
+    For an executable example see "UniqueLogic.ST.TF.Example.Rule".
+  .
+  * "UniqueLogic.ST.TF.Expression":
+    Allows to write rules using arithmetic operators.
+    It creates temporary variables automatically.
+    Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.
+    For an executable example see "UniqueLogic.ST.TF.Example.Expression".
+  .
+  * "UniqueLogic.ST.TF.System.Simple":
+    Provides specialised functions from "UniqueLogic.ST.TF.System"
+    for the case of a system without labels and consistency checks.
+  .
+  * "UniqueLogic.ST.TF.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
+    using symbolic expressions.
+    The naming and logging allows us to observe shared intermediate results.
+    For an executable example see "UniqueLogic.ST.TF.Example.Label".
+  .
+  * 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.TF.Example.Verify".
+  .
+  This variant of the package requires type families.
+Tested-With:       GHC==7.4.2
+Cabal-Version:     >=1.8
+Build-Type:        Simple
+
+Source-Repository this
+  Tag:         0.4
+  Type:        darcs
+  Location:    http://code.haskell.org/~thielema/unique-logic-tf/
+
+Source-Repository head
+  Type:        darcs
+  Location:    http://code.haskell.org/~thielema/unique-logic-tf/
+
+Library
+  Build-Depends:
+    explicit-exception >=0.1.7 && <0.2,
+    transformers >=0.2 && <0.4,
+    containers >=0.4 && <0.6,
+    utility-ht >=0.0.9 && <0.1,
+    base >= 4 && <5
+  GHC-Options:      -Wall
+  Hs-Source-Dirs:   src
+
+  Exposed-Modules:
+    UniqueLogic.ST.TF.MonadTrans
+    UniqueLogic.ST.TF.System
+    UniqueLogic.ST.TF.System.Simple
+    UniqueLogic.ST.TF.System.Label
+    UniqueLogic.ST.TF.Rule
+    UniqueLogic.ST.TF.Expression
+    -- example modules
+    UniqueLogic.ST.TF.Example.Rule
+    UniqueLogic.ST.TF.Example.Label
+    UniqueLogic.ST.TF.Example.Expression
+    UniqueLogic.ST.TF.Example.Verify
+    UniqueLogic.ST.TF.Example.Term
+
+Test-Suite test-unique-logic
+  Type:    exitcode-stdio-1.0
+  Main-Is: src/UniqueLogic/ST/TF/Test.hs
+  GHC-Options: -Wall
+  Build-Depends:
+    unique-logic-tf,
+    QuickCheck >=2.4 && <2.6,
+    non-empty >=0.0 && <0.1,
+    transformers,
+    utility-ht,
+    base