diff --git a/Compressor.hs b/Compressor.hs
new file mode 100644
--- /dev/null
+++ b/Compressor.hs
@@ -0,0 +1,80 @@
+{-# language DoAndIfThenElse #-}
+
+import TPDB.Compress (compress)
+import TPDB.DP ( dp, Marked (Auxiliary) )
+import TPDB.Data
+import TPDB.XTC.Read ( readProblems )
+import TPDB.Plain.Write ( )
+import TPDB.Pretty ( pretty )
+import Text.PrettyPrint.HughesPJ 
+  ( text, ($$), nest, vcat )
+
+import System.Environment
+import System.IO
+import System.Directory
+import Control.Monad ( guard, forM )
+import Data.List ( isSuffixOf, isPrefixOf )
+import qualified Data.Set as S
+
+-- | give file/dir name(s) on cmd line.
+-- recursively collect all *.xml files,
+-- and apply TRS compression.
+
+main = do
+    hSetBuffering stdout LineBuffering 
+    args <- getArgs
+    ss <- collect args
+    putStrLn "action"
+    forM ( map dp ss ) $ \ s -> do
+        print $ text "original TRS" </> pretty s 
+        let ( com, rules ) = compress supply s
+        print $ text "compressed TRS" </> vcat
+            ( pretty com : map pretty rules )
+        print $ judge s
+
+p </> q = p $$ nest 4 q
+
+judge sys = 
+    let csys = compress supply sys
+    in  ( cost_trs sys , cost_comp csys )
+
+supply = do 
+    i <- [ 0 .. ] 
+    return $ Auxiliary $ mknullary $ "c" ++ show i
+
+cost_comp ( s, sub ) = 
+    cost_trs s + cost_sub sub
+    
+cost_sub sub = sum $ do
+    ((f, af), Just (g, k, h, ca)) <- sub
+    return ca
+
+cost_trs s = sum $ do
+    u <- rules s
+    t <- [ lhs u, rhs u ]
+    return $ cost_term t
+
+cost_term t = sum $ do 
+    (p,s) <- positions t 
+    return $ multiplications s
+
+multiplications t = case t of
+    Node f xs -> sum $ do
+        x @ Node {} <- xs
+        return $ S.size $ vars x
+    _ -> 0    
+
+collect fs = do
+    let special d = isPrefixOf "." d
+    fss <- forM fs $ \ f -> do
+        d <- doesDirectoryExist f
+        if d 
+        then do
+           fs <- getDirectoryContents f
+           collect $ map ( ( f ++ "/" ) ++ )
+                   $ filter (not . special) fs
+        else if isSuffixOf ".xml" f
+             then fmap (map trs) $ readProblems f
+             else return []
+    return $ concat fss
+
diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
--- a/TPDB/CPF/Proof/Type.hs
+++ b/TPDB/CPF/Proof/Type.hs
@@ -19,9 +19,17 @@
 
 data CertificationProblem =
      CertificationProblem { input :: CertificationProblemInput 
-                          , proof :: Proof }  
+                          , cpfVersion :: String -- urgh
+                          , proof :: Proof 
+                          , origin :: Origin  
+                          }  
    deriving ( Typeable )
 
+data Origin = ProofOrigin Tool 
+    deriving Typeable
+data Tool = Tool { name :: String , version :: String } 
+    deriving Typeable
+
 data CertificationProblemInput 
     = TrsInput { trsinput_trs :: TRS Identifier Identifier }
       -- ^ this is actually not true, since instead of copying from XTC,
@@ -42,12 +50,10 @@
 
 data TrsTerminationProof 
      = RIsEmpty
-{-
-     | RuleRemoval { orderingConstraintProof :: OrderingConstraintProof
+     | RuleRemoval { rr_orderingConstraintProof :: OrderingConstraintProof
                    , trs :: TRS Identifier Identifier 
                    , trsTerminationProof :: TrsTerminationProof  
                    }  
--}
      | DpTrans  { dptrans_dps :: DPS
                 , markedSymbols :: Bool , dptrans_dpProof :: DpProof }
      | StringReversal { trs :: TRS Identifier Identifier
@@ -56,7 +62,7 @@
    deriving ( Typeable )
        
 data DpProof = PIsEmpty  
-     | RedPairProc { orderingConstraintProof :: OrderingConstraintProof
+     | RedPairProc { dp_orderingConstraintProof :: OrderingConstraintProof
                    , red_pair_dps :: DPS , redpairproc_dpProof :: DpProof }  
    deriving ( Typeable )
 
@@ -77,6 +83,9 @@
    deriving ( Typeable )
 
 data Domain = Naturals 
+            | Rationals Rational
+            | Arctic Domain
+            | Tropical Domain
    deriving ( Typeable )
 
 data Interpret = forall s .  XmlContent s => Interpret 
@@ -89,6 +98,7 @@
 data Polynomial = Sum [ Polynomial ]
                 | Product [ Polynomial ]
                 | Polynomial_Coefficient Coefficient
+                | Polynomial_Variable String
    deriving ( Typeable )
 
 data Coefficient = Vector [ Coefficient ]
@@ -96,10 +106,8 @@
            | forall a . XmlContent a => Coefficient_Coefficient a
    deriving ( Typeable )
 
-
-
-
-
-
+data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
+   deriving Typeable
 
+class ToExotic a where toExotic :: a -> Exotic
 
diff --git a/TPDB/CPF/Proof/Xml.hs b/TPDB/CPF/Proof/Xml.hs
--- a/TPDB/CPF/Proof/Xml.hs
+++ b/TPDB/CPF/Proof/Xml.hs
@@ -25,6 +25,7 @@
 import qualified Data.Time as T
 import Control.Monad
 import Data.Typeable
+import Data.Ratio
 
 tox :: CertificationProblem -> Document ()
 tox p = 
@@ -36,9 +37,21 @@
 instance XmlContent CertificationProblem where
    toContents cp = rmkel "certificationProblem"
          [ mkel "input" $ toContents ( input cp )
+         , mkel "cpfVersion" [ CString False ( cpfVersion cp ) () ]
          , mkel "proof" $ toContents ( proof cp )
+         , mkel "origin" $ toContents ( origin cp )
          ]
 
+instance XmlContent Origin where
+   toContents o = case o of
+       ProofOrigin t -> rmkel "proofOrigin" $ toContents t
+
+instance XmlContent Tool where
+   toContents t = rmkel "tool" 
+         [ mkel "name" [ CString False ( name t ) () ]
+         , mkel "version" [ CString False ( version t ) () ]
+         ]
+
 instance XmlContent CertificationProblemInput where
    toContents i = case i of
       TrsInput {} -> rmkel "trsInput" $ toContents ( trsinput_trs i )
@@ -65,7 +78,8 @@
        Sharp q -> rmkel "sharp" $ toContents  q
 
 instance XmlContent DPS where
-   toContents ( DPS rules ) = rmkel "dps" $ concat $ map toContents rules
+   toContents ( DPS rules ) = rmkel "dps" 
+        $ rmkel "rules" $ rules >>= toContents
 
 instance XmlContent TrsTerminationProof where
    toContents p = rmkel "trsTerminationProof" $ case p of
@@ -73,12 +87,19 @@
              toContents ( dptrans_dps p )
           ++ rmkel "markedSymbols" [ CString False "true" () ]
           ++ toContents ( dptrans_dpProof p )
+      StringReversal {} -> rmkel "stringReversal" $
+             ( toContents $ trs p )
+          ++ ( toContents $ trsTerminationProof p )
+      RuleRemoval {} -> rmkel "ruleRemoval"
+          $  toContents ( rr_orderingConstraintProof p )
+          ++ toContents ( trs p )
+          ++ toContents ( trsTerminationProof p )
 
 instance XmlContent DpProof where
    toContents p = rmkel "dpProof" $ case p of
        PIsEmpty -> rmkel "pIsEmpty" []
        RedPairProc {} ->  rmkel "redPairProc" 
-         $ toContents ( orderingConstraintProof p )
+         $ toContents ( dp_orderingConstraintProof p )
         ++ toContents ( red_pair_dps p )
         ++ toContents ( redpairproc_dpProof p )
 
@@ -102,11 +123,21 @@
 instance XmlContent Domain where
    toContents d = rmkel "domain" $ case d of
        Naturals -> rmkel "naturals" []
+       Rationals delta -> rmkel "rationals" 
+         $ rmkel "delta" $ toContents delta
+       Arctic d -> rmkel "arctic" $ toContents d
+       Tropical d -> rmkel  "tropical" $ toContents d
 
+instance XmlContent Rational where
+    toContents r = rmkel "rational" 
+        [ mkel "numerator" [ CString False ( show $ numerator r ) () ]
+        , mkel "denominator" [ CString False ( show $ denominator r ) () ]
+        ]
+
 instance XmlContent Interpret  where
    toContents i = rmkel "interpret" $ case i of
        Interpret { symbol = s } -> 
-           toContents s
+           sharp_name_HACK ( toContents s )
         ++ rmkel "arity" [ CString False ( show ( arity i )) () ]
         ++ toContents ( value i )
 
@@ -119,7 +150,9 @@
        Sum     ps -> rmkel "sum"     $ concat ( map toContents ps )
        Product ps -> rmkel "product" $ concat ( map toContents ps )
        Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
+       Polynomial_Variable v -> rmkel "variable" [ CString False v () ]
 
+
 instance XmlContent Coefficient where
    toContents v = case v of
        Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
@@ -127,7 +160,11 @@
        Coefficient_Coefficient i -> 
           rmkel "coefficient" $ toContents i
 
-
+instance XmlContent Exotic where
+    toContents e = case e of
+       Minus_Infinite -> rmkel "minusInfinity" []
+       E_Integer i -> rmkel "integer" [ CString False ( show i ) () ]
+       Plus_Infinite -> rmkel "plusInfinity" []
 
 
 
diff --git a/TPDB/Compress.hs b/TPDB/Compress.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Compress.hs
@@ -0,0 +1,179 @@
+{-# language TemplateHaskell #-}
+
+module TPDB.Compress where
+
+import TPDB.Data hiding ( trs, arity )
+import TPDB.Plain.Write ()
+import qualified TPDB.Plain.Read (trs) -- for testing
+import TPDB.Pretty 
+
+import Control.Monad ( guard ) 
+import qualified Data.Set as S
+import qualified Data.Map.Strict as M
+import Data.List ( sortBy )
+import Data.Ord ( comparing )
+
+
+-- | compute a compressed version of the TRS.
+-- Warning: in the output, the arities of fresh identifiers will be nonsensical
+compress :: ( Ord s )
+         => [s] -- ^ supply of function symbols. This can be any infinite list,
+                -- the implementation will filter out those elements that
+                -- occur in the original TRS's signature.
+         -> TRS v s 
+         -> ( TRS v s 
+            , [ ((s, Int), Maybe (s,Int,s,Int) ) ] 
+            ) -- ^  ((f, a), Just (g,i,h,a)) semantics: new function symbols f
+              -- by substituting h in the i-th position (start at 0) of g.
+              -- arity of child is a
+              -- ((f, a), Nothing ) semantics: f of arity a is an "old" function symbol.
+              -- output is in dependency order (will only refer to previously defined symbols).
+compress pool sys = 
+    let osig = ohsig sys
+        forbidden = M.keysSet osig
+        fresh = filter ( `S.notMember` forbidden ) pool
+        con = make fresh sys
+    in  ( trs con 
+        ,    map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig )
+          ++ map ( \ (f, p) -> ( (f, arity p), Just (parent p, branch p, child p, child_arity p) ) ) 
+             (  reverse $ defs con )
+        )
+
+ohsig sys = M.fromListWith ( \ o n -> if o == n then o else error "different arities" ) 
+             $ do u <- rules sys ; t <- [ lhs u , rhs u ]
+                  ( _ , Node f args ) <- positions t
+                  return ( f, length args )
+
+dont_compress pool sys = 
+    let osig = ohsig sys
+    in ( sys , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig ) )
+                  
+
+data Pattern s = Pattern
+             { parent :: ! s
+             , branch :: ! Int
+             , child :: ! s
+             , arity :: ! Int
+             , child_arity :: ! Int
+             , has_grand_child :: ! Bool 
+             }
+    deriving ( Eq, Ord )
+
+data Container v s = Container 
+               { trs :: TRS v s
+               , defs :: [( s, Pattern s)] 
+               }
+
+make fresh trs = handle fresh $ Container trs []
+
+
+handle free con = 
+    case -- take 1 $ 
+         disjoint $ best_patterns $ trs con of
+        [] -> con
+        ps -> 
+            let ( pre, post ) 
+                    = splitAt ( length ps ) free
+                here = zip pre ps      
+            in handle post
+                 $ con { trs = apply_system here $ trs con
+                       , defs = here ++ defs con
+                       }
+
+patterns_in_term t = 
+    nonoverlapping t ++ overlapping t
+
+overlapping t = do
+    (pos, Node f xs) <- positions t
+    ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs
+    guard $ f == g
+    let sub = case ys !! k of 
+          Node h _ -> True
+          _ -> False
+    guard $ if sub then even $ length pos else True 
+    let r = not $ null $ do Node {} <- ys ; return ()
+    return $ Pattern { arity = length xs - 1 + length ys
+                     , parent = f, branch = k
+                     , child = g, child_arity = length ys
+                     , has_grand_child = r 
+                     }
+
+nonoverlapping t = do
+    Node f xs <- subterms t
+    ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs
+    guard $ f /= g
+    let r = not $ null $ do Node {} <- ys ; return ()
+    return $ Pattern { arity = length xs - 1 + length ys
+                     , parent = f, branch = k
+                     , child = g, child_arity = length ys
+                     , has_grand_child = r 
+                     }
+
+patterns_in_rule u = do
+    t <- [ lhs u, rhs u ]
+    patterns_in_term t
+
+patterns trs = do
+    u <- rules trs
+    patterns_in_rule u
+
+disjoint ps =
+   let h seen [] = []
+       h seen (p:ps) = 
+         if S.notMember (parent p) seen
+            && S.notMember (child p) seen
+         then p : h (S.insert (parent p)   
+                     $ S.insert (child p) seen) ps
+         else h seen ps     
+   in  h S.empty ps 
+
+best_patterns trs = do
+    let pns = sortBy ( comparing ( negate . snd ))
+            $  M.toList $ collect $ patterns trs
+    let threshold = case pns of          
+          [] -> 0
+          (p,n) : _ -> div n 2
+    (p,n) <- takeWhile ( \ (p,n) -> n >= threshold ) pns
+    guard $ ( n > 1 ) || ( n == 1 && has_grand_child p )
+    return p
+
+
+apply_system fgps trs = do
+    trs { rules = map ( apply_rule fgps ) $ rules trs }
+
+apply_rule fgps u = 
+    u { lhs = apply_term fgps $ lhs u
+      , rhs = apply_term fgps $ rhs u
+      }
+
+apply_term _ ( Var v ) = Var v
+apply_term fgps t @ (Node top args) = 
+    let Node newtop newargs = multi_matches fgps t
+    in  Node newtop $ map (apply_term fgps) newargs
+        
+multi_matches [] t = t
+multi_matches ((fg, p@Pattern{parent=f,branch=i,child=g}) : fgps ) t@(Node top args) = 
+    if matches p t
+    then let ( pre, Node _ sub : post) = splitAt i args 
+         in  Node fg ( pre ++ sub ++ post )    
+    else multi_matches fgps t         
+
+matches ( Pattern { parent = f, branch = i, child = g } ) 
+        ( Node top args ) | top == f = 
+    case args !! i of
+         Node bot _ | bot == g -> True
+         _ -> False
+matches p _ = False
+
+
+
+collect xs = M.fromListWith (+) $ do 
+    x <- xs 
+    return ( x, child_arity x )
+
+
+invert :: ( Ord a, Ord b )
+       => M.Map a b -> M.Map b [a]
+invert fm = M.fromListWith (++) $ do
+    ( k, v ) <- M.toList fm
+    return ( v, [k] )
diff --git a/TPDB/Convert.hs b/TPDB/Convert.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Convert.hs
@@ -0,0 +1,36 @@
+module TPDB.Convert where
+
+import TPDB.Data
+import Control.Monad ( forM, guard )
+
+srs2trs :: SRS s -> TRS Identifier s
+srs2trs s = s { separate = False
+              , rules = map convert_srs_rule $ rules s
+              }  
+
+convert_srs_rule u = 
+    let v = Identifier "x" 0 
+    in  u { lhs = unspine v $ lhs u
+          , rhs = unspine v $ rhs u        
+          } 
+                  
+trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
+trs2srs t = do
+    us <- forM ( rules t ) convert_trs_rule 
+    return $ t { separate = True , rules = us }
+
+convert_trs_rule u = do
+      ( left_spine, left_base ) <- spine $ lhs u
+      ( right_spine, right_base ) <- spine $ rhs u
+      guard $ left_base == right_base     
+      return $ u { lhs = left_spine, rhs = right_spine }
+
+unspine :: v -> [s] -> Term v s
+unspine v = foldr (  \ c t -> Node c [ t ] ) ( Var v )
+
+spine :: Term v s -> Maybe ( [s], v )
+spine t = case t of
+    Node f [ a ] -> do
+      ( sp, base ) <- spine a 
+      return ( f : sp, base )
+    Var v -> return ( [] , v ) 
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -25,12 +25,24 @@
 
 ---------------------------------------------------------------------
 
+data Relation = Strict |  Weak | Equal deriving ( Eq, Ord, Typeable, Show )
+
 data Rule a = Rule { lhs :: a, rhs :: a 
-                   , strict :: Bool
+                   , relation :: Relation
                    , top :: Bool
                    }
     deriving ( Eq, Ord, Typeable )
 
+strict :: Rule a -> Bool
+strict u = case relation u of Strict -> True ; _ -> False
+
+weak :: Rule a -> Bool
+weak u = case relation u of Weak -> True ; _ -> False
+
+equal :: Rule a -> Bool
+equal u = case relation u of Equal -> True ; _ -> False
+
+
 data RS s r = 
      RS { signature :: [ s ] -- ^ better keep order in signature (?)
          , rules :: [ Rule r ]
@@ -40,8 +52,10 @@
 
 strict_rules sys = 
     do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
-non_strict_rules sys = 
-    do u <- rules sys ; guard $ not $ strict u ; return ( lhs u, rhs u )
+weak_rules sys = 
+    do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )
+equal_rules sys = 
+    do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u )
 
 type TRS v s = RS s ( Term v s )
 
@@ -79,7 +93,7 @@
 from_strict_rules :: Bool -> [(t,t)] -> RS i t
 from_strict_rules sep rs = 
     RS { rules = map ( \ (l,r) ->
-             Rule { strict = True, top = False, lhs = l, rhs = r } ) rs
+             Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs
        , separate = sep 
        }
 
diff --git a/TPDB/Data/Xml.hs b/TPDB/Data/Xml.hs
--- a/TPDB/Data/Xml.hs
+++ b/TPDB/Data/Xml.hs
@@ -38,8 +38,14 @@
 -}
 -- for CPF:
     toContents ( Node f args ) = rmkel "funapp" 
-            $ rmkel "name" ( toContents f )
+            $ sharp_name_HACK ( toContents f )
            ++ map ( \ arg -> mkel "arg" $ toContents arg ) args
+
+
+sharp_name_HACK e = case e of
+    [ CElem ( Elem (N "sharp") [] cs ) () ] -> 
+        rmkel "sharp" $ rmkel "name" cs
+    _ -> rmkel "name" e
 
 
 
diff --git a/TPDB/Input.hs b/TPDB/Input.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Input.hs
@@ -0,0 +1,48 @@
+module TPDB.Input where
+
+import TPDB.Data
+import TPDB.Plain.Read
+import TPDB.XTC.Read
+import TPDB.Convert
+
+import System.FilePath.Posix ( splitExtension )
+
+-- | read input from file with given name.
+-- can have extension .srs, .trs, .xml.
+
+get :: FilePath 
+         -> IO ( Either (TRS Identifier Identifier) 
+                        ( SRS Identifier ) )
+get f = do
+    let ( base, ext ) = splitExtension f    
+    case ext of                     
+      ".srs" -> do
+          s <- readFile f    
+          case srs s of
+              Left err -> error err
+              Right t -> return $ Right t
+      ".trs" -> do        
+          s <- readFile f
+          case TPDB.Plain.Read.trs s of
+              Left err -> error err
+              Right t -> return $ Left t            
+      ".xml" -> do
+          ps <- readProblems f
+          case ps of 
+              [ p ] -> return $ Left $ TPDB.Data.trs p
+
+get_trs f = do
+    x <- get f
+    return $ case x of
+        Right x -> srs2trs x
+        Left  x -> x
+
+get_srs f = do
+    x <- get f
+    return $ case x of
+        Right x -> x
+        Left  x -> case trs2srs x of
+            Nothing -> error "not an SRS"
+            Just x -> x
+            
+
diff --git a/TPDB/Mirror.hs b/TPDB/Mirror.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Mirror.hs
@@ -0,0 +1,19 @@
+module TPDB.Mirror where
+
+import TPDB.Data
+import TPDB.Convert
+
+import Control.Monad ( forM, guard )
+
+-- | if input is SRS, reverse lhs and rhs of each rule
+mirror :: TRS Identifier s 
+       -> Maybe ( TRS Identifier s )
+mirror trs = do
+    us <- forM (rules trs) $ \ u -> do
+      ( left_spine, left_base ) <- spine $ lhs u
+      ( right_spine, right_base ) <- spine $ rhs u
+      guard $ left_base == right_base 
+      return $ u { lhs = unspine left_base $ reverse left_spine
+                 , rhs = unspine right_base $ reverse right_spine
+                 }
+    return $ trs { rules = us }
diff --git a/TPDB/Plain/Read.hs b/TPDB/Plain/Read.hs
--- a/TPDB/Plain/Read.hs
+++ b/TPDB/Plain/Read.hs
@@ -58,10 +58,13 @@
 instance Reader u => Reader ( Rule u ) where
     reader = do
         l <- reader
-        s <-  do reservedOp lexer "->"  ; return True
-          <|> do reservedOp lexer "->=" ; return False
+        rel <-  do reservedOp lexer "->"  ; return Strict
+          <|> do reservedOp lexer "->=" ; return Weak
+          -- FIXME: for the moment, we do not parse this
+          -- as it would deviate from published TPDB syntax
+          -- <|> do reservedOp lexer "=" ; return Equal
         r <- reader
-        return $ Rule { lhs = l, strict = s, top = False, rhs = r }
+        return $ Rule { lhs = l, relation = rel, top = False, rhs = r }
 
 data Declaration u
      = Var_Declaration [ Identifier ]
diff --git a/TPDB/Plain/Write.hs b/TPDB/Plain/Write.hs
--- a/TPDB/Plain/Write.hs
+++ b/TPDB/Plain/Write.hs
@@ -9,6 +9,8 @@
 import TPDB.Pretty
 import Text.PrettyPrint.HughesPJ
 
+import Data.List ( nub )
+
 instance Pretty Identifier where
     pretty i = text $ name i
 
@@ -21,14 +23,18 @@
 
 instance PrettyTerm a => Pretty ( Rule a ) where
     pretty u = hsep [ prettyTerm $ lhs u
-                    , if strict u then text "->" else text "->="
+                    , case relation u of 
+                         Strict -> text "->" 
+                         Weak -> text "->="
+                         Equal -> text "="
                     -- FIXME: implement "top" annotation
                     , prettyTerm $ rhs u
                     ]
 
-class PrettyTerm a where prettyTerm :: a -> Doc
+class PrettyTerm a where 
+    prettyTerm :: a -> Doc
 
-instance Pretty s => PrettyTerm [s] where
+instance Pretty s => PrettyTerm [s] where    
     prettyTerm xs = hsep $ map pretty xs
 
 instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
@@ -40,6 +46,9 @@
           vcat ( ( if separate sys then punctuate comma else id )
                  $ map pretty $ rules sys 
                )
+        -- FIXME: variables are not shown (and it is impossible to compute
+        -- them here, this is actually a TPDB format design error, 
+        -- since variables should be local (per rule), not global)
         -- FIXME: output strategy, theory
         ]
 
diff --git a/TPDB/Pretty.hs b/TPDB/Pretty.hs
--- a/TPDB/Pretty.hs
+++ b/TPDB/Pretty.hs
@@ -9,5 +9,16 @@
 instance ( Pretty a, Pretty b ) => Pretty (a,b) where
     pretty (x,y) = parens $ fsep $ punctuate comma [ pretty x, pretty y ]
 
+instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where
+    pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]
+
+instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where
+    pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]
+
 instance Pretty a => Pretty [a]  where
     pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
+
+instance Pretty a => Pretty (Maybe a) where
+    pretty m = case m of
+        Nothing -> text "Nothing"
+        Just x -> text "Just" <+> pretty x -- FIXME: parens missing
diff --git a/TPDB/Rainbow/Proof/Type.hs b/TPDB/Rainbow/Proof/Type.hs
--- a/TPDB/Rainbow/Proof/Type.hs
+++ b/TPDB/Rainbow/Proof/Type.hs
@@ -13,6 +13,8 @@
 import TPDB.Plain.Write () -- just instances
 import Text.PrettyPrint.HughesPJ
 
+import qualified TPDB.CPF.Proof.Type as C
+
 import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
 import qualified Text.Parsec as P
 
@@ -25,9 +27,12 @@
 data Matrix a = Matrix [ Vector a ]
    deriving Typeable
 
-data MaxPlus = MinusInfinite | Finite Integer
+data MaxPlus = MinusInfinite | MaxPlusFinite Integer
    deriving ( Show, Read, Typeable )
 
+data MinPlus = MinPlusFinite Integer | PlusInfinite 
+   deriving ( Show, Read, Typeable )
+
 data Mi_Fun a = 
      Mi_Fun { mi_const :: Vector a
             , mi_args :: [ Matrix a ]
@@ -43,7 +48,7 @@
 type Polynomial_Int = Interpretation Poly_Fun
 
 data Interpretation f = forall k a 
-    . ( XmlContent k, XmlContent a, Typeable a ) -- Haskell2Xml a 
+    . ( XmlContent k, XmlContent a, C.ToExotic a, Typeable a ) -- Haskell2Xml a 
      => 
      Interpretation { mi_domain :: Domain
                 , mi_dim :: Integer
@@ -153,6 +158,19 @@
 
 
 
-
+instance C.ToExotic Integer where
+  toExotic = C.E_Integer
+instance C.ToExotic MaxPlus where
+  toExotic a = case a of
+    MinusInfinite -> C.Minus_Infinite
+    MaxPlusFinite f -> C.E_Integer f
+instance C.ToExotic MinPlus where
+  toExotic a = case a of
+    MinPlusFinite f -> C.E_Integer f
+    PlusInfinite -> C.Plus_Infinite
 
+{-
+instance C.ToExotic ( Xml_As_String Integer ) where
+  toExotic ( Xml_As_String i ) = C.toExotic i
+-}
 
diff --git a/TPDB/Rainbow/Proof/Xml.hs b/TPDB/Rainbow/Proof/Xml.hs
--- a/TPDB/Rainbow/Proof/Xml.hs
+++ b/TPDB/Rainbow/Proof/Xml.hs
@@ -6,6 +6,8 @@
 
 import TPDB.Rainbow.Proof.Type
 
+import qualified TPDB.CPF.Proof.Type as C
+
 import TPDB.Xml
 import TPDB.Data.Xml
 -- import Matrix.MaxPlus ( MaxPlus )
@@ -113,7 +115,8 @@
 	args <- many $ element "arg" xread
 	return $ Mi_Fun { mi_const = con, mi_args = args }
         
-
+instance C.ToExotic a => C.ToExotic (Xml_As_String a) where
+    toExotic (Xml_As_String x) = C.toExotic x
 
 --------------------------------------------------------------------------------
 
@@ -151,7 +154,7 @@
 
 -- | FIXME this is broken because the keys could be
 -- Identifier or Marked Identifier
-mai :: forall a . ( Typeable a, XmlContent a )
+mai :: forall a . ( Typeable a, XmlContent a, C.ToExotic a )
     => String -> Domain -> a -> CParser Matrix_Int
 mai tag o v0 = element tag $ do
     d <- element "dimension" $ xfromstring
@@ -225,7 +228,8 @@
 	    [ element "trivial" $ return Trivial
 	    , element "reverse" $ fmap Reverse xread
 	    , element "as_trs" $ fmap As_TRS xread
-	    , element "manna_ness" $ do return () ; o <- xread ; p <- xread ; return $ MannaNess o p 
+	    , element "manna_ness" $ do 
+                      return () ; o <- xread ; p <- xread ; return $ MannaNess o p 
 	    , element "mark_symbols" $ fmap MarkSymb xread
 	    , element "dp" $ fmap DP xread
 	    , complain "Proof"
@@ -245,7 +249,8 @@
 	rename v = let Just w = Map.lookup v m in w
 	handle ( Node f args ) = Node ( Hd_Mark $ unP f ) 
 	    $ map ( fmap Int_Mark . vmap rename ) args
-    in  Rule { lhs = handle $ lhs u, rhs = handle $ rhs u, strict = True , top = False } 
+    in  Rule { lhs = handle $ lhs u, rhs = handle $ rhs u
+             , relation = Strict , top = False } 
 
 -- | super ugly risky: name mangling
 unP :: Identifier -> Identifier
diff --git a/TPDB/XTC/Read.hs b/TPDB/XTC/Read.hs
--- a/TPDB/XTC/Read.hs
+++ b/TPDB/XTC/Read.hs
@@ -73,8 +73,8 @@
 
 getTRS = proc x -> do
     sig <- getSignature <<< getChild "signature" -< x
-    str <- getRules True <<< getChild "rules" -< x
-    nostr <- listA ( getRules False <<< getChild "relrules" <<< getChild "rules" ) -< x
+    str <- getRules Strict <<< getChild "rules" -< x
+    nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x
     -- FIXME: check that symbols are use with correct arity
     th <- listA ( atTag "theory" ) -< x
     returnA -< case th of
@@ -98,7 +98,7 @@
 getRule str = proc x -> do
     l <-  getTerm <<< isElem <<< gotoChild "lhs" -< x
     r <-  getTerm <<< isElem <<< gotoChild "rhs" -< x
-    returnA -< Rule { lhs = l, strict = str, rhs = r, top = False }
+    returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
 
 readProblems :: FilePath -> IO [ Problem Identifier Identifier ]
 readProblems file = do
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 0.3
+Version: 0.6.0
 Author: Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Science
@@ -26,14 +26,20 @@
 --   test/3.15.xml, test/33.trs ,  test/z001.srs
 
 Library
-  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml
+  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml, filepath
 
   Exposed-Modules:
     TPDB.Data,     TPDB.Data.Term, TPDB.Data.Xml
+    TPDB.Compress, TPDB.Convert, TPDB.Input
+    TPDB.Mirror, 
     TPDB.Pretty, TPDB.Plain.Write,     TPDB.Plain.Read,
     TPDB.XTC,  TPDB.XTC.Read, TPDB.Xml, 
     TPDB.Rainbow.Proof.Xml,     TPDB.Rainbow.Proof.Type
     TPDB.CPF.Proof.Xml,     TPDB.CPF.Proof.Type
+
+Executable Compressor
+    Main-is: Compressor.hs
+    Build-depends: base==4.*, containers, directory, pretty, hxt, parsec
 
 Test-Suite XML
   Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml