YES(O(1), O(n^2)) 0.00/0.96 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 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/1.00
↳4 CdtProblem0.00/1.00
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/1.00
↳6 CdtProblem0.00/1.00
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/1.00
↳8 CdtProblem0.00/1.00
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/1.00
↳10 BOUNDS(O(1), O(1))0.00/1.00
pred(s(x)) → x 0.00/1.00
minus(x, 0) → x 0.00/1.00
minus(x, s(y)) → pred(minus(x, y)) 0.00/1.00
quot(0, s(y)) → 0 0.00/1.00
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
Tuples:
pred(s(z0)) → z0 0.00/1.00
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
quot(0, s(z0)) → 0 0.00/1.00
quot(s(z0), s(z1)) → s(quot(minus(z0, z1), s(z1)))
S tuples:
MINUS(z0, s(z1)) → c2(PRED(minus(z0, z1)), MINUS(z0, z1)) 0.00/1.00
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
MINUS(z0, s(z1)) → c2(PRED(minus(z0, z1)), MINUS(z0, z1)) 0.00/1.00
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
pred, minus, quot
MINUS, QUOT
c2, c4
Tuples:
pred(s(z0)) → z0 0.00/1.00
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
quot(0, s(z0)) → 0 0.00/1.00
quot(s(z0), s(z1)) → s(quot(minus(z0, z1), s(z1)))
S tuples:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
K tuples:none
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
pred, minus, quot
QUOT, MINUS
c4, c2
We considered the (Usable) Rules:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
And the Tuples:
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
pred(s(z0)) → z0
The order we found is given by the following interpretation:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
POL(0) = 0 0.00/1.00
POL(MINUS(x1, x2)) = [1] 0.00/1.00
POL(QUOT(x1, x2)) = [2]x1 0.00/1.00
POL(c2(x1)) = x1 0.00/1.00
POL(c4(x1, x2)) = x1 + x2 0.00/1.00
POL(minus(x1, x2)) = x1 0.00/1.00
POL(pred(x1)) = x1 0.00/1.00
POL(s(x1)) = [1] + x1
Tuples:
pred(s(z0)) → z0 0.00/1.00
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
quot(0, s(z0)) → 0 0.00/1.00
quot(s(z0), s(z1)) → s(quot(minus(z0, z1), s(z1)))
S tuples:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
K tuples:
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
Defined Rule Symbols:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
pred, minus, quot
QUOT, MINUS
c4, c2
We considered the (Usable) Rules:
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
And the Tuples:
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
pred(s(z0)) → z0
The order we found is given by the following interpretation:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
POL(0) = [3] 0.00/1.00
POL(MINUS(x1, x2)) = [1] + x2 0.00/1.00
POL(QUOT(x1, x2)) = x1·x2 0.00/1.00
POL(c2(x1)) = x1 0.00/1.00
POL(c4(x1, x2)) = x1 + x2 0.00/1.00
POL(minus(x1, x2)) = x1 0.00/1.00
POL(pred(x1)) = x1 0.00/1.00
POL(s(x1)) = [1] + x1
Tuples:
pred(s(z0)) → z0 0.00/1.00
minus(z0, 0) → z0 0.00/1.00
minus(z0, s(z1)) → pred(minus(z0, z1)) 0.00/1.00
quot(0, s(z0)) → 0 0.00/1.00
quot(s(z0), s(z1)) → s(quot(minus(z0, z1), s(z1)))
S tuples:none
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
Defined Rule Symbols:
QUOT(s(z0), s(z1)) → c4(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) 0.00/1.00
MINUS(z0, s(z1)) → c2(MINUS(z0, z1))
pred, minus, quot
QUOT, MINUS
c4, c2