YES(O(1), O(n^2)) 0.00/0.99 YES(O(1), O(n^2)) 0.00/1.00 0.00/1.00 0.00/1.00
0.00/1.00 0.00/1.000 CpxTRS0.00/1.00
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/1.00
↳2 CdtProblem0.00/1.00
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/1.00
↳4 CdtProblem0.00/1.00
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/1.00
↳6 CdtProblem0.00/1.00
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/1.00
↳8 BOUNDS(O(1), O(1))0.00/1.00
sum(0) → 0 0.00/1.00
sum(s(x)) → +(sum(x), s(x)) 0.00/1.00
+(x, 0) → x 0.00/1.00
+(x, s(y)) → s(+(x, y))
Tuples:
sum(0) → 0 0.00/1.00
sum(s(z0)) → +(sum(z0), s(z0)) 0.00/1.00
+(z0, 0) → z0 0.00/1.00
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
K tuples:none
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
sum, +
SUM, +'
c1, c3
We considered the (Usable) Rules:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0))
And the Tuples:
sum(0) → 0 0.00/1.00
sum(s(z0)) → +(sum(z0), s(z0)) 0.00/1.00
+(z0, s(z1)) → s(+(z0, z1)) 0.00/1.00
+(z0, 0) → z0
The order we found is given by the following interpretation:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
POL(+(x1, x2)) = [5] 0.00/1.00
POL(+'(x1, x2)) = [3] 0.00/1.00
POL(0) = [3] 0.00/1.00
POL(SUM(x1)) = x1 0.00/1.00
POL(c1(x1, x2)) = x1 + x2 0.00/1.00
POL(c3(x1)) = x1 0.00/1.00
POL(s(x1)) = [4] + x1 0.00/1.00
POL(sum(x1)) = 0
Tuples:
sum(0) → 0 0.00/1.00
sum(s(z0)) → +(sum(z0), s(z0)) 0.00/1.00
+(z0, 0) → z0 0.00/1.00
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
K tuples:
+'(z0, s(z1)) → c3(+'(z0, z1))
Defined Rule Symbols:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0))
sum, +
SUM, +'
c1, c3
We considered the (Usable) Rules:
+'(z0, s(z1)) → c3(+'(z0, z1))
And the Tuples:
sum(0) → 0 0.00/1.00
sum(s(z0)) → +(sum(z0), s(z0)) 0.00/1.00
+(z0, s(z1)) → s(+(z0, z1)) 0.00/1.00
+(z0, 0) → z0
The order we found is given by the following interpretation:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
POL(+(x1, x2)) = [3] + [3]x2 0.00/1.00
POL(+'(x1, x2)) = x2 0.00/1.00
POL(0) = [1] 0.00/1.00
POL(SUM(x1)) = x12 0.00/1.00
POL(c1(x1, x2)) = x1 + x2 0.00/1.00
POL(c3(x1)) = x1 0.00/1.00
POL(s(x1)) = [1] + x1 0.00/1.00
POL(sum(x1)) = 0
Tuples:
sum(0) → 0 0.00/1.00
sum(s(z0)) → +(sum(z0), s(z0)) 0.00/1.00
+(z0, 0) → z0 0.00/1.00
+(z0, s(z1)) → s(+(z0, z1))
S tuples:none
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
Defined Rule Symbols:
SUM(s(z0)) → c1(+'(sum(z0), s(z0)), SUM(z0)) 0.00/1.00
+'(z0, s(z1)) → c3(+'(z0, z1))
sum, +
SUM, +'
c1, c3