WORST_CASE(?,O(n^2)) Solution: --------- 0 :: [] -(0)-> A(6, 3) 0 :: [] -(0)-> A(9, 3) 0 :: [] -(0)-> A(13, 5) a__add :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3) a__from :: [A(9, 3)] -(8)-> A(6, 3) a__fst :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3) a__len :: [A(6, 3)] -(7)-> A(6, 3) add :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3) add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) add :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3) cons :: [A(9, 3) x A(0, 0)] -(9)-> A(9, 3) cons :: [A(6, 3) x A(0, 0)] -(6)-> A(6, 3) from :: [A(12, 3)] -(9)-> A(9, 3) from :: [A(0, 0)] -(0)-> A(0, 0) from :: [A(9, 3)] -(6)-> A(6, 3) fst :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3) fst :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) fst :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3) len :: [A(9, 3)] -(9)-> A(9, 3) len :: [A(0, 0)] -(0)-> A(0, 0) len :: [A(6, 3)] -(6)-> A(6, 3) mark :: [A(9, 3)] -(1)-> A(6, 3) nil :: [] -(0)-> A(6, 3) nil :: [] -(0)-> A(9, 3) nil :: [] -(0)-> A(13, 5) s :: [A(0, 0)] -(0)-> A(6, 3) s :: [A(0, 0)] -(0)-> A(9, 3) s :: [A(0, 0)] -(0)-> A(2, 11) s :: [A(0, 0)] -(0)-> A(12, 13) s :: [A(0, 0)] -(0)-> A(11, 15) s :: [A(0, 0)] -(0)-> A(8, 10) Cost Free Signatures: --------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(3, 0) 0 :: [] -(0)-> A_cf(3, 2) a__add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) a__from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) a__from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) a__fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) a__fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) a__len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) a__len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(3, 0) x A_cf(0, 0)] -(3)-> A_cf(3, 0) from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) from :: [A_cf(1, 1)] -(0)-> A_cf(0, 1) from :: [A_cf(2, 2)] -(0)-> A_cf(0, 2) fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) mark :: [A_cf(3, 0)] -(0)-> A_cf(3, 0) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(3, 0) nil :: [] -(0)-> A_cf(3, 2) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(3, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(1, 4) s :: [A_cf(0, 0)] -(0)-> A_cf(4, 4) s :: [A_cf(0, 0)] -(0)-> A_cf(12, 12) s :: [A_cf(0, 0)] -(0)-> A_cf(7, 8) s :: [A_cf(0, 0)] -(0)-> A_cf(2, 12) s :: [A_cf(0, 0)] -(0)-> A_cf(5, 8) s :: [A_cf(0, 0)] -(0)-> A_cf(3, 10) s :: [A_cf(0, 0)] -(0)-> A_cf(9, 10) s :: [A_cf(0, 0)] -(0)-> A_cf(14, 14) s :: [A_cf(0, 0)] -(0)-> A_cf(6, 6) s :: [A_cf(0, 0)] -(0)-> A_cf(3, 2) Base Constructors: ------------------ 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) add_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) add_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) cons_A :: [A(1, 0) x A(0, 0)] -(1)-> A(1, 0) cons_A :: [A(0, 1) x A(0, 0)] -(0)-> A(0, 1) from_A :: [A(1, 0)] -(1)-> A(1, 0) from_A :: [A(1, 1)] -(0)-> A(0, 1) fst_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) fst_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) len_A :: [A(1, 0)] -(1)-> A(1, 0) len_A :: [A(0, 1)] -(0)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) s_A :: [A(0, 0)] -(0)-> A(1, 0) s_A :: [A(0, 0)] -(0)-> A(0, 1)