WORST_CASE(?,O(n^2))

Solution:
---------

  "Add" :: ["expr"(12, 12) x "expr"(12, 12)] -(12)-> "expr"(0, 12)
  "Nat" :: ["nat"(12, 0)] -(12)-> "expr"(0, 12)
  "Sub" :: ["expr"(0, 12) x "expr"(0, 12)] -(12)-> "expr"(0, 12)
  "Succ" :: ["nat"(0, 0)] -(0)-> "nat"(0, 0)
  "Succ" :: ["nat"(4, 0)] -(4)-> "nat"(4, 0)
  "Succ" :: ["nat"(5, 0)] -(5)-> "nat"(5, 0)
  "Zero" :: [] -(0)-> "nat"(0, 0)
  "Zero" :: [] -(0)-> "nat"(4, 0)
  "Zero" :: [] -(0)-> "nat"(5, 0)
  "Zero" :: [] -(0)-> "nat"(12, 8)
  "add#2" :: ["nat"(5, 0) x "nat"(9, 0)] -(2)-> "nat"(4, 0)
  "eval#1" :: ["expr"(0, 12)] -(0)-> "nat"(4, 0)
  "main" :: ["expr"(14, 14)] -(8)-> "nat"(2, 0)
  "sub#2" :: ["nat"(4, 0) x "nat"(0, 0)] -(9)-> "nat"(4, 0)


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

  "Add" :: ["expr"_cf(12, 0) x "expr"_cf(12, 0)] -(0)-> "expr"_cf(12, 0)
  "Add" :: ["expr"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Nat" :: ["nat"_cf(12, 0)] -(0)-> "expr"_cf(12, 0)
  "Nat" :: ["nat"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Sub" :: ["expr"_cf(12, 0) x "expr"_cf(12, 0)] -(12)-> "expr"_cf(12, 0)
  "Sub" :: ["expr"_cf(0, 0) x "expr"_cf(0, 0)] -(0)-> "expr"_cf(0, 0)
  "Succ" :: ["nat"_cf(1, 0)] -(1)-> "nat"_cf(1, 0)
  "Succ" :: ["nat"_cf(1, 0)] -(1)-> "nat"_cf(1, 14)
  "Succ" :: ["nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "Succ" :: ["nat"_cf(6, 0)] -(6)-> "nat"_cf(6, 0)
  "Succ" :: ["nat"_cf(6, 0)] -(6)-> "nat"_cf(6, 15)
  "Zero" :: [] -(0)-> "nat"_cf(1, 0)
  "Zero" :: [] -(0)-> "nat"_cf(0, 0)
  "Zero" :: [] -(0)-> "nat"_cf(12, 8)
  "Zero" :: [] -(0)-> "nat"_cf(6, 0)
  "Zero" :: [] -(0)-> "nat"_cf(15, 0)
  "add#2" :: ["nat"_cf(1, 0) x "nat"_cf(1, 0)] -(0)-> "nat"_cf(1, 0)
  "add#2" :: ["nat"_cf(6, 0) x "nat"_cf(6, 0)] -(0)-> "nat"_cf(6, 0)
  "add#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "eval#1" :: ["expr"_cf(12, 0)] -(0)-> "nat"_cf(1, 0)
  "eval#1" :: ["expr"_cf(12, 0)] -(0)-> "nat"_cf(6, 0)
  "eval#1" :: ["expr"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "sub#2" :: ["nat"_cf(1, 0) x "nat"_cf(0, 0)] -(0)-> "nat"_cf(1, 0)
  "sub#2" :: ["nat"_cf(6, 0) x "nat"_cf(0, 0)] -(0)-> "nat"_cf(6, 0)
  "sub#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "sub#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(1)-> "nat"_cf(0, 0)


Base Constructors:
------------------
  "\"Add\"_expr" :: ["expr"(1, 0) x "expr"(1, 0)] -(0)-> "expr"(1, 0)
  "\"Add\"_expr" :: ["expr"(1, 1) x "expr"(1, 1)] -(1)-> "expr"(0, 1)
  "\"Nat\"_expr" :: ["nat"(1, 0)] -(0)-> "expr"(1, 0)
  "\"Nat\"_expr" :: ["nat"(1, 0)] -(1)-> "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)] -(1)-> "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
 "v1" "v2" "v8" "v16" "v4" "v12")
(DATATYPES
   "expr" = µX.< "Nat"("nat"), "Add"(X, X), "Sub"(X, X) >
   "nat" = µX.< "Zero", "Succ"(X) >)
(SIGNATURES
   "eval#1" :: ["expr"] --> "nat"
   "sub#2" :: ["nat" x "nat"] --> "nat"
   "add#2" :: ["nat" x "nat"] --> "nat"
   "main" :: ["expr"] --> "nat")
(RULES
 "eval#1"("Nat"("v1")) -> "v1"
 "eval#1"("Add"("v2","v1")) -> "add#2"("eval#1"("v2"),"eval#1"("v1"))
 "eval#1"("Sub"("v2","v1")) -> "sub#2"("eval#1"("v2"),"eval#1"("v1"))
 "sub#2"("v8","Zero"()) -> "v8"
 "sub#2"("Zero"(),"Succ"("v16")) -> "Zero"()
 "sub#2"("Succ"("v4"),"Succ"("v2")) -> "sub#2"("v4","v2")
 "add#2"("Zero"(),"v8") -> "v8"
 "add#2"("Succ"("v4"),"v2") -> "Succ"("add#2"("v4","v2"))
 "main"("v12") -> "eval#1"("v12"))


WORST_CASE(?,O(n^2))