WORST_CASE(?,O(n^2))

Solution:
---------

  0 :: [] -(0)-> c(0, 0)
  0 :: [] -(0)-> c(3, 0)
  append :: [a(1, 0) x a(0, 0)] -(1)-> a(0, 0)
  dd :: [c(5, 4) x a(9, 4)] -(5)-> a(5, 4)
  dd :: [c(9, 4) x a(13, 4)] -(9)-> a(9, 4)
  dd :: [c(1, 0) x a(1, 0)] -(1)-> a(1, 0)
  dd :: [c(0, 0) x a(0, 0)] -(0)-> a(0, 0)
  dd :: [c(6, 4) x a(10, 4)] -(6)-> a(6, 4)
  false :: [] -(0)-> b(1, 1)
  false :: [] -(0)-> b(13, 13)
  gt :: [c(3, 0) x c(0, 0)] -(1)-> b(10, 10)
  nil :: [] -(0)-> a(5, 4)
  nil :: [] -(0)-> a(9, 4)
  nil :: [] -(0)-> a(1, 0)
  nil :: [] -(0)-> a(7, 7)
  nil :: [] -(0)-> a(15, 13)
  pair :: [a(6, 4) x a(6, 4)] -(0)-> d(6, 4)
  pair :: [a(10, 4) x a(10, 4)] -(0)-> d(10, 4)
  pair :: [a(8, 8) x a(8, 8)] -(0)-> d(8, 8)
  quicksort :: [a(5, 4)] -(1)-> a(0, 0)
  quicksort' :: [c(4, 0) x d(6, 4)] -(4)-> a(0, 0)
  s :: [c(3, 0)] -(3)-> c(3, 0)
  s :: [c(0, 0)] -(0)-> c(0, 0)
  split :: [c(0, 0) x a(9, 4)] -(1)-> d(6, 4)
  split' :: [b(1, 1) x c(6, 4) x d(10, 4)] -(7)-> d(6, 4)
  true :: [] -(0)-> b(1, 1)
  true :: [] -(0)-> b(13, 13)


Cost Free Signatures:
---------------------

  0 :: [] -(0)-> c_cf(0, 0)
  append :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  append :: [a_cf(1, 0) x a_cf(1, 0)] -(0)-> a_cf(1, 0)
  dd :: [c_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  dd :: [c_cf(1, 0) x a_cf(1, 0)] -(1)-> a_cf(1, 0)
  dd :: [c_cf(4, 0) x a_cf(4, 0)] -(4)-> a_cf(4, 0)
  false :: [] -(0)-> b_cf(0, 0)
  false :: [] -(0)-> b_cf(15, 15)
  false :: [] -(0)-> b_cf(1, 1)
  gt :: [c_cf(0, 0) x c_cf(0, 0)] -(0)-> b_cf(0, 0)
  gt :: [c_cf(0, 0) x c_cf(0, 0)] -(0)-> b_cf(13, 13)
  nil :: [] -(0)-> a_cf(0, 0)
  nil :: [] -(0)-> a_cf(1, 0)
  nil :: [] -(0)-> a_cf(3, 3)
  nil :: [] -(0)-> a_cf(15, 11)
  nil :: [] -(0)-> a_cf(12, 11)
  nil :: [] -(0)-> a_cf(11, 11)
  nil :: [] -(0)-> a_cf(4, 0)
  pair :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> d_cf(0, 0)
  pair :: [a_cf(1, 0) x a_cf(1, 0)] -(0)-> d_cf(1, 0)
  pair :: [a_cf(4, 1) x a_cf(4, 1)] -(0)-> d_cf(4, 1)
  pair :: [a_cf(6, 10) x a_cf(6, 10)] -(0)-> d_cf(6, 10)
  pair :: [a_cf(8, 5) x a_cf(8, 5)] -(0)-> d_cf(8, 5)
  pair :: [a_cf(4, 0) x a_cf(4, 0)] -(0)-> d_cf(4, 0)
  quicksort :: [a_cf(0, 0)] -(0)-> a_cf(0, 0)
  quicksort :: [a_cf(1, 0)] -(0)-> a_cf(1, 0)
  quicksort :: [a_cf(1, 0)] -(0)-> a_cf(0, 0)
  quicksort' :: [c_cf(0, 0) x d_cf(0, 0)] -(0)-> a_cf(0, 0)
  quicksort' :: [c_cf(1, 0) x d_cf(1, 0)] -(1)-> a_cf(1, 0)
  quicksort' :: [c_cf(0, 0) x d_cf(1, 0)] -(0)-> a_cf(0, 0)
  s :: [c_cf(0, 0)] -(0)-> c_cf(0, 0)
  split :: [c_cf(0, 0) x a_cf(0, 0)] -(0)-> d_cf(0, 0)
  split :: [c_cf(0, 0) x a_cf(1, 0)] -(0)-> d_cf(1, 0)
  split :: [c_cf(0, 0) x a_cf(4, 0)] -(0)-> d_cf(4, 0)
  split' :: [b_cf(0, 0) x c_cf(0, 0) x d_cf(0, 0)] -(0)-> d_cf(0, 0)
  split' :: [b_cf(0, 0) x c_cf(1, 0) x d_cf(1, 0)] -(1)-> d_cf(1, 0)
  split' :: [b_cf(1, 1) x c_cf(4, 0) x d_cf(4, 0)] -(4)-> d_cf(4, 0)
  true :: [] -(0)-> b_cf(0, 0)
  true :: [] -(0)-> b_cf(15, 15)
  true :: [] -(0)-> b_cf(1, 1)


Base Constructors:
------------------
  0_c :: [] -(0)-> c(1, 0)
  0_c :: [] -(0)-> c(0, 1)
  dd_a :: [c(1, 0) x a(1, 0)] -(1)-> a(1, 0)
  dd_a :: [c(0, 1) x a(1, 1)] -(0)-> a(0, 1)
  false_b :: [] -(0)-> b(1, 0)
  false_b :: [] -(0)-> b(0, 1)
  nil_a :: [] -(0)-> a(1, 0)
  nil_a :: [] -(0)-> a(0, 1)
  pair_d :: [a(1, 0) x a(1, 0)] -(0)-> d(1, 0)
  pair_d :: [a(0, 1) x a(0, 1)] -(0)-> d(0, 1)
  s_c :: [c(1, 0)] -(1)-> c(1, 0)
  s_c :: [c(0, 0)] -(0)-> c(0, 1)
  true_b :: [] -(0)-> b(1, 0)
  true_b :: [] -(0)-> b(0, 1)