YES(O(1), O(n^2)) 0.00/0.88 YES(O(1), O(n^2)) 0.00/0.89 0.00/0.89 0.00/0.89
0.00/0.89 0.00/0.890 CpxTRS0.00/0.89
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.89
↳2 CdtProblem0.00/0.89
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.89
↳4 CdtProblem0.00/0.89
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/0.89
↳6 CdtProblem0.00/0.89
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.89
↳8 BOUNDS(O(1), O(1))0.00/0.89
half(0) → 0 0.00/0.89
half(s(s(x))) → s(half(x)) 0.00/0.89
log(s(0)) → 0 0.00/0.89
log(s(s(x))) → s(log(s(half(x))))
Tuples:
half(0) → 0 0.00/0.89
half(s(s(z0))) → s(half(z0)) 0.00/0.89
log(s(0)) → 0 0.00/0.89
log(s(s(z0))) → s(log(s(half(z0))))
S tuples:
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
K tuples:none
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
half, log
HALF, LOG
c1, c3
We considered the (Usable) Rules:
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
And the Tuples:
half(0) → 0 0.00/0.89
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
POL(0) = 0 0.00/0.89
POL(HALF(x1)) = 0 0.00/0.89
POL(LOG(x1)) = x1 0.00/0.89
POL(c1(x1)) = x1 0.00/0.89
POL(c3(x1, x2)) = x1 + x2 0.00/0.89
POL(half(x1)) = x1 0.00/0.89
POL(s(x1)) = [4] + x1
Tuples:
half(0) → 0 0.00/0.89
half(s(s(z0))) → s(half(z0)) 0.00/0.89
log(s(0)) → 0 0.00/0.89
log(s(s(z0))) → s(log(s(half(z0))))
S tuples:
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
K tuples:
HALF(s(s(z0))) → c1(HALF(z0))
Defined Rule Symbols:
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
half, log
HALF, LOG
c1, c3
We considered the (Usable) Rules:
HALF(s(s(z0))) → c1(HALF(z0))
And the Tuples:
half(0) → 0 0.00/0.89
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
POL(0) = 0 0.00/0.89
POL(HALF(x1)) = x1 0.00/0.89
POL(LOG(x1)) = x12 0.00/0.89
POL(c1(x1)) = x1 0.00/0.89
POL(c3(x1, x2)) = x1 + x2 0.00/0.89
POL(half(x1)) = x1 0.00/0.89
POL(s(x1)) = [1] + x1
Tuples:
half(0) → 0 0.00/0.89
half(s(s(z0))) → s(half(z0)) 0.00/0.89
log(s(0)) → 0 0.00/0.89
log(s(s(z0))) → s(log(s(half(z0))))
S tuples:none
HALF(s(s(z0))) → c1(HALF(z0)) 0.00/0.89
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0))
Defined Rule Symbols:
LOG(s(s(z0))) → c3(LOG(s(half(z0))), HALF(z0)) 0.00/0.89
HALF(s(s(z0))) → c1(HALF(z0))
half, log
HALF, LOG
c1, c3