WORST_CASE(?,O(n^1)) Solution: --------- Cons :: [A(0) x A(1)] -(1)-> A(1) Cons :: [A(0) x A(0)] -(0)-> A(0) Cons :: [A(0) x A(5)] -(5)-> A(5) Cons :: [A(0) x A(4)] -(4)-> A(4) Cons :: [A(0) x A(8)] -(8)-> A(8) Cons :: [A(0) x A(7)] -(7)-> A(7) False :: [] -(0)-> A(10) False :: [] -(0)-> A(15) Nil :: [] -(0)-> A(0) Nil :: [] -(0)-> A(4) Nil :: [] -(0)-> A(5) Nil :: [] -(0)-> A(1) Nil :: [] -(0)-> A(13) Nil :: [] -(0)-> A(15) Nil :: [] -(0)-> A(12) True :: [] -(0)-> A(10) True :: [] -(0)-> A(15) True :: [] -(0)-> A(14) f :: [A(7) x A(4)] -(6)-> A(0) f[Ite][False][Ite] :: [A(10) x A(7) x A(4)] -(3)-> A(0) g :: [A(8) x A(4)] -(8)-> A(0) g[Ite][False][Ite] :: [A(10) x A(8) x A(4)] -(4)-> A(0) goal :: [A(15) x A(15)] -(15)-> A(0) lt0 :: [A(0) x A(1)] -(1)-> A(13) notEmpty :: [A(5)] -(11)-> A(0) number4 :: [A(0)] -(15)-> A(0) Cost Free Signatures: --------------------- Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) False :: [] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) True :: [] -(0)-> A_cf(0) f :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) f[Ite][False][Ite] :: [A_cf(0) x A_cf(0) x A_cf(0)] -(0)-> A_cf(0) g :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) g[Ite][False][Ite] :: [A_cf(0) x A_cf(0) x A_cf(0)] -(0)-> A_cf(0) lt0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Base Constructors: ------------------ Cons_A :: [A(0) x A(1)] -(1)-> A(1) False_A :: [] -(0)-> A(1) Nil_A :: [] -(0)-> A(1) True_A :: [] -(0)-> A(1)