insertsort-s4.out

max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Int
_ :: [Int]
False :: Bool
True :: Bool
[] :: [Int]
(:) :: Int -> [Int] -> [Int]
(++) :: [Int] -> [Int] -> [Int]
elem :: Int -> [Int] -> Bool
ordered :: [Int] -> Bool
all :: (Int -> Bool) -> [Int] -> Bool
insert :: Int -> [Int] -> [Int]
sort :: [Int] -> [Int]
(==) :: Int -> Int -> Bool
(<=) :: Int -> Int -> Bool
(<) :: Int -> Int -> Bool
(==) :: Bool -> Bool -> Bool
(==) :: [Int] -> [Int] -> Bool

    ordered (sort xs) == True
ordered (insert x xs) == ordered xs
      (xs == sort xs) == ordered xs
     elem x (sort xs) == elem x xs
      (sort xs == []) == (xs == [])
       sort (sort xs) == sort xs
          insert x [] == [x]
      sort (xs ++ ys) == sort (ys ++ xs)
   sort (insert x xs) == insert x (sort xs)
          sort (x:xs) == insert x (sort xs)

    sort xs <= xs
insert x xs <= x:xs