YES(O(1), O(n^2)) 3.64/1.32 YES(O(1), O(n^2)) 3.64/1.35 3.64/1.35 3.64/1.35
3.64/1.35 3.64/1.350 CpxTRS3.64/1.35
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))3.64/1.35
↳2 CdtProblem3.64/1.35
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.64/1.35
↳4 CdtProblem3.64/1.35
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))3.64/1.35
↳6 CdtProblem3.64/1.35
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))3.64/1.35
↳8 BOUNDS(O(1), O(1))3.64/1.35
plus(plus(X, Y), Z) → plus(X, plus(Y, Z)) 3.64/1.35
times(X, s(Y)) → plus(X, times(Y, X))
Tuples:
plus(plus(z0, z1), z2) → plus(z0, plus(z1, z2)) 3.64/1.35
times(z0, s(z1)) → plus(z0, times(z1, z0))
S tuples:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
K tuples:none
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
plus, times
PLUS, TIMES
c, c1
We considered the (Usable) Rules:
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
And the Tuples:
times(z0, s(z1)) → plus(z0, times(z1, z0)) 3.64/1.35
plus(plus(z0, z1), z2) → plus(z0, plus(z1, z2))
The order we found is given by the following interpretation:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
POL(PLUS(x1, x2)) = 0 3.64/1.35
POL(TIMES(x1, x2)) = [5]x1 + [5]x2 3.64/1.35
POL(c(x1, x2)) = x1 + x2 3.64/1.35
POL(c1(x1, x2)) = x1 + x2 3.64/1.35
POL(plus(x1, x2)) = [3] + x2 3.64/1.35
POL(s(x1)) = [3] + x1 3.64/1.35
POL(times(x1, x2)) = [5] + [5]x1 + [5]x2
Tuples:
plus(plus(z0, z1), z2) → plus(z0, plus(z1, z2)) 3.64/1.35
times(z0, s(z1)) → plus(z0, times(z1, z0))
S tuples:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
K tuples:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2))
Defined Rule Symbols:
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
plus, times
PLUS, TIMES
c, c1
We considered the (Usable) Rules:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2))
And the Tuples:
times(z0, s(z1)) → plus(z0, times(z1, z0)) 3.64/1.35
plus(plus(z0, z1), z2) → plus(z0, plus(z1, z2))
The order we found is given by the following interpretation:
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
POL(PLUS(x1, x2)) = x1 3.64/1.35
POL(TIMES(x1, x2)) = [2]x1 + [3]x2 + x1·x2 3.64/1.35
POL(c(x1, x2)) = x1 + x2 3.64/1.35
POL(c1(x1, x2)) = x1 + x2 3.64/1.35
POL(plus(x1, x2)) = [1] + [2]x1 + x2 3.64/1.35
POL(s(x1)) = [3] + x1 3.64/1.35
POL(times(x1, x2)) = 0
Tuples:
plus(plus(z0, z1), z2) → plus(z0, plus(z1, z2)) 3.64/1.35
times(z0, s(z1)) → plus(z0, times(z1, z0))
S tuples:none
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2)) 3.64/1.35
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0))
Defined Rule Symbols:
TIMES(z0, s(z1)) → c1(PLUS(z0, times(z1, z0)), TIMES(z1, z0)) 3.64/1.35
PLUS(plus(z0, z1), z2) → c(PLUS(z0, plus(z1, z2)), PLUS(z1, z2))
plus, times
PLUS, TIMES
c, c1