An example

• The original function:
  quicksort :: Ord a => [a] -> [a] quicksort [] = [] quicksort (x:xs) = quicksort (filter (<x) xs)++ x: quicksort (filter (>=x) xs)
• The domain predicate:
  Dqs :: [a] -> Prop QsNil :: Dqs [] QsCons :: (x::a)->(xs::[a])-> Dqs (filter (<x) xs)-> Dqs (filter (>=x) xs) -> Dqs (x:xs)