YES(O(1), O(n^1)) 0.00/0.82 YES(O(1), O(n^1)) 0.00/0.84 0.00/0.84 0.00/0.84
0.00/0.84 0.00/0.840 CpxTRS0.00/0.84
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳2 CdtProblem0.00/0.84
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳4 CdtProblem0.00/0.84
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.84
↳6 CdtProblem0.00/0.84
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.84
↳8 CdtProblem0.00/0.84
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.84
↳10 CdtProblem0.00/0.84
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳12 BOUNDS(O(1), O(1))0.00/0.84
not(true) → false 0.00/0.84
not(false) → true 0.00/0.84
odd(0) → false 0.00/0.84
odd(s(x)) → not(odd(x)) 0.00/0.84
+(x, 0) → x 0.00/0.84
+(x, s(y)) → s(+(x, y)) 0.00/0.84
+(s(x), y) → s(+(x, y))
Tuples:
not(true) → false 0.00/0.84
not(false) → true 0.00/0.84
odd(0) → false 0.00/0.84
odd(s(z0)) → not(odd(z0)) 0.00/0.84
+(z0, 0) → z0 0.00/0.84
+(z0, s(z1)) → s(+(z0, z1)) 0.00/0.84
+(s(z0), z1) → s(+(z0, z1))
S tuples:
ODD(s(z0)) → c3(NOT(odd(z0)), ODD(z0)) 0.00/0.84
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1))
K tuples:none
ODD(s(z0)) → c3(NOT(odd(z0)), ODD(z0)) 0.00/0.84
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1))
not, odd, +
ODD, +'
c3, c5, c6
Tuples:
not(true) → false 0.00/0.84
not(false) → true 0.00/0.84
odd(0) → false 0.00/0.84
odd(s(z0)) → not(odd(z0)) 0.00/0.84
+(z0, 0) → z0 0.00/0.84
+(z0, s(z1)) → s(+(z0, z1)) 0.00/0.84
+(s(z0), z1) → s(+(z0, z1))
S tuples:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
K tuples:none
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
not, odd, +
+', ODD
c5, c6, c3
We considered the (Usable) Rules:none
+'(z0, s(z1)) → c5(+'(z0, z1))
The order we found is given by the following interpretation:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
POL(+'(x1, x2)) = x2 0.00/0.84
POL(ODD(x1)) = 0 0.00/0.84
POL(c3(x1)) = x1 0.00/0.84
POL(c5(x1)) = x1 0.00/0.84
POL(c6(x1)) = x1 0.00/0.84
POL(s(x1)) = [1] + x1
Tuples:
not(true) → false 0.00/0.84
not(false) → true 0.00/0.84
odd(0) → false 0.00/0.84
odd(s(z0)) → not(odd(z0)) 0.00/0.84
+(z0, 0) → z0 0.00/0.84
+(z0, s(z1)) → s(+(z0, z1)) 0.00/0.84
+(s(z0), z1) → s(+(z0, z1))
S tuples:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
K tuples:
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
Defined Rule Symbols:
+'(z0, s(z1)) → c5(+'(z0, z1))
not, odd, +
+', ODD
c5, c6, c3
We considered the (Usable) Rules:none
+'(s(z0), z1) → c6(+'(z0, z1))
The order we found is given by the following interpretation:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
POL(+'(x1, x2)) = x1 + [5]x2 0.00/0.84
POL(ODD(x1)) = 0 0.00/0.84
POL(c3(x1)) = x1 0.00/0.84
POL(c5(x1)) = x1 0.00/0.84
POL(c6(x1)) = x1 0.00/0.84
POL(s(x1)) = [1] + x1
Tuples:
not(true) → false 0.00/0.84
not(false) → true 0.00/0.84
odd(0) → false 0.00/0.84
odd(s(z0)) → not(odd(z0)) 0.00/0.84
+(z0, 0) → z0 0.00/0.84
+(z0, s(z1)) → s(+(z0, z1)) 0.00/0.84
+(s(z0), z1) → s(+(z0, z1))
S tuples:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.84
ODD(s(z0)) → c3(ODD(z0))
K tuples:
ODD(s(z0)) → c3(ODD(z0))
Defined Rule Symbols:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.84
+'(s(z0), z1) → c6(+'(z0, z1))
not, odd, +
+', ODD
c5, c6, c3
We considered the (Usable) Rules:none
ODD(s(z0)) → c3(ODD(z0))
The order we found is given by the following interpretation:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.85
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.85
ODD(s(z0)) → c3(ODD(z0))
POL(+'(x1, x2)) = [5]x1 + [5]x2 0.00/0.85
POL(ODD(x1)) = [3]x1 0.00/0.85
POL(c3(x1)) = x1 0.00/0.85
POL(c5(x1)) = x1 0.00/0.85
POL(c6(x1)) = x1 0.00/0.85
POL(s(x1)) = [1] + x1
Tuples:
not(true) → false 0.00/0.85
not(false) → true 0.00/0.85
odd(0) → false 0.00/0.85
odd(s(z0)) → not(odd(z0)) 0.00/0.85
+(z0, 0) → z0 0.00/0.85
+(z0, s(z1)) → s(+(z0, z1)) 0.00/0.85
+(s(z0), z1) → s(+(z0, z1))
S tuples:none
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.85
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.85
ODD(s(z0)) → c3(ODD(z0))
Defined Rule Symbols:
+'(z0, s(z1)) → c5(+'(z0, z1)) 0.00/0.85
+'(s(z0), z1) → c6(+'(z0, z1)) 0.00/0.85
ODD(s(z0)) → c3(ODD(z0))
not, odd, +
+', ODD
c5, c6, c3