WORST_CASE(?,O(n^2))

Solution:
---------

  "Add" :: ["expr"(7, 3) x "expr"(4, 3)] -(4)-> "expr"(4, 3)
  "Nat" :: ["nat"(4, 0)] -(0)-> "expr"(4, 3)
  "Nat" :: ["nat"(7, 0)] -(0)-> "expr"(7, 4)
  "Nat" :: ["nat"(4, 0)] -(0)-> "expr"(4, 14)
  "Nat" :: ["nat"(4, 0)] -(0)-> "expr"(4, 13)
  "Sub" :: ["expr"(4, 3) x "expr"(4, 3)] -(4)-> "expr"(4, 3)
  "Sub" :: ["expr"(4, 4) x "expr"(4, 4)] -(4)-> "expr"(4, 4)
  "Succ" :: ["nat"(7, 0)] -(7)-> "nat"(7, 0)
  "Succ" :: ["nat"(4, 0)] -(4)-> "nat"(4, 0)
  "Succ" :: ["nat"(4, 0)] -(4)-> "nat"(4, 12)
  "Zero" :: [] -(0)-> "nat"(7, 0)
  "Zero" :: [] -(0)-> "nat"(4, 0)
  "Zero" :: [] -(0)-> "nat"(12, 8)
  "cond_eval_expr_1" :: ["nat"(7, 0) x "expr"(4, 3)] -(3)-> "nat"(4, 0)
  "cond_eval_expr_2" :: ["nat"(4, 0) x "expr"(4, 3)] -(2)-> "nat"(4, 0)
  "cond_eval_expr_3" :: ["nat"(4, 0) x "nat"(4, 0)] -(4)-> "nat"(4, 0)
  "eval#1" :: ["expr"(4, 3)] -(1)-> "nat"(4, 0)
  "main" :: ["expr"(10, 13)] -(16)-> "nat"(2, 0)


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

  "Add" :: ["expr"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Add" :: ["expr"_cf(3, 0) x "expr"_cf(3, 0)] -(3)-> "expr"_cf(3, 0)
  "Nat" :: ["nat"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Nat" :: ["nat"_cf(3, 0)] -(0)-> "expr"_cf(3, 0)
  "Nat" :: ["nat"_cf(3, 0)] -(0)-> "expr"_cf(3, 14)
  "Nat" :: ["nat"_cf(3, 0)] -(0)-> "expr"_cf(3, 8)
  "Nat" :: ["nat"_cf(3, 0)] -(0)-> "expr"_cf(3, 13)
  "Sub" :: ["expr"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Sub" :: ["expr"_cf(3, 0) x "expr"_cf(3, 0)] -(3)-> "expr"_cf(3, 0)
  "Succ" :: ["nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "Succ" :: ["nat"_cf(3, 0)] -(3)-> "nat"_cf(3, 0)
  "Zero" :: [] -(0)-> "nat"_cf(0, 0)
  "Zero" :: [] -(0)-> "nat"_cf(3, 0)
  "Zero" :: [] -(0)-> "nat"_cf(12, 8)
  "cond_eval_expr_1" :: ["nat"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "cond_eval_expr_1" :: ["nat"_cf(3, 0) x "expr"_cf(3, 0)] -(3)-> "nat"_cf(3, 0)
  "cond_eval_expr_2" :: ["nat"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "cond_eval_expr_2" :: ["nat"_cf(3, 0) x "expr"_cf(3, 0)] -(0)-> "nat"_cf(3, 0)
  "cond_eval_expr_3" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "cond_eval_expr_3" :: ["nat"_cf(3, 0) x "nat"_cf(3, 0)] -(1)-> "nat"_cf(3, 0)
  "eval#1" :: ["expr"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "eval#1" :: ["expr"_cf(3, 0)] -(0)-> "nat"_cf(3, 0)


Base Constructors:
------------------
  "\"Add\"_expr" :: ["expr"(1, 0) x "expr"(1, 0)] -(1)-> "expr"(1, 0)
  "\"Add\"_expr" :: ["expr"(1, 1) x "expr"(0, 1)] -(0)-> "expr"(0, 1)
  "\"Nat\"_expr" :: ["nat"(1, 0)] -(0)-> "expr"(1, 0)
  "\"Nat\"_expr" :: ["nat"(0, 0)] -(0)-> "expr"(0, 1)
  "\"Sub\"_expr" :: ["expr"(1, 0) x "expr"(1, 0)] -(1)-> "expr"(1, 0)
  "\"Sub\"_expr" :: ["expr"(0, 1) x "expr"(0, 1)] -(0)-> "expr"(0, 1)
  "\"Succ\"_nat" :: ["nat"(1, 0)] -(1)-> "nat"(1, 0)
  "\"Succ\"_nat" :: ["nat"(0, 0)] -(0)-> "nat"(0, 1)
  "\"Zero\"_nat" :: [] -(0)-> "nat"(1, 0)
  "\"Zero\"_nat" :: [] -(0)-> "nat"(0, 1)



Parsed Typed Term Rewrite System:
---------------------------------

(STRATEGY
 INNERMOST)
(VAR
 "v3" "v5" "v7" "v2" "v10" "v4" "v12" "v8" "v14" "v0")
(DATATYPES
   "expr" = µX.< "Add"(X, X), "Nat"("nat"), "Sub"(X, X) >
   "nat" = µX.< "Zero", "Succ"(X) >)
(SIGNATURES
   "cond_eval_expr_1" :: ["nat" x "expr"] --> "nat"
   "cond_eval_expr_3" :: ["nat" x "nat"] --> "nat"
   "cond_eval_expr_2" :: ["nat" x "expr"] --> "nat"
   "eval#1" :: ["expr"] --> "nat"
   "main" :: ["expr"] --> "nat")
(RULES
 "cond_eval_expr_1"("Zero"(),"v3") -> "eval#1"("v3")
 "cond_eval_expr_1"("Succ"("v5"),"v3") -> "Succ"("eval#1"("Add"("Nat"("v5"),"v3")))
 "cond_eval_expr_3"("Zero"(),"v5") -> "Zero"()
 "cond_eval_expr_3"("Succ"("v7"),"v5") -> "eval#1"("Sub"("Nat"("v7"),"Nat"("v5")))
 "cond_eval_expr_2"("Zero"(),"v2") -> "eval#1"("v2")
 "cond_eval_expr_2"("Succ"("v10"),"v5") -> "cond_eval_expr_3"("eval#1"("v5"),"v10")
 "eval#1"("Nat"("v4")) -> "v4"
 "eval#1"("Add"("v10","v12")) -> "cond_eval_expr_1"("eval#1"("v10"),"v12")
 "eval#1"("Sub"("v8","v14")) -> "cond_eval_expr_2"("eval#1"("v14"),"v8")
 "main"("v0") -> "eval#1"("v0"))


WORST_CASE(?,O(n^2))