YES(O(1), O(n^2)) 8.16/2.54 YES(O(1), O(n^2)) 8.16/2.58 8.16/2.58 8.16/2.58
8.16/2.58 8.16/2.580 CpxTRS8.16/2.58
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))8.16/2.58
↳2 CdtProblem8.16/2.58
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))8.16/2.58
↳4 CdtProblem8.16/2.58
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))8.16/2.58
↳6 CdtProblem8.16/2.58
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))8.16/2.58
↳8 CdtProblem8.16/2.58
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))8.16/2.58
↳10 BOUNDS(O(1), O(1))8.16/2.58
min(X, 0) → X 8.16/2.58
min(s(X), s(Y)) → min(X, Y) 8.16/2.58
quot(0, s(Y)) → 0 8.16/2.58
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y))) 8.16/2.58
log(s(0)) → 0 8.16/2.58
log(s(s(X))) → s(log(s(quot(X, s(s(0))))))
Tuples:
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1) 8.16/2.58
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
log(s(0)) → 0 8.16/2.58
log(s(s(z0))) → s(log(s(quot(z0, s(s(0))))))
S tuples:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
K tuples:none
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
min, quot, log
MIN, QUOT, LOG
c1, c3, c5
We considered the (Usable) Rules:
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
And the Tuples:
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1)
The order we found is given by the following interpretation:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
POL(0) = 0 8.16/2.58
POL(LOG(x1)) = x1 8.16/2.58
POL(MIN(x1, x2)) = 0 8.16/2.58
POL(QUOT(x1, x2)) = 0 8.16/2.58
POL(c1(x1)) = x1 8.16/2.58
POL(c3(x1, x2)) = x1 + x2 8.16/2.58
POL(c5(x1, x2)) = x1 + x2 8.16/2.58
POL(min(x1, x2)) = x1 8.16/2.58
POL(quot(x1, x2)) = x1 8.16/2.58
POL(s(x1)) = [4] + x1
Tuples:
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1) 8.16/2.58
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
log(s(0)) → 0 8.16/2.58
log(s(s(z0))) → s(log(s(quot(z0, s(s(0))))))
S tuples:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
K tuples:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1))
Defined Rule Symbols:
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
min, quot, log
MIN, QUOT, LOG
c1, c3, c5
We considered the (Usable) Rules:
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1))
And the Tuples:
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1)
The order we found is given by the following interpretation:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
POL(0) = 0 8.16/2.58
POL(LOG(x1)) = [2]x1 + [2]x12 8.16/2.58
POL(MIN(x1, x2)) = 0 8.16/2.58
POL(QUOT(x1, x2)) = [2]x1·x2 8.16/2.58
POL(c1(x1)) = x1 8.16/2.58
POL(c3(x1, x2)) = x1 + x2 8.16/2.58
POL(c5(x1, x2)) = x1 + x2 8.16/2.58
POL(min(x1, x2)) = x1 8.16/2.58
POL(quot(x1, x2)) = x1 8.16/2.58
POL(s(x1)) = [2] + x1
Tuples:
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1) 8.16/2.58
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
log(s(0)) → 0 8.16/2.58
log(s(s(z0))) → s(log(s(quot(z0, s(s(0))))))
S tuples:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
K tuples:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1))
Defined Rule Symbols:
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0)))) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1))
min, quot, log
MIN, QUOT, LOG
c1, c3, c5
We considered the (Usable) Rules:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1))
And the Tuples:
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1)
The order we found is given by the following interpretation:
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
POL(0) = 0 8.16/2.58
POL(LOG(x1)) = [2]x1 + [2]x12 8.16/2.58
POL(MIN(x1, x2)) = x2 8.16/2.58
POL(QUOT(x1, x2)) = [2] + [2]x1 + x1·x2 8.16/2.58
POL(c1(x1)) = x1 8.16/2.58
POL(c3(x1, x2)) = x1 + x2 8.16/2.58
POL(c5(x1, x2)) = x1 + x2 8.16/2.58
POL(min(x1, x2)) = x1 8.16/2.58
POL(quot(x1, x2)) = x1 8.16/2.58
POL(s(x1)) = [2] + x1
Tuples:
min(z0, 0) → z0 8.16/2.58
min(s(z0), s(z1)) → min(z0, z1) 8.16/2.58
quot(0, s(z0)) → 0 8.16/2.58
quot(s(z0), s(z1)) → s(quot(min(z0, z1), s(z1))) 8.16/2.58
log(s(0)) → 0 8.16/2.58
log(s(s(z0))) → s(log(s(quot(z0, s(s(0))))))
S tuples:none
MIN(s(z0), s(z1)) → c1(MIN(z0, z1)) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0))))
Defined Rule Symbols:
LOG(s(s(z0))) → c5(LOG(s(quot(z0, s(s(0))))), QUOT(z0, s(s(0)))) 8.16/2.58
QUOT(s(z0), s(z1)) → c3(QUOT(min(z0, z1), s(z1)), MIN(z0, z1)) 8.16/2.58
MIN(s(z0), s(z1)) → c1(MIN(z0, z1))
min, quot, log
MIN, QUOT, LOG
c1, c3, c5