YES(O(1), O(n^2)) 0.00/1.00 YES(O(1), O(n^2)) 0.00/1.02 0.00/1.02 0.00/1.02
0.00/1.02 0.00/1.020 CpxTRS0.00/1.02
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/1.02
↳2 CdtProblem0.00/1.02
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/1.02
↳4 CdtProblem0.00/1.02
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/1.02
↳6 CdtProblem0.00/1.02
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/1.02
↳8 CdtProblem0.00/1.02
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/1.02
↳10 BOUNDS(O(1), O(1))0.00/1.02
minus(X, 0) → X 0.00/1.02
minus(s(X), s(Y)) → p(minus(X, Y)) 0.00/1.02
p(s(X)) → X 0.00/1.02
div(0, s(Y)) → 0 0.00/1.02
div(s(X), s(Y)) → s(div(minus(X, Y), s(Y)))
Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0 0.00/1.02
div(0, s(z0)) → 0 0.00/1.02
div(s(z0), s(z1)) → s(div(minus(z0, z1), s(z1)))
S tuples:
MINUS(s(z0), s(z1)) → c1(P(minus(z0, z1)), MINUS(z0, z1)) 0.00/1.02
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
MINUS(s(z0), s(z1)) → c1(P(minus(z0, z1)), MINUS(z0, z1)) 0.00/1.02
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1))
minus, p, div
MINUS, DIV
c1, c4
Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0 0.00/1.02
div(0, s(z0)) → 0 0.00/1.02
div(s(z0), s(z1)) → s(div(minus(z0, z1), s(z1)))
S tuples:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
K tuples:none
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
minus, p, div
DIV, MINUS
c4, c1
We considered the (Usable) Rules:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1))
And the Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0
The order we found is given by the following interpretation:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
POL(0) = 0 0.00/1.02
POL(DIV(x1, x2)) = [2]x1 0.00/1.02
POL(MINUS(x1, x2)) = 0 0.00/1.02
POL(c1(x1)) = x1 0.00/1.02
POL(c4(x1, x2)) = x1 + x2 0.00/1.02
POL(minus(x1, x2)) = x1 0.00/1.02
POL(p(x1)) = x1 0.00/1.02
POL(s(x1)) = [1] + x1
Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0 0.00/1.02
div(0, s(z0)) → 0 0.00/1.02
div(s(z0), s(z1)) → s(div(minus(z0, z1), s(z1)))
S tuples:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
K tuples:
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
Defined Rule Symbols:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1))
minus, p, div
DIV, MINUS
c4, c1
We considered the (Usable) Rules:
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
And the Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0
The order we found is given by the following interpretation:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
POL(0) = [3] 0.00/1.02
POL(DIV(x1, x2)) = x12 0.00/1.02
POL(MINUS(x1, x2)) = x1 0.00/1.02
POL(c1(x1)) = x1 0.00/1.02
POL(c4(x1, x2)) = x1 + x2 0.00/1.02
POL(minus(x1, x2)) = x1 0.00/1.02
POL(p(x1)) = x1 0.00/1.02
POL(s(x1)) = [2] + x1
Tuples:
minus(z0, 0) → z0 0.00/1.02
minus(s(z0), s(z1)) → p(minus(z0, z1)) 0.00/1.02
p(s(z0)) → z0 0.00/1.02
div(0, s(z0)) → 0 0.00/1.02
div(s(z0), s(z1)) → s(div(minus(z0, z1), s(z1)))
S tuples:none
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
Defined Rule Symbols:
DIV(s(z0), s(z1)) → c4(DIV(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.02
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))
minus, p, div
DIV, MINUS
c4, c1