Index: sizechecking/Constraints.hs
===================================================================
--- sizechecking/Constraints.hs	(revision 13)
+++ sizechecking/Constraints.hs	(revision 14)
@@ -158,6 +158,6 @@
         l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x)
         l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x)
-        putStrLn $ " -> " ++ show l1
-        putStrLn $ " -> " ++ show l2
+--        putStrLn $ " -> " ++ show l1
+--        putStrLn $ " -> " ++ show l2
         return $ l1 ++ l2
     checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b =
@@ -321,4 +321,5 @@
     '-' -> al - bl
     '*' -> al * bl
+    '/' -> al `SBV.sDiv` bl
     where
     al = compilel v a
Index: sizechecking/Examples.hs
===================================================================
--- sizechecking/Examples.hs	(revision 13)
+++ sizechecking/Examples.hs	(revision 14)
@@ -46,12 +46,12 @@
 
 t27 :: (SizedExp se) => Size se ((a -> a) -> a -> a)
-t27 = bind ( App t3s t3s) $ t3 `app` t3
+t27 = bind (App t3s t3s) $ t3 `app` t3
 
 t27_ :: (SizedExp se) => Size se ((a -> a) -> a -> a)
-t27_ = bind ( App t3s t3s) $ 
+t27_ = bind (App t3s t3s) $ 
         \f ->  t3 `app` t3 `app` f
 
 t27__ :: (SizedExp se) => Size se ((a -> a) -> a -> a)
-t27__ = bind ( App t3s t3s) $ \f x ->
+t27__ = bind (App t3s t3s) $ \f x ->
             t3 `app` t3 `app` f `app` x
 
@@ -216,7 +216,8 @@
 
 
-test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` List (Var 18) (Var 5)
+test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App`
+  (appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` List (Var 18) (Var 5))
 test2 :: (SizedExp se)  => Size se (([a] -> [a]) -> [a] -> [a])
-test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` l
+test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` (append `app` (f `app` l) `app` l)
 
 data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a)
@@ -234,6 +235,6 @@
         , TestCase "t9" t9
 --        , TestCase "t9_" t9_  -- too few arguments in definition
-        , TestCase "t27" t27
-        , TestCase "t27_" t27_
+--        , TestCase "t27" t27
+--        , TestCase "t27_" t27_
         , TestCase "t27__" t27__
         , TestCase "addone" addone
@@ -251,4 +252,8 @@
         , TestCase "charm" charm
         , TestCase "comp" comp
+        , TestCase "merge" merge
+        , TestCase "split1" split1
+        , TestCase "split2" split2
+        , TestCase "mergesort" mergesort
     ]
 
Index: sizechecking/SizedExp.hs
===================================================================
--- sizechecking/SizedExp.hs	(revision 13)
+++ sizechecking/SizedExp.hs	(revision 14)
@@ -81,5 +81,5 @@
         where
         (x, f) = u $ exp $ QSynt $ do 
-            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q)
+--            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q)
             return [([], fv)]
         fv = fresh (tk q) s3
@@ -90,9 +90,9 @@
 concatMapM :: (a -> IO [b]) -> [a] -> IO [b]
 concatMapM f l = liftM concat $ mapM f l
-    
+
 type SExp = ([Constraint], L)
 newtype Q a = Q { unQ :: () }
 instance SizedExp Q where
-    data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition]) 
+    data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition])
     known l = QSynt $return [([], l)]
     true = QSynt $ return []
@@ -100,19 +100,19 @@
             match1 (cond, ltype) = do
                     x <- sizeof l
-                    putStrLn $ "ORIGINAL is " ++ show x
-                    putStrLn $ "[MATCH] ==> " ++ show ltype
+--                    putStrLn $ "ORIGINAL is " ++ show x
+--                    putStrLn $ "[MATCH] ==> " ++ show ltype
                     let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
-                    putStrLn $ " --- NIL  ---" ++ show lt
+--                    putStrLn $ " --- NIL  ---" ++ show lt
                     nils <- sizeof nil
-                    print nils
+--                    print nils
                     let nilc = foldr addConstraint nils $ Zero lt:cond
                     let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype
                     let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype
-                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs
+--                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs
                     conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
-                    print conss
+--                    print conss
                     let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond
-                    print "END MATCH"
-                    print  $ nilc ++ consc
+--                    print "END MATCH"
+--                    print  $ nilc ++ consc
                     return $ nilc ++ consc
         in QSynt $ sizeof l >>= concatMapM match1 
@@ -139,6 +139,6 @@
             in do 
                 l3 <- sizeof sexp 
-                print l
-                print ll
+--                print l
+--                print ll
                 return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3
 
@@ -151,4 +151,10 @@
     signum = undefined
     fromInteger = num
+
+conditions :: Size Q b -> IO ()
+conditions (QProvable l x) = do
+    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1)
+    c <- x s1
+    print c
 
 prove :: Size Q b -> IO Bool
@@ -178,3 +184,2 @@
         print y
         return False
-