YES(O(1), O(n^2)) 2.42/1.05 YES(O(1), O(n^2)) 2.42/1.08 2.42/1.08 2.42/1.08
2.42/1.08 2.42/1.080 CpxTRS2.42/1.08
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.42/1.08
↳2 CdtProblem2.42/1.08
↳3 CdtUnreachableProof (⇔)2.42/1.08
↳4 CdtProblem2.42/1.08
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.42/1.08
↳6 CdtProblem2.42/1.08
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.42/1.08
↳8 CdtProblem2.42/1.08
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.42/1.08
↳10 BOUNDS(O(1), O(1))2.42/1.08
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z))) 2.42/1.08
times(x, 0) → 0 2.42/1.08
times(x, s(y)) → plus(times(x, y), x) 2.42/1.08
plus(x, 0) → x 2.42/1.08
plus(x, s(y)) → s(plus(x, y))
Tuples:
times(z0, plus(z1, s(z2))) → plus(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))) 2.42/1.08
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
S tuples:
TIMES(z0, plus(z1, s(z2))) → c(PLUS(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))), TIMES(z0, plus(z1, times(s(z2), 0))), PLUS(z1, times(s(z2), 0)), TIMES(s(z2), 0), TIMES(z0, s(z2))) 2.42/1.08
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
K tuples:none
TIMES(z0, plus(z1, s(z2))) → c(PLUS(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))), TIMES(z0, plus(z1, times(s(z2), 0))), PLUS(z1, times(s(z2), 0)), TIMES(s(z2), 0), TIMES(z0, s(z2))) 2.42/1.08
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
times, plus
TIMES, PLUS
c, c2, c4
TIMES(z0, plus(z1, s(z2))) → c(PLUS(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))), TIMES(z0, plus(z1, times(s(z2), 0))), PLUS(z1, times(s(z2), 0)), TIMES(s(z2), 0), TIMES(z0, s(z2)))
Tuples:
times(z0, plus(z1, s(z2))) → plus(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))) 2.42/1.08
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
S tuples:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
K tuples:none
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
times, plus
TIMES, PLUS
c2, c4
We considered the (Usable) Rules:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1))
And the Tuples:
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
The order we found is given by the following interpretation:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
POL(0) = [3] 2.42/1.08
POL(PLUS(x1, x2)) = [1] 2.42/1.08
POL(TIMES(x1, x2)) = [4]x2 2.42/1.08
POL(c2(x1, x2)) = x1 + x2 2.42/1.08
POL(c4(x1)) = x1 2.42/1.08
POL(plus(x1, x2)) = [5] 2.42/1.08
POL(s(x1)) = [1] + x1 2.42/1.08
POL(times(x1, x2)) = 0
Tuples:
times(z0, plus(z1, s(z2))) → plus(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))) 2.42/1.08
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
S tuples:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
K tuples:
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
Defined Rule Symbols:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1))
times, plus
TIMES, PLUS
c2, c4
We considered the (Usable) Rules:
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
And the Tuples:
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
The order we found is given by the following interpretation:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
POL(0) = [1] 2.42/1.08
POL(PLUS(x1, x2)) = [2]x2 2.42/1.08
POL(TIMES(x1, x2)) = x22 + x1·x2 2.42/1.08
POL(c2(x1, x2)) = x1 + x2 2.42/1.08
POL(c4(x1)) = x1 2.42/1.08
POL(plus(x1, x2)) = [1] + x1 + [3]x2 2.42/1.08
POL(s(x1)) = [3] + x1 2.42/1.08
POL(times(x1, x2)) = [1] + [2]x1 + x2 + x22 + [2]x1·x2
Tuples:
times(z0, plus(z1, s(z2))) → plus(times(z0, plus(z1, times(s(z2), 0))), times(z0, s(z2))) 2.42/1.08
times(z0, 0) → 0 2.42/1.08
times(z0, s(z1)) → plus(times(z0, z1), z0) 2.42/1.08
plus(z0, 0) → z0 2.42/1.08
plus(z0, s(z1)) → s(plus(z0, z1))
S tuples:none
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
Defined Rule Symbols:
TIMES(z0, s(z1)) → c2(PLUS(times(z0, z1), z0), TIMES(z0, z1)) 2.42/1.08
PLUS(z0, s(z1)) → c4(PLUS(z0, z1))
times, plus
TIMES, PLUS
c2, c4