YES(O(1), O(n^1)) 0.00/0.71 YES(O(1), O(n^1)) 0.00/0.72 0.00/0.72 0.00/0.72
0.00/0.72 0.00/0.720 CpxTRS0.00/0.72
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.72
↳2 CdtProblem0.00/0.72
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.72
↳4 CdtProblem0.00/0.72
↳5 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.72
↳6 BOUNDS(O(1), O(1))0.00/0.72
odd(S(x)) → even(x) 0.00/0.72
even(S(x)) → odd(x) 0.00/0.72
odd(0) → 0 0.00/0.72
even(0) → S(0)
Tuples:
odd(S(z0)) → even(z0) 0.00/0.72
odd(0) → 0 0.00/0.72
even(S(z0)) → odd(z0) 0.00/0.72
even(0) → S(0)
S tuples:
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
K tuples:none
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
odd, even
ODD, EVEN
c, c2
We considered the (Usable) Rules:none
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
The order we found is given by the following interpretation:
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
POL(EVEN(x1)) = [2] + [2]x1 0.00/0.72
POL(ODD(x1)) = [4] + [2]x1 0.00/0.72
POL(S(x1)) = [4] + x1 0.00/0.72
POL(c(x1)) = x1 0.00/0.72
POL(c2(x1)) = x1
Tuples:
odd(S(z0)) → even(z0) 0.00/0.72
odd(0) → 0 0.00/0.72
even(S(z0)) → odd(z0) 0.00/0.72
even(0) → S(0)
S tuples:none
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
Defined Rule Symbols:
ODD(S(z0)) → c(EVEN(z0)) 0.00/0.72
EVEN(S(z0)) → c2(ODD(z0))
odd, even
ODD, EVEN
c, c2