YES(O(1), O(n^2)) 4.11/1.53 YES(O(1), O(n^2)) 4.11/1.57 4.11/1.57 4.11/1.57
4.11/1.57 4.11/1.570 CpxTRS4.11/1.57
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))4.11/1.57
↳2 CdtProblem4.11/1.57
↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID))4.11/1.57
↳4 CdtProblem4.11/1.57
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))4.11/1.57
↳6 CdtProblem4.11/1.57
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))4.11/1.57
↳8 CdtProblem4.11/1.57
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))4.11/1.57
↳10 CdtProblem4.11/1.57
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))4.11/1.57
↳12 CdtProblem4.11/1.57
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))4.11/1.57
↳14 CdtProblem4.11/1.57
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))4.11/1.57
↳16 CdtProblem4.11/1.57
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID))4.11/1.57
↳18 BOUNDS(O(1), O(1))4.11/1.57
half(0) → 0 4.11/1.57
half(s(0)) → 0 4.11/1.57
half(s(s(x))) → s(half(x)) 4.11/1.57
lastbit(0) → 0 4.11/1.57
lastbit(s(0)) → s(0) 4.11/1.57
lastbit(s(s(x))) → lastbit(x) 4.11/1.57
conv(0) → cons(nil, 0) 4.11/1.57
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
Tuples:
half(0) → 0 4.11/1.57
half(s(0)) → 0 4.11/1.57
half(s(s(z0))) → s(half(z0)) 4.11/1.57
lastbit(0) → 0 4.11/1.57
lastbit(s(0)) → s(0) 4.11/1.57
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.57
conv(0) → cons(nil, 0) 4.11/1.57
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(z0)) → c7(CONV(half(s(z0))), HALF(s(z0)), LASTBIT(s(z0)))
K tuples:none
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(z0)) → c7(CONV(half(s(z0))), HALF(s(z0)), LASTBIT(s(z0)))
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7
CONV(s(0)) → c7(CONV(0), HALF(s(0)), LASTBIT(s(0))) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Tuples:
half(0) → 0 4.11/1.57
half(s(0)) → 0 4.11/1.57
half(s(s(z0))) → s(half(z0)) 4.11/1.57
lastbit(0) → 0 4.11/1.57
lastbit(s(0)) → s(0) 4.11/1.57
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.57
conv(0) → cons(nil, 0) 4.11/1.57
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(0)) → c7(CONV(0), HALF(s(0)), LASTBIT(s(0))) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
K tuples:none
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(0)) → c7(CONV(0), HALF(s(0)), LASTBIT(s(0))) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7
Tuples:
half(0) → 0 4.11/1.57
half(s(0)) → 0 4.11/1.57
half(s(s(z0))) → s(half(z0)) 4.11/1.57
lastbit(0) → 0 4.11/1.57
lastbit(s(0)) → s(0) 4.11/1.57
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.57
conv(0) → cons(nil, 0) 4.11/1.57
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.57
CONV(s(0)) → c7
K tuples:none
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.57
CONV(s(0)) → c7
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7
CONV(s(0)) → c7
Tuples:
half(0) → 0 4.11/1.57
half(s(0)) → 0 4.11/1.57
half(s(s(z0))) → s(half(z0)) 4.11/1.57
lastbit(0) → 0 4.11/1.57
lastbit(s(0)) → s(0) 4.11/1.57
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.57
conv(0) → cons(nil, 0) 4.11/1.57
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.57
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.57
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.57
CONV(s(0)) → c7
K tuples:none
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7
We considered the (Usable) Rules:
CONV(s(0)) → c7
And the Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
POL(0) = [2] 4.11/1.58
POL(CONV(x1)) = [1] 4.11/1.58
POL(HALF(x1)) = 0 4.11/1.58
POL(LASTBIT(x1)) = 0 4.11/1.58
POL(c2(x1)) = x1 4.11/1.58
POL(c5(x1)) = x1 4.11/1.58
POL(c7) = 0 4.11/1.58
POL(c7(x1, x2, x3)) = x1 + x2 + x3 4.11/1.58
POL(half(x1)) = [2] + [2]x1 4.11/1.58
POL(s(x1)) = [4]
Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0)) 4.11/1.58
lastbit(0) → 0 4.11/1.58
lastbit(s(0)) → s(0) 4.11/1.58
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.58
conv(0) → cons(nil, 0) 4.11/1.58
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
K tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:
CONV(s(0)) → c7
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7
We considered the (Usable) Rules:
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
And the Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
POL(0) = 0 4.11/1.58
POL(CONV(x1)) = x1 4.11/1.58
POL(HALF(x1)) = 0 4.11/1.58
POL(LASTBIT(x1)) = 0 4.11/1.58
POL(c2(x1)) = x1 4.11/1.58
POL(c5(x1)) = x1 4.11/1.58
POL(c7) = 0 4.11/1.58
POL(c7(x1, x2, x3)) = x1 + x2 + x3 4.11/1.58
POL(half(x1)) = x1 4.11/1.58
POL(s(x1)) = [4] + x1
Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0)) 4.11/1.58
lastbit(0) → 0 4.11/1.58
lastbit(s(0)) → s(0) 4.11/1.58
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.58
conv(0) → cons(nil, 0) 4.11/1.58
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
K tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
Defined Rule Symbols:
CONV(s(0)) → c7 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0))))
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7
We considered the (Usable) Rules:
HALF(s(s(z0))) → c2(HALF(z0))
And the Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
POL(0) = 0 4.11/1.58
POL(CONV(x1)) = x12 4.11/1.58
POL(HALF(x1)) = x1 4.11/1.58
POL(LASTBIT(x1)) = 0 4.11/1.58
POL(c2(x1)) = x1 4.11/1.58
POL(c5(x1)) = x1 4.11/1.58
POL(c7) = 0 4.11/1.58
POL(c7(x1, x2, x3)) = x1 + x2 + x3 4.11/1.58
POL(half(x1)) = x1 4.11/1.58
POL(s(x1)) = [1] + x1
Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0)) 4.11/1.58
lastbit(0) → 0 4.11/1.58
lastbit(s(0)) → s(0) 4.11/1.58
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.58
conv(0) → cons(nil, 0) 4.11/1.58
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
K tuples:
LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
Defined Rule Symbols:
CONV(s(0)) → c7 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
HALF(s(s(z0))) → c2(HALF(z0))
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7
We considered the (Usable) Rules:
LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
And the Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0))
The order we found is given by the following interpretation:
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
POL(0) = 0 4.11/1.58
POL(CONV(x1)) = x12 4.11/1.58
POL(HALF(x1)) = 0 4.11/1.58
POL(LASTBIT(x1)) = [2]x1 4.11/1.58
POL(c2(x1)) = x1 4.11/1.58
POL(c5(x1)) = x1 4.11/1.58
POL(c7) = 0 4.11/1.58
POL(c7(x1, x2, x3)) = x1 + x2 + x3 4.11/1.58
POL(half(x1)) = x1 4.11/1.58
POL(s(x1)) = [2] + x1
Tuples:
half(0) → 0 4.11/1.58
half(s(0)) → 0 4.11/1.58
half(s(s(z0))) → s(half(z0)) 4.11/1.58
lastbit(0) → 0 4.11/1.58
lastbit(s(0)) → s(0) 4.11/1.58
lastbit(s(s(z0))) → lastbit(z0) 4.11/1.58
conv(0) → cons(nil, 0) 4.11/1.58
conv(s(z0)) → cons(conv(half(s(z0))), lastbit(s(z0)))
S tuples:none
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
CONV(s(0)) → c7
Defined Rule Symbols:
CONV(s(0)) → c7 4.11/1.58
CONV(s(s(z0))) → c7(CONV(s(half(z0))), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 4.11/1.58
HALF(s(s(z0))) → c2(HALF(z0)) 4.11/1.58
LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
half, lastbit, conv
HALF, LASTBIT, CONV
c2, c5, c7, c7