diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,34 @@
+The module free-theorems-seq-0.1 can be installed via
+
+cabal install
+
+or the following way:
+
+runhaskell Setup.hs configure --user
+runhaskell Setup.hs build
+runhaskell Setup.hs haddock
+runhaskell Setup.hs install
+
+runhaskell Setup.hs haddock builds the documentation.
+This step is not necessary.
+
+After installation the modules
+        Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq
+        Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint
+        Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator
+        Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight
+are available.
+
+The functionality of the library is also available via a webinterface
+that is either available via the package at
+
+http://hackage.haskell.org/package/free-theorems-seq-webui
+
+or can be used online at
+
+http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi.
+
+Enjoy.
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,5 @@
+#!/usr/bin/runhaskell
+
+import Distribution.Simple
+
+main = defaultMain
diff --git a/free-theorems-seq.cabal b/free-theorems-seq.cabal
new file mode 100644
--- /dev/null
+++ b/free-theorems-seq.cabal
@@ -0,0 +1,72 @@
+name:           free-theorems-seq
+version:        1.0
+license:        PublicDomain
+author:         Daniel Seidel
+maintainer:     ds@iai.uni-bonn.de
+synopsis:       Taming Selective Strictness
+description:
+	Given a term, this program calculates a set of \"optimal\" free theorems 
+        that hold in a lambda calculus with selective strictness. It omits 	
+        totality (in general, bottom-reflection) and other restrictions when 
+        possible. The underlying theory is described in the paper \"Taming 
+        Selective Strictness\" (ATPS'09) by Daniel Seidel and Janis Voigtländer.
+	A webinterface for the program is running online at 
+	<http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi>
+        or available offline via the package 
+        <http://hackage.haskell.org/package/free-theorems-seq-webui>.
+        .
+        Related to this package you may be interested in the online free theorem generator
+        at <http://www-ps.iai.uni-bonn.de/ft> that is also available offline via
+        <http://hackage.haskell.org/package/free-theorems-webui>.
+        Additionally interesting may be the counterexample generator for free theorems that
+        exemplifies the need of strictness conditions imposed by general recursion.
+        It can be downloaded at 
+        <http://hackage.haskell.org/package/free-theorems-counterexamples>
+        or used via a webinterface at
+        <http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi>.
+	
+category:       Language
+tested-with:    GHC==7.0.1
+build-type:	Simple
+cabal-version:  >= 1.6
+
+extra-source-files:
+    src/Tests.hs
+    README
+
+library
+    build-depends:
+        array == 0.*
+      , bytestring >= 0.9.0.1
+      , containers >= 0.1.0.1 
+      , free-theorems >= 0.3.1 && < 0.4
+      , haskell-src >= 1.0.1.1 
+      , mtl >= 1.1.0.0
+      , old-locale == 1.*
+      , old-time == 1.* 
+      , parsec == 3.*
+      , pretty == 1.*
+      , utf8-string >= 0.3.1.1 && < 0.4
+      , xhtml == 3000.*
+    if impl(ghc >= 6.10)
+      build-depends:
+          base >= 4
+        , syb >= 0.1.0.0
+    else
+      build-depends:
+          base >= 1 && < 4
+    exposed-modules:
+        Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq
+        Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint
+        Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator
+        Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight
+    other-modules:
+        Language.Haskell.FreeTheorems.Variations.PolySeq.M
+        Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Debug
+        Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg
+        Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon
+        Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+    hs-source-dirs: src
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/AlgCommon.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/AlgCommon.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/AlgCommon.hs
@@ -0,0 +1,170 @@
+{-# OPTIONS_GHC -XTypeOperators -XRank2Types #-}
+{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, DeriveDataTypeable #-} 
+module Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon
+    (Cont(..)
+    , emptyCont
+    , addTermVar
+    , addTypVar
+    , getLabTVar
+    , getTypVarInCont
+    , makeLabel
+    , getElemType
+    , getArrowComps
+    , isInt
+    , isBool
+    , getAllComps
+    , instantiateWithEpsilon
+    , annotate
+    , removeTrue
+    , getEquals
+    , substTyp
+--    , parseTerm
+--    , collectAll
+    , collectOne
+    , substLabel
+    , getUsedLabels
+    , getUsedExtraLabels
+    ) where
+
+import Data.Generics(Data, everywhere, everywhereM, mkT, mkQ, mkM, gmapT, gmapQ)
+import Data.List(nub)
+import Control.Monad(mplus)
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.M
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+
+-- |representation of \Gamma
+data Cont = Cont { tVars :: [(TypVar,Label)], vars :: [TypedVar] } deriving (Show,Eq)
+
+emptyCont :: Cont
+emptyCont = Cont [] []
+
+-- * auxiliar functions
+
+addTermVar :: Cont -> TypedVar -> Cont
+addTermVar (Cont tVars vars) v = Cont tVars (v:vars)
+
+addTypVar :: Cont -> (TypVar,Label) -> Cont
+addTypVar (Cont tVars vars) tv = Cont (tv:tVars) vars
+
+getTypVarInCont :: Cont -> TermVar -> M Typ
+getTypVarInCont gamma v = 
+    case filter (\x->(fst x == v)) (vars gamma) of
+      [(_,tau)] -> return tau
+      _        -> abort
+
+getLabTVar :: Cont -> TypVar -> M Label
+getLabTVar gamma tv =
+    case filter (\x->(fst x == tv)) (tVars gamma) of
+      [(_,lab)] -> return lab
+      _         -> abort
+
+makeLabel :: M Label
+makeLabel = do{ i <- newLab;
+		return (LVar (LabVar i))
+	      }
+
+getElemType :: Typ -> M Typ
+getElemType tau =
+    case tau of
+      TList tau' -> return tau'
+      _          -> abort
+
+getArrowComps :: Typ -> M (Typ,Typ)
+getArrowComps tau =
+    case tau of
+      TArrow _ tau1 tau2 -> return (tau1,tau2)
+      _                  -> abort
+    
+getAllComps :: Typ -> M (Label,TypVar,Typ)
+getAllComps tau =
+    case tau of
+      TAll lab tv tau' -> return (lab,tv,tau')
+      _                -> abort
+
+isInt :: Typ -> M ()
+isInt tau = if tau == TInt then return () else abort
+
+isBool :: Typ -> M ()
+isBool tau = if tau == TBool then return () else abort
+
+annotate dat = everywhereM (mkM nonToVar) dat
+
+nonToVar :: Label -> M Label
+nonToVar l = if l == Non then makeLabel else return l
+
+substLabel :: (Data a) => Label -> Label -> a -> a
+substLabel new old dat = everywhere (mkT (substLab new old)) dat
+
+substLab :: Label -> Label -> Label -> Label
+substLab new old recent =
+    if old == recent then new else recent
+
+substTyp :: Typ -> Typ -> TypVar -> Typ
+substTyp tau new old = (justUnboundTypVars old) (mkT (substTV new old)) tau
+
+justUnboundTypVars :: TypVar -> (Typ -> Typ) -> Typ -> Typ
+justUnboundTypVars tv sub tau =
+    case tau of
+      TAll _ tv' _ -> if tv == tv' then tau else gmapT (mkT (justUnboundTypVars tv sub)) (sub tau)
+      _            -> gmapT (mkT (justUnboundTypVars tv sub)) (sub tau)
+
+substTV :: Typ -> TypVar -> Typ -> Typ
+substTV new old tau = case tau of
+                      TVar tv -> if tv == old then new else tau
+                      _            -> tau
+
+
+getEquals :: Constraint -> [(Label,Label)]
+getEquals c = getEquals' (mkQ [] rmEq) c
+
+getEquals' f c =
+    case c of
+      Impl c1 c2 -> concat ((f c1) : (gmapQ  (mkQ [](getEquals' f)) c1))
+      _          -> concat ((f c) : (gmapQ (mkQ [] (getEquals' f)) c))
+
+rmEq c =
+    case c of
+      Eq l1 l2 -> case l1 of
+                    LVar (LabVar i) -> case l2 of
+                                         LVar (LabVar j) -> if i<j then [(l1,l2)] else [(l2,l1)]
+                                         _               -> [(l1,l2)]
+                    _               -> [(l2,l1)]
+      _        -> []
+
+collectAll :: (Data a) => (forall a1. (Data a1) => a1 -> [u]) -> a -> [u]
+collectAll f c = concat ((f c) : (gmapQ (collectAll f) c)) 
+
+collectOne :: (Data a) => (forall a1. (Data a1) => a1 -> Maybe u) -> a -> Maybe u
+collectOne f c = foldl mplus (f c) (gmapQ (collectOne f) c) 
+
+
+removeTrue :: Constraint -> Constraint
+removeTrue = everywhere (mkT remTru)
+
+remTru :: Constraint -> Constraint
+remTru c =
+    case c of
+      Conj Tru c2 -> c2
+      Conj c1 Tru -> c1
+      Impl Tru c2 -> c2
+      _           -> c
+
+
+instantiateWithEpsilon :: Typ -> Typ
+instantiateWithEpsilon tau = everywhere (mkT instWithEpsilon) tau
+
+instWithEpsilon :: Label -> Label
+instWithEpsilon l = LVal Epsilon
+
+getUsedLabels :: (Data a) => a -> [Int]
+getUsedLabels = getUsedExtraLabels []
+
+getUsedExtraLabels ::(Data a) => [Int] -> a -> [Int]
+getUsedExtraLabels notIn x = nub (collectAll (mkQ [] (getLabVar notIn)) x)
+
+getLabVar :: [Int] -> LabVar -> [Int]
+getLabVar ls (LabVar i) = if i `elem` ls then [] else [i]
+
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs
@@ -0,0 +1,314 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint(prettyConstraint) --only for debugging
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon
+    ( collectOne
+    , substLabel
+    , getUsedLabels
+    , getUsedExtraLabels
+    , removeTrue
+    )
+import qualified Data.List as List
+import qualified Data.Map as Map
+import Data.Generics(everywhere, mkQ, mkT)
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug
+import Control.Monad(mplus)
+import Data.Function
+
+--debuging stuff
+trace2 = trace_ignore
+trace = trace_ignore
+trace1 = trace_ignore
+
+-- | simplifies the initial constraint and replaces variables in term and type
+simplifyConstraint :: (Term,Typ,Constraint) -> (Term,Typ,Constraint)
+simplifyConstraint (t',tau',c') =
+    let (t,tau,c) = simpConstraint (t',tau',c') in
+    (t,tau,checkContradiction (removeTrue c))
+
+-- | subfunction of simplifyConstraint
+simpConstraint :: (Term,Typ,Constraint) -> (Term,Typ,Constraint)
+simpConstraint (t,tau,c') =
+    let c = removeUseless c' in
+    case findEq c of
+      Just (Eq l1 l2)      -> trace "found Eq by findEq" (if l1 /= (LVal Epsilon) 
+                              then simpConstraint (substLabel l2 l1 t, substLabel l2 l1 tau, substLabel l2 l1 c)
+			      else simpConstraint (substLabel l1 l2 t, substLabel l1 l2 tau, substLabel l1 l2 c))
+      Nothing ->
+        case findGtEpsilon c of
+        Just (Leq _ l)     -> trace "found GtEpsilon" (simpConstraint (substLabel (LVal Epsilon) l t, substLabel (LVal Epsilon) l tau, substLabel (LVal Epsilon) l c))
+        Nothing ->
+          case findLtNbr c of
+            Just (Leq l _) -> trace "found LtNbr" (simpConstraint (substLabel (LVal Nbr) l t, substLabel (LVal Nbr) l tau, substLabel (LVal Nbr) l c))
+	    Nothing        -> (t,tau,c)
+
+-- | removes Equations and InEquations, that are always fulfilled
+removeUseless :: Constraint -> Constraint
+removeUseless = everywhere (mkT rmUseLess)
+
+-- | generic function for removing trivial parts of the constraint
+rmUseLess c =
+    case c of
+      Conj c1 c2 -> if useLess c1 then c2 else if useLess c2 then c1 else Conj c1 c2
+      Impl (Eq (LVal (Epsilon)) (LVal (Epsilon))) c2 -> c2
+      Impl (Eq (LVal (Nbr))     (LVal (Epsilon))) _  -> Tru
+      _           -> if useLess c then Tru else c
+
+-- | checks if a constraint is trivial
+useLess c =
+  case c of
+    Eq  c1 c2 -> if c1 == c2 then True else False
+    Leq _ (LVal (Epsilon))           -> True
+    Leq (LVal (Nbr)) _               -> True
+    Leq (LVar (LabVar i)) (LVar (LabVar j)) -> if i == j then True else False
+    _                                       -> False
+
+-- | returns the first Equation part of a constraint. Does not consider Equations in the body of an implication
+findEq :: Constraint -> Maybe Constraint
+findEq c =
+    case c of
+      Conj c1 c2 -> findEq c1 `mplus` findEq c2
+      Eq _ _     -> Just c
+      _          -> Nothing
+
+
+-- | returns the first "epsilon <= x" inequation part of a constraint. Does consider Equations in the body of an implication
+findGtEpsilon = collectOne (mkQ Nothing fndGtEpsilon)
+
+
+-- | generic function for findGtEpsilon
+fndGtEpsilon :: Constraint -> Maybe Constraint
+fndGtEpsilon c =
+  case c of
+    Leq (LVal (Epsilon)) _ -> Just c
+    _                      -> Nothing
+
+
+-- | returns the first "x <= nbr" inequation part of a constraint. Does consider Equations in the body of an implication
+findLtNbr = collectOne (mkQ Nothing fndLtNbr)
+
+
+-- | generic function for findLtNbr
+fndLtNbr :: Constraint -> Maybe Constraint
+fndLtNbr c =
+  case c of
+    Leq _ (LVal (Nbr)) -> Just c
+    _                  -> Nothing
+
+
+-- | returns Fls if the constraint is has no solution, otherwise the whole constraint
+checkContradiction :: Constraint -> Constraint
+checkContradiction c = 
+    case fndContr c of
+      Just _  -> Fls
+      Nothing -> c
+
+
+-- | auxiliar function, used in checkContradiction
+fndContr :: Constraint -> Maybe Constraint
+fndContr c =
+    case c of
+      Eq  (LVal Nbr) (LVal Epsilon) -> Just c
+      Eq  (LVal Epsilon) (LVal Nbr) -> Just c
+      Leq (LVal Epsilon) (LVal Nbr) -> Just c
+      Conj c1 c2                    -> fndContr c1 `mplus` fndContr c2
+      _                             -> Nothing
+				       
+
+-- | the first component of the returned tuple are the label variable numbers of the instantiated labels and the second
+--   component is an array of all possible instantiation. For each instantiation the order matches the order of the 
+--   variables in the first component of the tuple.
+solveConstraint :: Constraint -> ([Int],[[LabVal]])
+solveConstraint c =
+    let labConstr = getUsedLabels$c
+	vars = List.sort labConstr
+        vals = (map (snd.unzip.(Map.toAscList)) (slvConstr labConstr Map.empty c))
+    in
+    trace1 ("solveConstraint produces\n"++ show vars ++ "with values\n" ++ show vals ++ "n") (vars,vals)
+
+
+-- | Used by solveConstraint. Kind of breadth-first search for valid variable instantiations, aborting whenever a
+--   partial instantiation leads to a contradiction in the constraint.
+--   The map keeps track of all already instantiated variables and the list as first argument are the still free
+--   variables.
+--   The final result is a list of all possible complete (first argument is []) instantiations in form of a map
+--   with variable number as key and concrete LabVal (Epsilon or Nbr) as value.
+slvConstr :: [Int] -> Map.Map Int LabVal -> Constraint -> [Map.Map Int LabVal]
+slvConstr vars map c =
+    case vars of
+      []   -> [map]
+      i:is -> let c1  = substLabel (LVal Nbr)     (LVar (LabVar i)) c
+		  c2  = substLabel (LVal Epsilon) (LVar (LabVar i)) c in
+	      solve Nbr c1 ++ solve Epsilon c2
+              where 
+              solve lab c' = trace1 ("starting solve with " ++ show (prettyConstraint c')) (
+                case reduceConstraint [(i,lab)] c' of
+                  Nothing -> []
+                  Just (as,c'') ->
+                    let map'   = Map.union map (Map.fromList as)
+		        asvars = fst.unzip$as
+                        vars'  = filter (flip notElem asvars) is
+                    in
+                    slvConstr vars' map' c'')
+
+
+-- | takes a list of variable instantiations, allready done in the constraint, and the constraint. It adds further
+--   variable instantiations, if possible, after reducing the constraint.
+--   It is called recursively until no further instantiation is possible.
+reduceConstraint :: [(Int,LabVal)] -> Constraint -> Maybe ([(Int,LabVal)],Constraint)
+reduceConstraint as c' =
+    let c = removeTrue.removeUseless$c' in
+    if checkContradiction c == Fls then Nothing
+    else
+    case findEq c of
+      Just (Eq l1 l2)      -> trace "found Eq by findEq"(
+			      case l1 of
+                              LVar (LabVar i) -> let LVal w = l2 in reduceConstraint ((i,w):as) (substLabel l2 l1 c)
+			      LVal w -> let LVar (LabVar i) = l2 in reduceConstraint ((i,w):as) (substLabel l1 l2 c))
+      Nothing ->
+        case findGtEpsilon c of
+        Just (Leq _ (LVar (LabVar i))) -> trace "found GtEpsilon" (		   
+					  reduceConstraint ((i,Epsilon):as) (substLabel (LVal Epsilon) (LVar (LabVar i))  c))
+	Just c'                        -> error ("strange Constraint: " ++ show c' ++ "\n")
+        Nothing ->
+          case findLtNbr c of
+            Just (Leq (LVar (LabVar i)) _) -> trace "found LtNbr" (reduceConstraint ((i,Nbr):as) (substLabel (LVal Nbr) (LVar (LabVar i))  c))
+	    Just c'                        -> error ("strange Constraint: " ++ show c' ++ "\n")
+	    Nothing        -> case checkContradiction c of
+			        Fls -> Nothing
+                                _   -> Just (as,c)
+
+
+-- | reduces the possible type instantiations to the variables that appear in the given term and type.
+--   Also removing duplicates.
+filterTermAndTyp :: Term -> Typ -> ([Int],[[LabVal]]) -> ([Int],[[LabVal]])
+filterTermAndTyp t tau  res = 
+    let labTerm = getUsedLabels t
+        labTermTyp = getUsedExtraLabels labTerm tau
+        (varList,resList) = filterLabVars labTermTyp res
+    in 
+    (varList,List.nub resList)
+
+
+-- | reduces the possible type instantiations to the variables that appear in the given type.
+--   Also removing duplicates.
+filterTyp :: Typ -> ([Int],[[LabVal]]) -> ([Int],[[LabVal]])
+filterTyp tau res = 
+    let labTyp = getUsedLabels tau
+        (varList,resList) = filterLabVars labTyp res
+    in 
+    (varList,List.nub resList)
+
+
+-- | auxiliar function used by filterTermAndTyp and filterTyp
+filterLabVars varList (vars,vals) =
+    case vars of
+      []   -> (vars,vals)
+      x:xs -> let (vrs, vls) = filterLabVars varList (xs,map tail vals) in
+              if x `elem` varList then
+              (x:vrs,zipWith (:) (map head vals) vls)
+	      else (vrs,vls)
+
+
+-- | takes a type and an array of instantiations (second component of the input tuple) for a subset of label
+--    variables present in that type (first component of the input variable) and returns a list of types,
+--    all partly instantiated by the one of the given instantiations.
+makeTypes :: Typ -> ([Int],[[LabVal]]) -> [Typ]
+makeTypes tau (vars, res) =
+    map (\x->substLabFromList tau (zip vars x)) res
+    where substLabFromList tau' l =
+            case l of
+              []         -> tau'
+              (i,val):xs -> substLabFromList (substLabel (LVal val) (LVar (LabVar i)) tau') xs
+
+
+-- | takes a type and an array of instantiations (second component of the input tuple) for a subset of label
+--    variables present in that type (first component of the input variable) and returns a list of types,
+--    all completely instantiated and including one of the partial instantiation given, such that no other
+--    complete instantiation, including one of the given partial instantiations as a subset of the logical relation.
+--    as logical relation.
+makeMinimalTypes :: Typ -> ([Int],[[LabVal]]) -> [Typ]
+makeMinimalTypes tau (vars,valss) =
+    let (setVarOpt,unsetVarOpt) = List.partition (\x->(fst x) `elem` vars) (getOptimal tau) --should still be sorted
+        types = makeTypes tau (vars, 
+			       getMinimal (snd.unzip$
+					   (trace2 ("the setOptVars are: " ++ show setVarOpt ++ "\n\n") 
+					    setVarOpt)) 
+			                  valss)
+    in
+    concat (map (getOptTypes unsetVarOpt) types)
+  where
+    --lessEqual. returns True if the logical relation of vals1 is a subset of the logical relation of vals2
+    leq opts vals1 vals2 = --smaller is better -> opts has the smallest logical relation
+      case opts of
+       [] -> True
+       o:os -> let v1:vs1 = vals1
+                   v2:vs2 = vals2
+               in
+               if o == Non then leq os vs1 vs2
+               else if LVal v1 == o && LVal v2 /= o then False 
+                    else leq os vs1 vs2
+    --notGreaterEqual, returns false if the logical relation of vals2 is a superset of the logical relation of vals1
+    --Note: Since we have only a partial order leq /= notgeq.
+    notgeq opts vals1 vals2 = --smaller is better -> opts has the smallest logical relation
+      case opts of
+       [] -> False
+       o:os -> let v1:vs1 = vals1
+                   v2:vs2 = vals2
+               in
+               if o == Non then notgeq os vs1 vs2
+               else if LVal v2 == o && LVal v1 /= o then True
+                    else notgeq os vs1 vs2
+    -- sorts out the optimal (minimal logical relation) from all instantiations produced by the constraint
+    -- notice that this is for normally the instantiation of just a part of all label variables in the type.
+    getMinimal opts valss =
+      case valss of
+        [] -> []
+        x:xs -> case List.find (leq opts x) xs of
+                Nothing -> x : getMinimal opts (filter (notgeq opts x) xs)
+                Just _  -> getMinimal opts xs
+    -- instantiates label variables with no previous restriction on it and returns a set of optimal instantiations.
+    getOptTypes opts typ =
+      case opts of
+        [] -> [typ]
+        (i,opt):xs -> case opt of
+                        Non          -> (getOptTypes xs (substLabel (LVal Epsilon) (LVar (LabVar i)) typ))
+					++ (getOptTypes xs (substLabel (LVal Nbr) (LVar (LabVar i)) typ))
+                        LVal Nbr     -> getOptTypes xs (substLabel (LVal Nbr)     (LVar (LabVar i)) typ)
+                        LVal Epsilon -> getOptTypes xs (substLabel (LVal Epsilon) (LVar (LabVar i)) typ)
+                     
+
+-- |returns the optimal (minimal logical relations) instantiation of a type in the form
+--  LVal Epsilon, LVal Nbr or Non. Where Non stands for both, Epsilon and Nbr, would lead
+--  to a minimal type.
+--  Note that first there might be several optimal instantiations for the same label variable, which are
+--  afterwards removed by resolveConflicts. This actually is the first time Non can appear.
+getOptimal :: Typ -> [(Int,Label)]
+getOptimal tau = resolveConflicts (List.sortBy  (compare  `on` fst) (getOpt True tau))
+  where resolveConflicts l =
+          case l of
+            []   -> []
+            [x]  -> [x]
+            (i,l1):(j,l2):xs -> if i == j then
+                                  if l1 /= l2 then resolveConflicts ((i,Non):xs)
+                                  else resolveConflicts ((i,l1):xs)
+                                else (i,l1):(resolveConflicts ((j,l2):xs))
+
+
+-- | returns the optimal instantiation for a label variable. It is always LVal Nbr or LVal Epsilon.
+--   the first parameter marks if the logical relation has to be minimised (True) or maximised (False)
+getOpt :: Bool -> Typ -> [(Int,Label)]
+getOpt min tau =
+    case tau of
+      TVar _                             -> []
+      TArrow (LVar (LabVar i)) tau1 tau2 -> ((i,opt):(getOpt (not min) tau1)) ++ (getOpt min tau2)
+      TArrow _ tau1 tau2                 -> (getOpt (not min) tau1) ++ (getOpt min tau2)
+      TAll (LVar (LabVar i)) _ tau1      -> (i,notOpt):(getOpt min tau1)
+      TAll _ _ tau1                      -> getOpt min tau1
+      TList tau1                         -> getOpt min tau1
+      TInt                               -> []
+      TBool                              -> []
+    where 
+      opt    = if min == False then LVal Nbr else LVal Epsilon
+      notOpt = if min == True  then LVal Nbr else LVal Epsilon
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs
@@ -0,0 +1,18 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.Debug 
+    (trace_ignore, trace_toShell,
+     traceM_ignore, traceM_toShell) where
+
+import System.IO.Unsafe
+
+trace_ignore :: String -> a -> a
+trace_ignore str a = a
+
+trace_toShell str a = if unsafePerformIO (putStr (str++"\n")) == () then a else a
+
+traceM_ignore :: (Monad m) => String -> m ()
+traceM_ignore str = return ()
+
+traceM_toShell :: (Monad m) => String -> m ()
+traceM_toShell str = if unsafePerformIO (putStr (str++"\n")) == () then return () else return ()
+
+
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs
@@ -0,0 +1,172 @@
+{-OPTIONS_GHC -XFlexibleInstances -XFlexibleContexts -}
+module Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight (highlight,highlightWith) where
+
+import Text.XHtml
+import Text.PrettyPrint.HughesPJ hiding (char,style)
+import Text.Parsec.String(Parser)
+--import Text.Parsec.Token as P
+import Text.Parsec.Combinator(manyTill, lookAhead, eof)
+import Text.Parsec.Prim(ParsecT,Stream,(<|>),try,parse,getParserState)
+import Text.ParserCombinators.Parsec.Char(oneOf,char,anyChar,string)
+--import Text.ParserCombinators.Parsec.Language(emptyDef)
+import Text.Parsec
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug
+
+--traceM = traceM_toShell
+--traceM = traceM_ignore
+--traceState = do state <- getParserState;
+--                traceM ("with the Parser state " ++ show (stateInput state) ++ "\n");	
+
+-- data What = Keyword String
+-- 	  | BottomReflectionRestriction
+
+-- data HighLightMode  = Color String
+--  		    | BgColor String
+
+makeHglt :: String -> (Html -> Html)
+makeHglt mode = thespan![thestyle (mode)]
+
+
+highlightWith :: String -> String -> Html
+highlightWith hgltMode str =
+    let hglt = makeHglt hgltMode
+        res = parse (highlt hglt) "" str in
+    case res of
+      Left err   -> toHtml (show err)
+      Right html -> html
+
+highlight :: String -> Html
+highlight = highlightWith "background-color:yellow;color:red"
+
+-- myLanguage = 
+--     emptyDef
+--     { opStart         = oneOf "<"
+--     , opLetter        = oneOf "<=>"
+--     , reservedOpNames = ["<=>"]
+-- --    , reservedNames   = ["total", "bottom-reflecting"]
+--     , caseSensitive   = True
+--     }
+
+-- lexer = P.makeTokenParser emptyDef
+
+-- par   = P.parens     lexer
+-- resOp = P.reservedOp lexer
+
+
+highlt :: (Html -> Html) -> Parser Html
+highlt hglt =
+    parEOF
+    <|>	do{ str  <- ((try (parsBotRefRestriction hglt)) <|> (parAnything hglt));
+--	    traceM "highlt: from braced entry";
+--	    traceState;
+--	    traceM "enter highlt ...";
+--	    traceState;
+	    str' <- highlt hglt;
+--	    traceM "exit highlt ...";
+--	    traceState;
+	    return (str+++str')
+--	     return str
+	  }
+    <|> try (do{ str  <- keyword;
+--		 traceM  "highlt: read keyword";
+--		 traceState;
+		 str' <- highlt hglt;
+--		 traceState;
+		 return ((hglt << (toHtml str)) +++ str')
+	      })
+    <|> do{ str  <- anythingElse;
+--	    traceM "highlt: from anythingElse";
+--	    traceState;
+	    str' <- highlt hglt;
+	    return (str+++str')
+	  }
+
+tillEndOfBrace hglt =
+    do{ char ')';
+	return (toHtml "")
+      }
+    <|>	do{ str  <- ((try (parsBotRefRestriction hglt)) <|> (parAnything hglt));
+--	    traceM "tillEndOfBrace: braced entry";
+--	    traceState;
+	    str' <- tillEndOfBrace hglt;
+	    return (str+++str')
+--	     return str
+	  }
+    <|> try (do{ str  <- keyword;
+--		 traceM "tillEndOfBrace: read keyword";
+--		 traceState;
+		 str' <- tillEndOfBrace hglt;
+		 return ((hglt << (toHtml str)) +++ str')
+	       })
+    <|> do{ str  <- anythingElse;
+--	    traceM "tillEndOfBrace anythingElse";
+--	    traceState;
+	    str' <- tillEndOfBrace hglt;
+	    return (str+++str')
+	  }
+    
+parEOF :: Parser Html
+parEOF = do{ eof;
+	    return (toHtml "")
+	   }
+
+
+strEOF :: Parser String
+strEOF = do{ eof;
+	     return ""
+	   }
+
+
+parAnything :: (Html -> Html) -> Parser Html
+parAnything hglt =
+    do{ char '(';
+        str <- tillEndOfBrace hglt;
+--	traceState;
+	return ("("+++str+++")")
+      }
+
+
+parsBotRefRestriction :: (Html -> Html) -> Parser Html
+parsBotRefRestriction hglt =
+    do{ restrict <-  do { char '(';
+--			  traceState;
+			  char '(';
+			  s1 <-  tillEndOfBrace hglt;
+--			  traceState;
+		          spaces;
+			  string "<=>";
+                          spaces;
+--			  traceState;
+			  char '(';
+			  s2 <- tillEndOfBrace hglt;
+--			  traceState;
+			  char ')';
+--			  traceM "read highlight restriction.";
+--		          traceState;
+			  return (if (showHtml s1) == (showHtml s2) then noHtml else("("+++s1+++")"+++" <=> "+++"("+++s2+++")"))
+			};
+	ret <- if isNoHtml restrict then removeAnds else (return (toHtml "("+++restrict+++")"));
+	return (hglt << ret)
+      }
+
+removeAnds :: Parser Html
+removeAnds = do spaces
+                try (string "&&")
+                spaces
+                return noHtml
+
+brace = (lookAhead (string "(")) <|> (lookAhead (string ")"))
+  
+anythingElse :: Parser Html
+anythingElse =
+    do{ str <- manyTill anyChar (brace <|> (try keywordCheck) <|> strEOF);
+--	traceM "read anythingElse";
+--	traceState;
+	return (toHtml str)
+      }
+
+keywordCheck = (lookAhead (string "total")) <|> (lookAhead (string "bottom-reflecting"))
+keyword = (try (string "total")) <|> (string "bottom-reflecting")
+	
+	
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs
@@ -0,0 +1,23 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.M (M,runM,newLab,abort,track) where
+
+type State = (Int,[String])
+
+data M a = M (State -> [(a,State)])
+
+instance Monad M where
+    return a = M (\s -> [(a,s)])
+    M m >>= k = M (\s -> concatMap (\(a,s') -> case k a of M l -> l s') (m s))
+
+runM :: M a -> Maybe (a, [String])
+runM (M m) = case m (1,[]) of
+	       []        -> Nothing
+	       ((a,(_,ls)):_) -> Just (a,reverse ls)
+
+newLab :: M Int
+newLab = M(\(i,ls) -> [(i,(i+1,ls))])
+
+abort :: M a
+abort = M (\s -> [])
+
+track :: String -> M ()
+track l = M (\(i,ls) -> [((),(i,l:ls))])
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs
@@ -0,0 +1,365 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag) where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+
+import Control.Monad.Identity
+import Data.List ( nub )
+
+import Text.Parsec
+import Text.Parsec.Expr
+import Text.Parsec.String(Parser)
+import Text.Parsec.Combinator
+import Text.Parsec.Token as P
+import Text.Parsec.Language(emptyDef)
+import Text.ParserCombinators.Parsec.Prim(getParserState)
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug
+
+-- | ParseCont keeps track of all currently available term and type variable during parsing a term
+data ParseCont = ParseCont { pcTVar :: [String], pcVar :: [String] } deriving (Show, Eq)
+
+emptyParseCont = ParseCont [] []
+
+-- * debug functions, are set to a function defined in Debug, (un)comment the definitions as necessary for debug
+
+--trace1 = trace_toShell
+trace1 = trace_ignore
+--traceM = traceM_toShell
+traceM = traceM_ignore
+--traceM1 = traceM_toShell
+traceM1 = traceM_ignore
+--traceState = do state <- getParserState;
+--                traceM ("with the Parser state " ++ show (stateInput state) ++ "\n");
+traceState = return ()
+
+-- * auxiliar functions
+insertTVarPC (ParseCont tv v) str =
+    if elem str tv
+    then ParseCont tv v
+    else ParseCont (str:tv) (filter (\x->x /= str) v)
+
+checkOrInsertTVarState (ParseCont tv v) str =
+    if elem str tv
+    then return ()
+    else modifyState (str:)
+
+-- checkTVarPC (ParseCont tv v) str =
+--     if elem str tv
+--     then return ()
+--     else parserZero <?> "unbound type variable"
+
+insertVarPC (ParseCont tv v) str =
+    if elem str v
+    then ParseCont tv v
+    else ParseCont (filter (\x->x /= str) tv) (str:v)
+
+checkVarPC (ParseCont tv v) str =
+    if elem str v
+    then return ()
+    else parserZero <?> "unbound term variable"
+
+myLanguage = 
+    emptyDef
+    { identStart      = letter
+    , identLetter     = alphaNum <|> oneOf "'"
+    , opStart         = oneOf ":\\-+="
+    , opLetter        = oneOf ":\\->+=_"
+    , reservedOpNames = [":","::","=","->","\\","/\\","_","+"]
+    , reservedNames   = ["forall","Int", "Bool", "if", "then", "else", "True", "False", "case","of","let!","in","fix","let","seq","undefined"]
+    , caseSensitive   = True
+    }
+
+lexer = P.makeTokenParser myLanguage
+
+int      = P.integer    lexer
+res      = P.reserved   lexer
+resOp    = P.reservedOp lexer
+whiteSpc = P.whiteSpace lexer
+lexe     = P.lexeme     lexer
+par      = P.parens     lexer
+brack    = P.brackets   lexer
+symb     = P.symbol     lexer
+ident    = P.identifier lexer
+brace    = P.braces     lexer
+nat      = P.natural    lexer
+
+
+type MyState = [String]
+
+
+termParser :: ParseCont -> ParsecT String MyState Identity Term
+termParser pc = do
+  whiteSpc
+  x <- (term1 pc)
+  eof
+  return x
+
+term1 :: ParseCont -> ParsecT String MyState Identity Term
+term1 pc = do
+    do{ traceM "Enter term1\n";
+        traceState;
+         do{ resOp "\\";
+	     str <- ident;
+	     resOp "::";
+	     tau <- typ pc;
+	     symb ".";
+	     t   <- term1 (insertVarPC pc str);
+	     return (Abs (TermVar str) tau t)
+	   }
+     <|> do{ resOp "/\\";
+	     str <- ident;
+	     symb ".";
+	     traceM1 ("scanned /\\ " ++ str ++ ".\n");
+	     t <- (term1 (insertTVarPC pc str));
+	     return (TAbs (TypVar str) t)
+	   }
+     <|> do{ res "case";
+	     t <- (term1 pc);
+	     res "of";
+	     symb "{";
+	     (do{ symb "[";
+		  symb "]";
+		  resOp "->";
+		  t1 <- (term1 pc);
+		  resOp ";";
+		  v1 <- ident;
+		  resOp ":";
+		  v2 <- ident;
+		  resOp "->";
+		  t2 <- term1 (insertVarPC (insertVarPC pc v1) v2);
+		  symb "}";
+		  return (LCase t t1 (TermVar v1) (TermVar v2) t2)
+		}
+	      <|> do{ res "True";
+		      resOp "->";
+		      t1 <- term1 pc;
+		      resOp ";";
+		      res "False";
+		      resOp "->";
+		      t2 <- term1 pc;
+		      symb "}";
+		      return (BCase t t1 t2)
+		    }
+	      <|> do{ res "False";
+		      resOp "->";
+		      t1 <- term1 pc;
+		      resOp ";";
+		      res "True";
+		      resOp "->";
+		      t2 <- term1 pc;
+		      symb "}";
+		      return (BCase t t2 t1)
+		    })
+	   }
+    <|> ifParser pc
+    <|> do{ res "let!";
+	    v <- ident;
+	    let pc' = insertVarPC pc v in
+	    do{ resOp "=";
+		t <- (term1 pc');
+		res "in";
+		t' <- (term1 pc');
+		return (LSeq (TermVar v) t t')
+	      }
+	  }
+    <|> do{ res "let";
+	    v <- ident;
+	    let pc' = insertVarPC pc v in
+	    do{ resOp "=";
+		t <- (term1 pc');
+		res "in";
+		t' <- (term1 pc');
+		return (Let (TermVar v) t t')
+	      }
+	  }
+    <|> term2 pc
+      }
+
+ifParser :: ParseCont -> ParsecT String MyState Identity Term
+ifParser pc = do
+  res "if"
+  t <- term1 pc
+  res "then"
+  t1 <- term1 pc
+  res "else"
+  t2 <- term1 pc
+  return (BCase t t1 t2)
+
+term2 :: ParseCont -> ParsecT String MyState Identity Term
+term2 pc =
+    do{ traceM "Enter term2\n";
+        traceState;
+        l <- sepBy1 (term3 pc) (resOp ":");
+        traceState;
+        trace1 "returned from term2" 
+        return (foldr1 (\x y -> Cons x y) l)
+      }
+
+term3 :: ParseCont -> ParsecT String MyState Identity Term
+term3 pc = do{traceM "Enter term3\n";
+	      traceState;
+	      h <- (do{ i<-int; 
+			return (I (fromInteger i))
+		      } 
+	            <|> term4 pc);
+	      l <- (do{ resOp "+";
+			sepBy (term4 pc) (resOp "+")
+		      }
+		    <|> return []);
+	      trace1 "returned from term3" 
+              return (foldl1 (\x y -> Add x y) (h:l))
+	     }
+
+term4 :: ParseCont -> ParsecT String MyState Identity Term
+term4 pc =
+    do{ traceM "Enter term4\n";
+	traceState;
+     do{ t <- (term6 pc);
+	 traceM ("term4 scanned term6: " ++ show t ++ "\n");
+         args <- many (term5 pc);
+	 traceM ("term4 with args = " ++ show (length args) ++ "\n");
+	 traceM ("where the arguments are " ++ show (map ($(Var (TermVar "fake"))) args) ++ "\n");
+         let t' = ((foldl (.) id (reverse args))$t) in
+	 do{ traceM ("term4 is " ++ show t' ++ "\n");
+	     return t'
+	   }
+       }
+      }
+
+term5 pc =
+    do{traceM "Enter term5\n";
+       traceState;
+       do{ t' <- term7 pc;
+	traceM ("returned in term5 with " ++ show t' ++ "\n");
+        state <- getParserState;
+	traceM ("with the Parser state " ++ show (stateInput state) ++ "\n");
+        return (\t -> App t t')
+	 }
+      }
+
+term6 pc =
+    do{ traceM "Enter term6\n";
+	traceState;
+	do{ res "fix";
+	    t <- (term7 pc) <?> "the previous \"fix\" to be applied to an argument";
+	    return (Fix t)
+	  }
+	<|> do{ res "seq";
+		t <- (term7 pc) <?> "the previous \"seq\" to be applied to two arguments";
+		t'<- (term7 pc) <?> "the previous \"seq\" to be applied to two arguments";
+		return (Seq t t')
+	      }
+	<|> term7 pc
+      }
+	    
+
+term7 pc =
+    do{ traceM "Enter term7\n";
+	traceState;
+	t <- term8 pc;
+	do{ resOp "_";
+	    tau <- brace (typ pc);
+	    return (TApp t tau)
+	  }
+	<|> return t
+      }
+    
+term8 pc =
+    do{ traceM "Enter term8\n";
+	traceState;
+	par (term1 pc)
+     <|> do{ tl <- brack (sepBy (term1 pc) (symb ","));
+	     trace1 "scanned [t1, ..., tn], trying : ...\n" resOp "_";
+	     tau <- trace1 "scanned :, trying typ\n" (brace (typ pc));
+	     return (foldr (\x y -> Cons x y) (Nil tau) tl)
+	   } 
+     <|> do{ i <- (lexe nat);
+	     return (I (fromInteger i))
+	   }
+     <|> do{ str <- ident;
+	     traceM ("term8: identified " ++ str ++ "\n");
+	     checkVarPC pc str;
+	     traceM ("term8: Variable, checkVarPC successful\n");
+	     return (Var (TermVar str))
+	   }
+    <|> do{ res "True";
+	    return T
+	  }
+    <|> do{ res "False";
+	    return F;
+	  }
+    <|> do{ res "undefined";
+	    resOp "_" <?> "undefined has to be instantiated to a type.";
+	    tau <- brace (typ pc);
+	    return (Fix (Abs (TermVar "x") tau (Var (TermVar "x"))))
+	  } 
+    <|> do{ res "fix";
+	    parserZero <?> "the previous \"fix\" to be immediately applied to a term and not to be the argument to a function"
+	  }
+    <|> do{ res "seq";
+	    parserZero <?> "the previous \"seq\" to be immediately applied to two terms and not to be the argument to a function"
+	  }
+      }
+
+typ :: ParseCont -> ParsecT String MyState Identity Typ
+typ pc = buildExpressionParser tableTyp (typ1 pc)
+
+tableTyp = [ [op "->" (\x y -> TArrow Non x y) AssocRight] ]
+ where op s f assoc = Infix (do{ resOp s; return f} <?> "operator") assoc
+
+typ1 :: ParseCont -> ParsecT String MyState Identity Typ
+typ1 pc = 
+        do{
+        traceM "Enter typ1\n";
+	traceState;
+        par (typ pc)
+    <|> do{ symb "[";
+	    tau <- (typ pc);
+	    symb "]";
+	    return (TList tau)
+	  }
+    <|> do{ str <- ident;
+	    traceM ("identifier TypeVariable " ++ str);
+	    checkOrInsertTVarState pc str;
+	    traceM "checked TVar identifier.";
+	    return (TVar (TypVar str))
+	  }
+    <|> do{ res "Int";
+	    return TInt
+	  }
+    <|> do{ res "forall";
+	    str <- ident;
+	    resOp ".";
+	    tau <- (typ (insertTVarPC pc str));
+	    return (TAll Non (TypVar str) tau)
+	  }
+    <|> do{ res "Bool";
+	    return TBool
+	  }
+      }
+
+cTermParser = termParser emptyParseCont
+testParser = termParser (ParseCont ["a","b"] ["f","g"])
+
+addFreeTVar :: [String] -> Term -> Term
+addFreeTVar [] t = t
+addFreeTVar (x:xs) t = addFreeTVar xs (TAbs (TypVar x) t)
+
+addTVarParser :: ParseCont -> ParsecT String MyState Identity Term 
+addTVarParser pc = do
+  res <- termParser pc
+  tvars <- getState
+  return (addFreeTVar (nub tvars) res)
+
+parseTerm :: String -> Either ParseError Term
+parseTerm = runP (addTVarParser emptyParseCont) [] "user input term"
+
+-- the additional Bool is a flag to see if type abstraction is explicit (Bool = True)
+
+addTVarParserWithFlag :: ParseCont -> ParsecT String MyState Identity (Term,Bool) 
+addTVarParserWithFlag pc = do
+  res <- termParser pc
+  tvars <- getState
+  return (if tvars == [] then (res, True) else (addFreeTVar (nub tvars) res, False))
+
+parseTermWithFlag :: String -> Either ParseError (Term,Bool)
+parseTermWithFlag = runP (addTVarParserWithFlag emptyParseCont) [] "user input term"
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs
@@ -0,0 +1,129 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg
+import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon(removeTrue,getEquals,instantiateWithEpsilon)
+import Language.Haskell.FreeTheorems.Variations.PolySeq.M
+import Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen
+import Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver
+import Text.PrettyPrint(renderStyle,Style(..),Mode(..),(<+>),text)
+import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag)
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight
+import Text.XHtml hiding(text)
+
+--polySeq :: Term -> Maybe (Constraint,Typ)
+polySeq =  runM.algPolySeq
+
+shellStyle = Style PageMode 80 0.2
+webStyle = Style PageMode 80 0.2
+
+--getItT :: Term -> IO()
+getItT t = 
+    case polySeq t of
+      Just ((t',c,tau),_) -> do{ putStr "The term: ";
+				 putStr (renderStyle shellStyle (prettyMarkedTerm t'));
+				 putStr "\n\nThe Constraint: ";
+				 putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
+				 putStr "\n\nWith the equations: ";
+				 putStr (show (getEquals c));
+				 putStr "\n\nThe Type:";
+				 putStr (renderStyle shellStyle (prettyMarkedTyp tau));
+				 putStr "\n\nUsed Label Variables: ";
+				 putStr "\n\n newSimplify:\n\n";
+				 let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
+				 do{putStr "The term: ";
+				    putStr (renderStyle shellStyle (prettyMarkedTerm ts));
+				    putStr "\n\nThe Constraint: ";
+				    putStr (renderStyle shellStyle (prettyConstraint cs));
+				    putStr "\n\nThe Type:";
+				    putStr (renderStyle shellStyle (prettyMarkedTyp taus));
+				    putStr "\n\nWhich optimal would be:";
+				    putStr (show (getOpt True taus));
+				    putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
+				    putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n"++y) ""
+					    (makeTypes taus ((filterTyp taus).solveConstraint$cs)));
+				    putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
+				    putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n\n"++y) ""
+					    (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
+				   };
+				 putStr "\n\n";
+			    }
+      Nothing            -> putStr "Term is not typable at all.\n"
+
+--getItTRaw :: Term -> IO()
+getItTRaw t = 
+    case polySeq t of
+      Just ((t',c,tau),_) -> do{ putStr "The term: ";
+				 putStr (renderStyle shellStyle (prettyMarkedTerm t'));
+				 putStr "\n\nThe Constraint: ";
+				 putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
+				 putStr "\n\nWith the equations: ";
+				 putStr (show (getEquals c));
+				 putStr "\n\nThe Type:";
+				 putStr (renderStyle shellStyle (prettyMarkedTyp tau));
+				 putStr "\n\nUsed Label Variables: ";
+				 putStr "\n\n newSimplify:\n\n";
+				 let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
+				 do{putStr "The term: ";
+				    putStr (renderStyle shellStyle (prettyMarkedTerm ts));
+				    putStr "\n\nThe Constraint: ";
+				    putStr (renderStyle shellStyle (prettyConstraint cs));
+				    putStr "\n\nThe Type:";
+				    putStr (renderStyle shellStyle (prettyMarkedTyp taus));
+				    putStr "\n\nWhich optimal would be:";
+				    putStr (show (getOpt True taus));
+				    putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
+				    putStr (foldr (\x y->(show x)++"\n\n"++y) ""
+					    (makeTypes taus ((filterTyp taus).solveConstraint$cs)));
+				    putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
+				    putStr (foldr (\x y->(show x)++"\n\n"++y) ""
+					    (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
+				   };
+				 putStr "\n\n";
+			    }
+      Nothing            -> putStr "Term is not typable at all.\n"
+
+getIt str = 
+    case parseTerm str of
+      Left err -> putStr (show err)
+      Right t  -> getItT t
+
+getItRaw str =
+    case parseTerm str of
+      Left err -> putStr (show err)
+      Right t  -> getItTRaw t
+
+
+--                    termstring         (ErrType,ErrMsg) (Term  ,Constraint,Typ   ,NormalFT, [(MinTyp,FT)])
+getForWebInterface :: String  ->  Either (String, String) (String,String,      String,String,  [(String,String)])
+getForWebInterface termstr =
+    case parseTermWithFlag termstr of
+      Left err       -> Left ("ParseError",(show err))
+      Right (t,flag) -> case polySeq t of
+                           Just ((t'',c',tau'),_) -> 
+			     let (t',tau,c)   = simplifyConstraint (t'',tau',c')
+                                 minTypes     = makeMinimalTypes tau ((filterTyp tau).solveConstraint$c)
+                                 optFT        = map (fromRight.(makeFTFullFuncWithFlag flag)) minTypes
+                                 minTypFTList = zip (map ((renderStyle webStyle).prettyMarkedTyp) minTypes) optFT
+                                 normalFT     = fromRight.(makeFTFullFuncWithFlag flag).instantiateWithEpsilon$ tau'
+                                 termStr      = renderStyle webStyle (text "t =" <+> prettyUnMarkedTerm (adjustTypAbstraction flag t'))
+                                 constStr     = renderStyle webStyle (prettyConstraint c)
+                                 tauStr       = renderStyle webStyle (prettyMarkedTyp tau)
+                             in
+			     Right (termStr, constStr, tauStr,normalFT,minTypFTList)
+                           Nothing             -> Left ("NotTypable",renderStyle webStyle (prettyUnMarkedTerm t))
+    where fromRight (Right x) = x
+
+
+
+testTerm = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs }))"
+
+test = case getForWebInterface testTerm of
+	 Left _ -> putStr "shit happened."
+         Right (t,c,tau,nft,l) -> do{ putStr "\n\nThe normal Theorem:\n\n";
+				      putStr nft;
+				      putStr "\n\nThe highlighted version:\n\n";
+				      putStr (show.highlight$nft);
+				    }
+
+foldl'' = "/\\a./\\b.\\c :: a -> b -> a.let! c' = c in fix ( \\h :: a -> [b] -> a.\\n :: a.\\ys :: [b].let c'' = c n in case ys of {[]   -> n; x:xs -> let! xs' = xs in let! x' = x in let n' = c'' x' in h n' xs' })"
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs
@@ -0,0 +1,174 @@
+-- | contains all rule systems
+module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg (algPolySeq) where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.M
+import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+
+-- * Typing algorithm
+
+polySeqTyping :: Cont -> Term -> M (Constraint,Typ)
+polySeqTyping gamma t =
+    case t of
+      Var v        -> do{ tau <- getTypVarInCont gamma v;
+			  superType tau
+			}
+      Abs v tau t' -> do{ (c1,tau2) <- polySeqTyping (addTermVar gamma (v,tau)) t';
+			  (c2,tau1) <- subType tau;
+			  lab       <- makeLabel;
+			  return (Conj c1 c2, TArrow lab tau1 tau2)
+			}
+      App t1 t2    -> do{ (c1,tau12) <- polySeqTyping gamma t1;
+			  (tau1,tau2)<- getArrowComps tau12;
+			  (c2,tau1') <- polySeqTyping gamma t2;
+			  c3         <- makeEqual tau1 tau1';
+			  return (Conj (Conj c1 c2) c3,tau2)
+			}
+      TAbs tv t'   -> do{ lv <- makeLabel;
+			  (c,tau) <- polySeqTyping (addTypVar gamma (tv,lv)) t';
+			  return (c,TAll lv tv tau)
+			}
+      TApp t' tau  -> do{ c1           <- seqable gamma tau;
+			  (c2,atau)    <- polySeqTyping gamma t';
+			  (lab,tv,tau1)<- getAllComps atau;
+			  (c3,tau3)    <- superType (substTyp tau1 tau tv);
+			  return (Conj (Conj c2 c3) (Impl (Eq lab (LVal Epsilon)) c1),tau3)
+			}
+      Nil tau      -> do{ (c,tau') <- superType tau;
+			  return (c,TList tau')
+			}
+      Cons t1 t2   -> do{ (c1,tau) <- polySeqTyping gamma t1;
+			  (c2,ltau)<- polySeqTyping gamma t2;
+			  tau'     <- getElemType ltau;
+			  c3       <- makeEqual tau tau';
+			  return (Conj (Conj c1 c2) c3,TList tau)
+			}
+      LCase t1 t2 v1 v2 t3 ->
+                      do{ (c1,ltau)<- polySeqTyping gamma t1;
+			  tau1     <- getElemType ltau;
+			  (c2,tau2)<- polySeqTyping gamma t2;
+			  (c3,tau2')<- polySeqTyping (addTermVar (addTermVar gamma (v1,tau1)) (v2,ltau)) t3;
+			  c4       <- makeEqual tau2 tau2';
+			  return (Conj (Conj (Conj c1 c2) c3) c4,tau2)
+			}
+      Fix t'       -> do{ (c1,tau)   <- polySeqTyping gamma t';
+			  (tau1,tau2)<- getArrowComps tau;
+			  c2         <- makeEqual tau1 tau2;
+			  return (Conj c1 c2,tau1)
+			}
+      LSeq v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1;
+			  c2        <- seqable gamma tau1;
+			  (c3,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2;
+			  return (Conj (Conj c1 c2) c3, tau2)
+			}
+      Let  v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1;
+			  (c2,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2;
+			  return (Conj c1 c2, tau2)
+			}
+      Seq t1 t2    -> do{ (c1,tau1) <- polySeqTyping gamma t1;
+			  c2        <- seqable gamma tau1;
+			  (c3,tau2) <- polySeqTyping gamma t2;
+			  return (Conj (Conj c1 c2) c3, tau2)
+			}
+      I _          -> return (Tru,TInt)
+      Add t1 t2    -> do{ (c1,tau1) <- polySeqTyping gamma t1;
+			  isInt tau1;
+			  (c2,tau2) <- polySeqTyping gamma t2;
+			  isInt tau2;
+			  return (Conj c1 c2,TInt)
+			}
+      T            -> return (Tru,TBool)
+      F            -> return (Tru,TBool)
+      BCase t1 t2 t3 -> do{ (_,tau1) <- polySeqTyping gamma t1; --the constraint will always be Tru
+			    isBool tau1;
+			    (c2,tau2) <- polySeqTyping gamma t2;
+			    (c3,tau3) <- polySeqTyping gamma t3;
+			    c4        <- makeEqual tau2 tau3;
+			    return (Conj (Conj c2 c3) c4,tau2)
+			  }
+
+-- * seqable check
+
+seqable :: Cont -> Typ -> M Constraint
+seqable gamma tau =
+    case tau of
+      TVar tv              -> do{ lab <- getLabTVar gamma tv;
+				  return (Eq (lab) (LVal Epsilon))
+				}
+      TArrow lab _  _    -> return (Eq lab (LVal Epsilon))
+      TAll   _   tv tau' -> seqable (addTypVar gamma (tv,LVal Epsilon)) tau'
+      TList  _           -> return Tru
+      TInt               -> return Tru
+      TBool              -> return Tru
+
+-- * typ comparison
+
+superType :: Typ -> M (Constraint,Typ)
+superType tau =
+    case tau of
+      TVar tv              -> return (Tru,tau)
+      TArrow lab tau1 tau2 -> do{ (c1,tau) <- subType tau1;
+				  (c2,tau')<- superType tau2;
+				  lab'     <- makeLabel;
+				  return (Conj (Conj c1 c2) (Leq lab' lab),TArrow lab' tau tau')
+				}
+      TAll lab tv tau      -> do{ (c,tau') <- superType tau;
+				  lab'     <- makeLabel;
+				  return (Conj c (Leq lab lab'), TAll lab' tv tau')
+				}
+      TList tau            -> do{ (c,tau') <- superType tau;
+				  return (c,TList tau')
+				}
+      TInt                 -> return (Tru,TInt)
+      TBool                -> return (Tru,TBool)
+
+subType :: Typ -> M (Constraint,Typ)
+subType tau =
+    case tau of
+      TVar tv              -> return (Tru,tau)
+      TArrow lab tau1 tau2 -> do{ (c1,tau) <- superType tau1;
+				  (c2,tau')<- subType tau2;
+				  lab'     <- makeLabel;
+				  return (Conj (Conj c1 c2) (Leq lab lab'),TArrow lab' tau tau')
+				}
+      TAll lab tv tau      -> do{ (c,tau') <- subType tau;
+				  lab'     <- makeLabel;
+				  return (Conj c (Leq lab' lab), TAll lab' tv tau')
+				}
+      TList tau            -> do{ (c,tau') <- subType tau;
+				  return (c,TList tau')
+				}
+      TInt                 -> return (Tru,TInt)
+      TBool                -> return (Tru,TBool)
+
+makeEqual :: Typ -> Typ -> M Constraint
+makeEqual tau tau' =
+    case tau of
+      TVar tv              -> if tau' == TVar tv then return Tru else abort
+      TArrow lab tau1 tau2 -> case tau' of
+                                TArrow lab' tau1' tau2' -> do{ c1 <- makeEqual tau1 tau1';
+							       c2 <- makeEqual tau2 tau2';
+							       return (Conj (Conj c1 c2) (Eq lab lab'))
+							     }
+                                _                       -> abort
+      TAll lab tv tau1     -> case tau' of
+                                TAll lab' tv' tau1' -> if tv == tv'
+						       then
+						         do{ c <- makeEqual tau1 tau1';
+							     return (Conj c (Eq lab lab'))
+							   }
+						       else abort
+				_                   -> abort
+      TList tau1           -> case tau' of
+                                TList tau1' -> makeEqual tau1 tau1'
+				_           -> abort
+      TInt                 -> if tau' == TInt  then return Tru else abort
+      TBool                -> if tau' == TBool then return Tru else abort
+
+-- * main function
+
+algPolySeq :: Term -> M (Term,Constraint,Typ)
+algPolySeq t = do{ t'      <- annotate t;
+		   (c,tau) <- polySeqTyping emptyCont t';
+		   return (t',c,tau)
+		 }
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs
@@ -0,0 +1,83 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint (prettyMarkedTyp, prettyUnMarkedTyp, prettyMarkedTerm, prettyUnMarkedTerm, prettyConstraint, prettyLabel, adjustTypAbstraction) where
+
+import Text.PrettyPrint
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+
+prettyLabel :: Label -> Doc
+prettyLabel l =
+    case l of
+      LVar (LabVar i) -> text ("v" ++ show i)
+      LVal Nbr        -> text "o"
+      LVal Epsilon    -> text "e"
+      Non             -> text "?"
+
+
+prettyMarkedTyp   = prettyTyp True
+prettyUnMarkedTyp = prettyTyp False
+
+prettyTyp :: Bool -> Typ -> Doc
+prettyTyp mark tau =
+    case tau of
+      TVar (TypVar s)          -> text s
+      TArrow l tau1 tau2       -> parens (fsep [prettyTyp mark tau1, if mark && l /= LVal Epsilon then text "->^" <> prettyLabel l else text "->",
+						(prettyTyp mark tau2)])
+      TAll   l (TypVar s) tau' -> parens (fsep [text "forall" <> if mark && l /= LVal Epsilon then text "^" <> (prettyLabel l) else empty,
+						text s <> text ".", prettyTyp mark tau'])
+      TList tau'               -> brackets (prettyTyp mark tau')
+      TInt                     -> text "Int"
+      TBool                    -> text "Bool"
+
+
+prettyMarkedTerm   = prettyTerm True
+prettyUnMarkedTerm = prettyTerm False
+
+adjustTypAbstraction :: Bool -> Term -> Term
+adjustTypAbstraction True t = t
+adjustTypAbstraction _    t = 
+    case t of
+      TAbs _ t' -> adjustTypAbstraction False t'
+      _         -> t
+
+prettyTerm :: Bool -> Term -> Doc
+prettyTerm mark t =
+    case t of
+      Var (TermVar s)        -> text s
+      Abs (TermVar s) tau t' -> parens (fsep [text ("\\" ++ s ++ "::") <> prettyTyp mark tau <> text ".",
+					      prettyTerm mark t'])
+      App t1 t2              -> parens (fsep [prettyTerm mark t1,prettyTerm mark t2])
+      TAbs (TypVar s) t'     -> parens (fsep [text ("/\\" ++ s ++ "."),prettyTerm mark t'])
+      TApp t' tau            -> prettyTerm mark t' <> text "_" <> braces (prettyTyp mark tau)
+      Nil tau                -> text "[]_" <> braces (prettyTyp mark tau)
+      Cons t1 t2             -> parens (prettyTerm mark t1 <> text ":" <> prettyTerm mark t2)
+      LCase t1 t2 (TermVar s1) (TermVar s2) t3 
+	                     -> parens (fsep [text "case" <+> prettyTerm mark t1<+> text "of {[] ->",
+					      prettyTerm mark t2 <> semi, text (s1 ++ ":" ++ s2 ++ " ->"),
+					      prettyTerm mark t3 <> text "}"])
+      Fix t'                 -> case t' of
+			          Abs x tau (Var y) -> if x == y 
+						       then text "undefined_" <> braces (prettyTyp mark tau)
+						       else parens (text "fix" <+> prettyTerm mark t')
+                                  _                 -> parens (text "fix" <+> prettyTerm mark t')
+      LSeq (TermVar s) t1 t2 -> parens (fsep [text "let!", text s, equals, prettyTerm mark t1, text "in",
+					      prettyTerm mark t2])
+      Let  (TermVar s) t1 t2 -> parens (fsep [text "let", text s, equals, prettyTerm mark t1,
+					      text "in",prettyTerm mark t2])
+      Seq t1 t2              -> parens (text "seq" <+> prettyTerm mark t1 <+> prettyTerm mark t2)
+      I i                    -> text (show i)
+      Add t1 t2              -> parens (fsep [prettyTerm mark t1, text "+", prettyTerm mark t2])
+      T                      -> text "True"
+      F                      -> text "False"
+      BCase t1 t2 t3         -> parens (fsep [text "if", prettyTerm mark t1, text "then", prettyTerm mark t2,
+					      text "else", prettyTerm mark t3])
+
+
+prettyConstraint :: Constraint -> Doc
+prettyConstraint c =
+    case c of
+      Conj c1 c2 -> fsep [prettyConstraint c1, text " ^ ", prettyConstraint c2]
+      Impl c1 c2 -> parens (fsep [prettyConstraint c1, text " -> ", prettyConstraint c2])
+      Leq  l1 l2 -> parens (fsep [prettyLabel l1, text " <= ", prettyLabel l2])
+      Eq   l1 l2 -> parens (fsep [prettyLabel l1, text " == ", prettyLabel l2])
+      Tru        -> text "T"
+      Fls        -> text "F"
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Syntax.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Syntax.hs
@@ -0,0 +1,68 @@
+{-# OPTIONS_GHC -XTypeOperators -XRank2Types #-}
+{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, DeriveDataTypeable #-} 
+module Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax where
+
+import Data.Generics(Typeable,Data)
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug
+
+
+-- *Data type declarations
+newtype LabVar = LabVar Int deriving (Show, Eq, Typeable, Data)
+
+data LabVal 
+    = Nbr
+    | Epsilon
+    deriving(Show, Eq, Ord, Typeable, Data)  
+
+data Label  
+    = LVar LabVar
+    | LVal LabVal
+    | Non
+    deriving(Show, Eq, Typeable, Data)
+
+newtype TypVar = TypVar String deriving (Show, Eq, Typeable, Data)
+
+data Typ    = TVar      TypVar
+            | TArrow    Label  Typ    Typ
+            | TAll      Label  TypVar Typ
+            | TList     Typ
+            | TInt
+	    | TBool
+            deriving (Show, Eq, Typeable, Data)
+
+newtype TermVar = TermVar String deriving (Show, Eq, Ord, Typeable, Data)
+
+-- |abbreviation for the pair (TermVar,Typ)
+type TypedVar = (TermVar,Typ)
+
+-- |Syntax of the terms used in the algorithm.
+data Term 
+    = Var TermVar   
+    | Abs    TermVar Typ     Term
+    | App    Term    Term
+    | TAbs   TypVar  Term
+    | TApp   Term    Typ
+    | Nil    Typ
+    | Cons   Term    Term 
+    | LCase  Term    Term TermVar TermVar Term
+    | Fix    Term
+    | LSeq   TermVar Term Term
+    | Let    TermVar Term Term
+    | Seq    Term    Term
+    | I      Int
+    | Add    Term    Term
+    | T
+    | F
+    | BCase  Term    Term Term     
+    deriving (Show, Eq, Typeable, Data)
+
+
+data Constraint 
+    = Conj Constraint Constraint
+    | Impl Constraint Constraint
+    | Leq  Label      Label
+    | Eq   Label      Label
+    | Tru
+    | Fls
+    deriving(Show, Eq, Typeable, Data)
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs
@@ -0,0 +1,74 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc, makeFTFullWithFlag, makeFTFullFuncWithFlag) where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator(translate)
+
+import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
+import Language.Haskell.FreeTheorems
+	( runChecks
+	, check
+	, prettyTheorem
+        , asTheorem
+	, asCompleteTheorem
+	, interpret
+	, unfoldLifts
+	, prettyUnfoldedLift
+	, LanguageSubset(SubsetWithSeq)
+        , TheoremType(EquationalTheorem)
+	, PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets)
+        , specialise
+        , relationVariables
+	)
+
+import Language.Haskell.FreeTheorems.BasicSyntax(Signature(..),Identifier(..))
+import Language.Haskell.FreeTheorems.ValidSyntax(ValidSignature(..))
+import Text.PrettyPrint.HughesPJ (render)
+
+
+--makeFTFull :: Typ -> Either String String
+makeFTFull = makeFTFullWithFlag True
+
+--makeFTFullWithFlag :: Typ -> Either String String
+makeFTFullWithFlag flag tau =
+    let sig         = ValidSignature (Signature (Ident "t") (translate tau))
+        bool        = "data Bool = False | True"
+        parse_input = unlines [bool]
+	(ds,es)     = runChecks (parse parse_input >>= check)
+	thmopts     = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations]
+    in if null es
+       then case interpret ds (SubsetWithSeq  EquationalTheorem) sig of
+              Nothing -> Left "interpret returned nothing"
+	      Just i  -> let i' = foldl specialise i (relationVariables i) in
+                         Right $ render (prettyTheorem thmopts (asCompleteTheorem i)) ++
+			   case unfoldLifts ds i of
+			   [] -> ""
+			   ls -> (if length ls == 1 
+			          then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
+				  else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
+				       unlines (map (render . prettyUnfoldedLift thmopts) ls)
+       else Left (unlines (map render es))
+
+
+
+--makeFTFullFuncWithFlag :: Typ -> Either String String
+makeFTFullFunc = makeFTFullFuncWithFlag True
+
+--makeFTFullFunc :: Bool -> Typ -> Either String String
+makeFTFullFuncWithFlag flag tau =
+    let sig         = ValidSignature (Signature (Ident "t") (translate tau))
+        bool        = "data Bool = False | True"
+        parse_input = unlines [bool]
+	(ds,es)     = runChecks (parse parse_input >>= check)
+	thmopts     = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations]
+    in if null es
+       then case interpret ds (SubsetWithSeq  EquationalTheorem) sig of
+              Nothing -> Left "interpret returned nothing"
+	      Just i  -> let i' = foldl specialise i (relationVariables i) in
+                         Right $ render (prettyTheorem thmopts (asCompleteTheorem i')) ++
+			   case unfoldLifts ds i' of
+			   [] -> ""
+			   ls -> (if length ls == 1 
+			          then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
+				  else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
+				       unlines (map (render . prettyUnfoldedLift thmopts) ls)
+       else Left (unlines (map render es))
+
diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs
@@ -0,0 +1,26 @@
+module Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+    ( Typ(..)
+    , Label(..)
+    , LabVal(..)
+    , TypVar(..)
+    )
+import Language.Haskell.FreeTheorems.Syntax
+    ( TypeExpression(..)
+    , Identifier(..)
+    , TypeVariable(..)
+    , TypeConstructor(..)
+    )
+
+translate :: Typ -> TypeExpression
+translate tau =
+    case tau of
+      TVar   (TypVar s)                      -> TypeVar    (TV (Ident s))
+      TArrow (LVal Epsilon) tau1       tau2  -> TypeFun    (translate tau1)  (translate tau2)
+      TArrow (LVal Nbr    ) tau1       tau2  -> TypeFunLab (translate tau1)  (translate tau2)
+      TAll   (LVal Epsilon) (TypVar s) tau1  -> TypeAbs    (TV (Ident s)) [] (translate tau1)
+      TAll   (LVal Nbr    ) (TypVar s) tau1  -> TypeAbsLab (TV (Ident s)) [] (translate tau1)
+      TList  tau1                            -> TypeCon    ConList           [translate tau1]
+      TInt                                   -> TypeCon    ConInt               []
+      TBool                                  -> TypeCon    (Con (Ident "Bool")) []
diff --git a/src/Tests.hs b/src/Tests.hs
new file mode 100644
--- /dev/null
+++ b/src/Tests.hs
@@ -0,0 +1,24 @@
+-- | contains terms and other useful things, imports PolySeq
+module Tests where
+
+import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq
+import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax
+
+term1 = TAbs (TypVar "a")
+	 (Abs (TermVar "x") (TArrow Non (TArrow Non (TVar (TypVar "a")) TInt) TInt)
+           (Abs (TermVar "y") (TArrow Non (TVar (TypVar "a")) TInt)
+	      (App (Var (TermVar "x")) (Var (TermVar "y")))))
+
+testInput1 = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs}))"
+
+testInput2 = "\\f::((Int->Int)->Int)->Int.\\g::(Int->Int)->Int.\\c::Int->Int. f g + g c + (f (\\h::Int->Int.let! h' = h in 3))"
+testTyp1 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))
+
+testTyp2 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))
+
+testTyp3 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))
+
+testTyp4 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Nbr) (TVar (TypVar "a")) TBool) (TArrow (LVal Nbr) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))
+
+
+testTerm = "/\\a.\\p::a->Bool.p:[]_{a->Bool}"