Comparison between rippling and case-analysis technique, and
simplification based technique.

16 theorems solved by rippling but not simplification:
-------------------------------------------------------------------
 take n xs @ drop n xs = xs
 (i minus j) minus k = i minus (j + k)
 drop n (map f xs) = map f (drop n xs)
 len drop n xs = (len xs) minus n
 len sort l = len l
 CaseAnalysis2.max (CaseAnalysis2.max a b) c =
CaseAnalysis2.max a (CaseAnalysis2.max b c)
 CaseAnalysis2.max a b = CaseAnalysis2.max b a
 (CaseAnalysis2.max a b = a) = b leq a
 (CaseAnalysis2.max a b = b) = a leq b
 CaseAnalysis2.min (CaseAnalysis2.min a b) c =
CaseAnalysis2.min a (CaseAnalysis2.min b c)
 CaseAnalysis2.min a b = CaseAnalysis2.min b a
 (CaseAnalysis2.min a b = a) = a leq b
 (CaseAnalysis2.min a b = b) = b leq a
 take n (map f xs) = map f (take n xs)
 zip (x # xs) ys = (case ys of [] => [] | y # ys => (x, y) # zip xs ys)
 height (mirror a) = height a


6 theorems solved by simplification but not rippling:
-----------------------------------------------------
 xs ~= [] ==> butlast xs @ [last xs] = xs
 butlast (xs @ [x]) = xs
 ys = [] ==> last (xs @ ys) = last xs
 xs ~= [] ==> last (x # xs) = last xs
 last (xs @ [x]) = x
 x ~= y ==> x mem ins y l = x mem l