insertsort.out

== Signature ==
       [] :: [Int]
      (:) :: Int -> [Int] -> [Int]
     (++) :: [Int] -> [Int] -> [Int]
   insert :: Int -> [Int] -> [Int]
     sort :: [Int] -> [Int]
 (prj_<=) :: TestCaseWrapped "<=" (Int -> Int -> Bool) -> Int
(prj_<=') :: TestCaseWrapped "<=" (Int -> Int -> Bool) -> Int
  (prj_<) :: TestCaseWrapped "<" (Int -> Int -> Bool) -> Int
 (prj_<') :: TestCaseWrapped "<" (Int -> Int -> Bool) -> Int
     (<=) :: Int -> Int -> Bool
      (<) :: Int -> Int -> Bool
     True :: Bool

== Laws ==
  1. sort [] = []
  2. x <= x = True
  3. xs ++ [] = xs
  4. [] ++ xs = xs
  5. insert x [] = x : []
  6. sort (sort xs) = sort xs
  7. x < x = y < y
  8. sort (x : xs) = insert x (sort xs)
  9. sort (insert x xs) = insert x (sort xs)
 10. sort (xs ++ ys) = sort (ys ++ xs)
 11. (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
 12. x : (xs ++ ys) = (x : xs) ++ ys
 13. insert x (x : xs) = x : (x : xs)
 14. x < y => x < y = True
 15. z < y => y < z = x < x
 16. z <= y => y < z = x < x
 17. x < y => x <= y = True
 18. z < y => y <= z = x < x
 19. x <= y => x <= y = True
 20. sort (xs ++ sort ys) = sort (xs ++ ys)
 21. insert y (insert x xs) = insert x (insert y xs)