WORST_CASE(?,O(n^2))

Solution:
---------

  0 :: [] -(0)-> A(4, 0)
  0 :: [] -(0)-> A(0, 0)
  0 :: [] -(0)-> A(1, 0)
  0 :: [] -(0)-> A(8, 1)
  0 :: [] -(0)-> A(2, 7)
  0 :: [] -(0)-> A(15, 7)
  0 :: [] -(0)-> A(7, 7)
  0 :: [] -(0)-> A(5, 13)
  a__div :: [A(8, 1) x A(0, 7)] -(6)-> A(1, 1)
  a__geq :: [A(1, 0) x A(0, 0)] -(1)-> A(1, 1)
  a__if :: [A(1, 1) x A(2, 7) x A(2, 7)] -(3)-> A(1, 1)
  a__minus :: [A(4, 0) x A(0, 0)] -(1)-> A(13, 1)
  div :: [A(9, 7) x A(0, 7)] -(7)-> A(2, 7)
  div :: [A(12, 7) x A(0, 7)] -(7)-> A(5, 7)
  div :: [A(5, 1) x A(0, 1)] -(1)-> A(4, 1)
  false :: [] -(0)-> A(1, 1)
  false :: [] -(0)-> A(2, 7)
  false :: [] -(0)-> A(7, 7)
  geq :: [A(2, 0) x A(0, 0)] -(0)-> A(2, 7)
  geq :: [A(1, 0) x A(0, 0)] -(0)-> A(1, 7)
  if :: [A(2, 7) x A(2, 7) x A(2, 7)] -(7)-> A(2, 7)
  if :: [A(1, 1) x A(1, 1) x A(1, 1)] -(1)-> A(1, 1)
  mark :: [A(2, 7)] -(2)-> A(1, 1)
  minus :: [A(7, 0) x A(0, 0)] -(0)-> A(2, 7)
  minus :: [A(7, 0) x A(0, 0)] -(0)-> A(12, 7)
  minus :: [A(1, 0) x A(0, 0)] -(0)-> A(14, 1)
  s :: [A(4, 0)] -(4)-> A(4, 0)
  s :: [A(0, 0)] -(0)-> A(0, 0)
  s :: [A(1, 0)] -(1)-> A(1, 0)
  s :: [A(0, 7)] -(0)-> A(0, 7)
  s :: [A(8, 1)] -(8)-> A(8, 1)
  s :: [A(2, 7)] -(2)-> A(2, 7)
  s :: [A(1, 1)] -(1)-> A(1, 1)
  true :: [] -(0)-> A(1, 1)
  true :: [] -(0)-> A(2, 7)
  true :: [] -(0)-> A(7, 7)


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

  0 :: [] -(0)-> A_cf(0, 0)
  0 :: [] -(0)-> A_cf(7, 0)
  0 :: [] -(0)-> A_cf(11, 3)
  0 :: [] -(0)-> A_cf(15, 11)
  0 :: [] -(0)-> A_cf(11, 2)
  a__div :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  a__div :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  a__geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  a__geq :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 3)
  a__geq :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  a__if :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  a__if :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(15, 8)] -(0)-> A_cf(7, 0)
  a__if :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(7, 0)] -(0)-> A_cf(7, 0)
  a__minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  a__minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  div :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  div :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  div :: [A_cf(11, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 0)
  false :: [] -(0)-> A_cf(0, 0)
  false :: [] -(0)-> A_cf(7, 0)
  false :: [] -(0)-> A_cf(11, 3)
  false :: [] -(0)-> A_cf(11, 2)
  geq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  geq :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  geq :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 12)
  geq :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 1)
  if :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  if :: [A_cf(7, 0) x A_cf(7, 0) x A_cf(7, 0)] -(0)-> A_cf(7, 0)
  mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
  mark :: [A_cf(7, 0)] -(0)-> A_cf(7, 0)
  minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
  minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(7, 0)
  minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 0)
  minus :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(13, 0)
  s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
  s :: [A_cf(7, 0)] -(7)-> A_cf(7, 0)
  true :: [] -(0)-> A_cf(0, 0)
  true :: [] -(0)-> A_cf(7, 0)
  true :: [] -(0)-> A_cf(11, 3)
  true :: [] -(0)-> A_cf(11, 2)


Base Constructors:
------------------
  0_A :: [] -(0)-> A(1, 0)
  0_A :: [] -(0)-> A(0, 1)
  div_A :: [A(1, 0) x A(0, 0)] -(0)-> A(1, 0)
  div_A :: [A(1, 1) x A(0, 1)] -(1)-> A(0, 1)
  false_A :: [] -(0)-> A(1, 0)
  false_A :: [] -(0)-> A(0, 1)
  geq_A :: [A(1, 0) x A(0, 0)] -(0)-> A(1, 0)
  geq_A :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 1)
  if_A :: [A(1, 0) x A(1, 0) x A(1, 0)] -(0)-> A(1, 0)
  if_A :: [A(0, 1) x A(0, 1) x A(0, 1)] -(1)-> A(0, 1)
  minus_A :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 0)
  minus_A :: [A(1, 0) x A(0, 0)] -(0)-> A(0, 1)
  s_A :: [A(1, 0)] -(1)-> A(1, 0)
  s_A :: [A(0, 1)] -(0)-> A(0, 1)
  true_A :: [] -(0)-> A(1, 0)
  true_A :: [] -(0)-> A(0, 1)