YES(O(1), O(n^3)) 13.90/4.41 YES(O(1), O(n^3)) 13.90/4.44 13.90/4.44 13.90/4.44
13.90/4.44 13.90/4.440 CpxTRS13.90/4.44
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))13.90/4.44
↳2 CdtProblem13.90/4.44
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))13.90/4.44
↳4 CdtProblem13.90/4.44
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))13.90/4.44
↳6 CdtProblem13.90/4.44
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))13.90/4.44
↳8 CdtProblem13.90/4.44
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))13.90/4.44
↳10 CdtProblem13.90/4.44
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))13.90/4.44
↳12 BOUNDS(O(1), O(1))13.90/4.44
+(0, y) → y 13.90/4.44
+(s(x), y) → s(+(x, y)) 13.90/4.44
+(p(x), y) → p(+(x, y)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(x)) → p(minus(x)) 13.90/4.44
minus(p(x)) → s(minus(x)) 13.90/4.44
*(0, y) → 0 13.90/4.44
*(s(x), y) → +(*(x, y), y) 13.90/4.44
*(p(x), y) → +(*(x, y), minus(y))
Tuples:
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:none
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
And the Tuples:
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = 0 13.90/4.44
POL(*'(x1, x2)) = [4]x1 13.90/4.44
POL(+(x1, x2)) = [3] 13.90/4.44
POL(+'(x1, x2)) = 0 13.90/4.44
POL(0) = [3] 13.90/4.44
POL(MINUS(x1)) = 0 13.90/4.44
POL(c1(x1)) = x1 13.90/4.44
POL(c2(x1)) = x1 13.90/4.44
POL(c4(x1)) = x1 13.90/4.44
POL(c5(x1)) = x1 13.90/4.44
POL(c7(x1, x2)) = x1 + x2 13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3 13.90/4.44
POL(minus(x1)) = 0 13.90/4.44
POL(p(x1)) = x1 13.90/4.44
POL(s(x1)) = [1] + x1
Tuples:
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
And the Tuples:
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = 0 13.90/4.44
POL(*'(x1, x2)) = x1 13.90/4.44
POL(+(x1, x2)) = [3] 13.90/4.44
POL(+'(x1, x2)) = [1] 13.90/4.44
POL(0) = 0 13.90/4.44
POL(MINUS(x1)) = 0 13.90/4.44
POL(c1(x1)) = x1 13.90/4.44
POL(c2(x1)) = x1 13.90/4.44
POL(c4(x1)) = x1 13.90/4.44
POL(c5(x1)) = x1 13.90/4.44
POL(c7(x1, x2)) = x1 + x2 13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3 13.90/4.44
POL(minus(x1)) = [4] + [5]x1 13.90/4.44
POL(p(x1)) = [4] + x1 13.90/4.44
POL(s(x1)) = [1] + x1
Tuples:
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
And the Tuples:
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = [3]x22 13.90/4.44
POL(*'(x1, x2)) = [3]x1 + x1·x2 + x12 13.90/4.44
POL(+(x1, x2)) = [3] 13.90/4.44
POL(+'(x1, x2)) = [2] 13.90/4.44
POL(0) = 0 13.90/4.44
POL(MINUS(x1)) = [2] + [2]x1 13.90/4.44
POL(c1(x1)) = x1 13.90/4.44
POL(c2(x1)) = x1 13.90/4.44
POL(c4(x1)) = x1 13.90/4.44
POL(c5(x1)) = x1 13.90/4.44
POL(c7(x1, x2)) = x1 + x2 13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3 13.90/4.44
POL(minus(x1)) = 0 13.90/4.44
POL(p(x1)) = [2] + x1 13.90/4.44
POL(s(x1)) = [1] + x1
Tuples:
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
And the Tuples:
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = x1·x2 13.90/4.44
POL(*'(x1, x2)) = x12·x2 13.90/4.44
POL(+(x1, x2)) = x1 + x2 13.90/4.44
POL(+'(x1, x2)) = x1 13.90/4.44
POL(0) = 0 13.90/4.44
POL(MINUS(x1)) = 0 13.90/4.44
POL(c1(x1)) = x1 13.90/4.44
POL(c2(x1)) = x1 13.90/4.44
POL(c4(x1)) = x1 13.90/4.44
POL(c5(x1)) = x1 13.90/4.44
POL(c7(x1, x2)) = x1 + x2 13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3 13.90/4.44
POL(minus(x1)) = x1 13.90/4.44
POL(p(x1)) = [1] + x1 13.90/4.44
POL(s(x1)) = [1] + x1
Tuples:
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:none
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8