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) _ :: Char _ :: [Char] _ :: [[Char]] "" :: [Char] " " :: [Char] "\n" :: [Char] lines :: [Char] -> [[Char]] words :: [Char] -> [[Char]] unlines :: [[Char]] -> [Char] unwords :: [[Char]] -> [Char] (++) :: [Char] -> [Char] -> [Char] cs ++ "" == cs "" ++ cs == cs unlines (lines (unlines css)) == unlines css lines (unlines (lines cs)) == lines cs words (unlines (words cs)) == words cs lines (unlines (words cs)) == words cs words (unlines (lines cs)) == words cs words (unwords css) == words (unlines css) words (cs ++ " ") == words cs words (cs ++ "\n") == words cs words (" " ++ cs) == words cs words ("\n" ++ cs) == words cs "" <= cs cs <= cs ++ ds cs <= unlines (lines cs) "\n" <= cs ++ "\n" "\n" <= cs ++ " " "\n" ++ cs <= " " unwords (lines cs) <= cs ++ ds "\n" ++ cs <= ds ++ " " unlines (lines cs) <= cs ++ cs "\n" ++ cs <= cs ++ "\n" cs ++ "\n" <= cs ++ " " unlines (lines cs) <= cs ++ " " unlines (lines cs) <= cs ++ "\n" lines "" <= css lines (unlines css) <= css