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
@@ -38,7 +38,7 @@
    deriving ( Typeable )      
 
 data Proof = TrsTerminationProof TrsTerminationProof
-           -- | TrsNonterminationProof  
+           --  | TrsNonterminationProof  
    deriving ( Typeable )
 
 data Sharp i = Sharp i | Plain i
@@ -56,9 +56,19 @@
                    }  
      | DpTrans  { dptrans_dps :: DPS
                 , markedSymbols :: Bool , dptrans_dpProof :: DpProof }
+     | Semlab {  model :: Model 
+              , trs :: TRS Identifier Identifier
+              , trsTerminationProof :: TrsTerminationProof
+              }
+     | Unlab {  trs :: TRS Identifier Identifier
+              , trsTerminationProof :: TrsTerminationProof
+              }
      | StringReversal { trs :: TRS Identifier Identifier
                       , trsTerminationProof :: TrsTerminationProof  
                       }  
+   deriving ( Typeable )
+
+data Model = FiniteModel { carrierSize :: Int }
    deriving ( Typeable )
        
 data DpProof = PIsEmpty  
diff --git a/TPDB/Convert.hs b/TPDB/Convert.hs
--- a/TPDB/Convert.hs
+++ b/TPDB/Convert.hs
@@ -3,15 +3,17 @@
 import TPDB.Data
 import Control.Monad ( forM, guard )
 
-srs2trs :: SRS s -> TRS Identifier s
+srs2trs :: SRS Identifier -> TRS Identifier Identifier
 srs2trs s = s { separate = False
               , rules = map convert_srs_rule $ rules s
               }  
 
 convert_srs_rule u = 
-    let v = mk 0 "x" 
-    in  u { lhs = unspine v $ lhs u
-          , rhs = unspine v $ rhs u        
+    let v = mk 0 "x"
+        set_arity a s = s { arity = a }
+        handle = unspine v . map (set_arity 1)
+    in  u { lhs = handle $ lhs u
+          , rhs = handle $ rhs u        
           } 
                   
 trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
diff --git a/TPDB/DP.hs b/TPDB/DP.hs
--- a/TPDB/DP.hs
+++ b/TPDB/DP.hs
@@ -33,6 +33,7 @@
        os = map ( \ u -> Rule { relation = Weak
                                , lhs = fmap Original $ lhs u  
                                , rhs = fmap Original $ rhs u  
+                               , top = False
                                } )
            $ rules s
        defined = S.fromList $ do 
@@ -43,5 +44,9 @@
             u <- rules s
             (_, r @ (Node f args)) <- positions $ rhs u
             guard $ S.member f defined
-            return $ u { lhs = marked $ lhs u, rhs = marked r }
+            return $ Rule { relation = Strict
+                          , lhs = marked $ lhs u
+                          , rhs = marked r 
+                          , top = True
+                          }
    in RS { rules = us ++ os, separate = separate s } 
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -94,8 +94,8 @@
 type TES = TRS Identifier Identifier
 type SES = SRS Identifier
 
-mknullary s = Identifier { arity = 0, name = s }
-mkunary s = Identifier { arity = 1, name = s }
+mknullary s = mk 0 s
+mkunary   s = mk 1 s
 
 from_strict_rules :: Bool -> [(t,t)] -> RS i t
 from_strict_rules sep rs = 
diff --git a/TPDB/Xml/Pretty.hs b/TPDB/Xml/Pretty.hs
--- a/TPDB/Xml/Pretty.hs
+++ b/TPDB/Xml/Pretty.hs
@@ -1,11 +1,11 @@
 -- | original author: Malcolm Wallace, 
 -- license: LGPL
 -- http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html
-
+--
 -- modified by Johannes Waldmann
 -- to use a different pretty-printer back-end.
-
--- | This is a pretty-printer for turning the internal representation
+--
+-- This is a pretty-printer for turning the internal representation
 --   of generic structured XML documents into the Doc type (which can
 --   later be rendered using Text.PrettyPrint.HughesPJ.render).
 --   Essentially there is one pp function for each type in
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 0.7.1
+Version: 0.8.2
 Author: Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Science