module Sublists where


sublist [] _ = True
sublist _ [] = False
sublist (x:xs) (y:ys) | x==y = sublist xs ys
                      | otherwise = sublist (x:xs) ys

sublists [] = [[]]
sublists (x:xs) = map (x:) s ++ s
  where s = sublists xs 

{-sublists (x:xs) = [x:l | l<-s] ++ s
  where s = sublists xs 
-}


{-P:
assert Sublist0 = {-#cert:QcSublist0#-}
  All l1::[Int] . 
     {[] `elem` sublists l1} ::: True

assert Sublist1 = {-#cert:QcSublist1#-}
  All l1::[Int] . All l2 . 
     {l1 `elem` sublists l2} ::: True
        ==> {sublist l1 l2}:::True
         
assert Sublist2 = {-#cert:QcSublist2#-}
  All l1::[Int] . All l2 . 
     {sublist l1 l2}:::True ==> 
        {l1 `elem` sublists l2} ::: True


 -}