YES(O(1), O(n^1)) 14.63/6.86 YES(O(1), O(n^1)) 14.63/6.88 14.63/6.88 14.63/6.88
14.63/6.88 14.63/6.880 CpxTRS14.63/6.88
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳2 CdtProblem14.63/6.88
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳4 CdtProblem14.63/6.88
↳5 CdtInstantiationProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳6 CdtProblem14.63/6.88
↳7 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳8 CdtProblem14.63/6.88
↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication)14.63/6.88
↳10 CdtProblem14.63/6.88
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳12 CdtProblem14.63/6.88
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳14 CdtProblem14.63/6.88
↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))14.63/6.88
↳16 CdtProblem14.63/6.88
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))14.63/6.88
↳18 CdtProblem14.63/6.88
↳19 CdtKnowledgeProof (⇔)14.63/6.88
↳20 BOUNDS(O(1), O(1))14.63/6.88
c(c(b(c(x)))) → b(a(0, c(x))) 14.63/6.88
c(c(x)) → b(c(b(c(x)))) 14.63/6.88
a(0, x) → c(c(x))
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.88
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.88
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(b(c(z0))), C(z0)) 14.63/6.88
A(0, z0) → c3(C(c(z0)), C(z0))
K tuples:none
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(b(c(z0))), C(z0)) 14.63/6.88
A(0, z0) → c3(C(c(z0)), C(z0))
c, a
C, A
c1, c2, c3
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.88
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.88
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
A(0, z0) → c3(C(c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(z0))
K tuples:none
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
A(0, z0) → c3(C(c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(z0))
c, a
C, A
c1, c3, c2
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.88
A1(0, z0) → c3(C(c(z0)), C(z0))
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.88
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.88
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(z0)) 14.63/6.88
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.88
A1(0, z0) → c3(C(c(z0)), C(z0))
K tuples:none
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.88
C(c(z0)) → c2(C(z0)) 14.63/6.88
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.88
A1(0, z0) → c3(C(c(z0)), C(z0))
c, a
C, A, A1
c1, c2, c3
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.89
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.89
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.89
A1(0, z0) → c4(C(c(z0))) 14.63/6.89
A1(0, z0) → c4(C(z0))
K tuples:none
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.89
A1(0, z0) → c4(C(c(z0))) 14.63/6.89
A1(0, z0) → c4(C(z0))
c, a
C, A, A1
c1, c2, c3, c4
A1(0, z0) → c4(C(z0))
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.89
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.89
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.89
A1(0, z0) → c4(C(c(z0)))
K tuples:none
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.89
A1(0, z0) → c4(C(c(z0)))
c, a
C, A, A1
c1, c2, c3, c4
A1(0, z0) → c4(C(c(z0)))
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.89
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.89
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0))) 14.63/6.89
A1(0, z0) → c4(C(c(z0)))
K tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.63/6.89
C(c(z0)) → c2(C(z0)) 14.63/6.89
A(0, c(x0)) → c3(C(c(c(x0))), C(c(x0)))
Defined Rule Symbols:
A1(0, z0) → c4(C(c(z0)))
c, a
C, A, A1
c1, c2, c3, c4
A(0, c(b(c(z0)))) → c3(C(b(a(0, c(z0)))), C(c(b(c(z0))))) 14.63/6.89
A(0, c(z0)) → c3(C(b(c(b(c(z0))))), C(c(z0)))
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.63/6.89
c(c(z0)) → b(c(b(c(z0)))) 14.63/6.89
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A1(0, z0) → c4(C(c(z0))) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(b(a(0, c(z0)))), C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(b(c(b(c(z0))))), C(c(z0)))
K tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(b(a(0, c(z0)))), C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(b(c(b(c(z0))))), C(c(z0)))
Defined Rule Symbols:
A1(0, z0) → c4(C(c(z0)))
c, a
C, A1, A
c1, c2, c4, c3
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.98/6.90
c(c(z0)) → b(c(b(c(z0)))) 14.98/6.90
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A1(0, z0) → c4(C(c(z0))) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0)))
K tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0)))
Defined Rule Symbols:
A1(0, z0) → c4(C(c(z0)))
c, a
C, A1, A
c1, c2, c4, c3
We considered the (Usable) Rules:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0))
And the Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.98/6.90
c(c(z0)) → b(c(b(c(z0)))) 14.98/6.90
a(0, z0) → c(c(z0))
The order we found is given by the following interpretation:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A1(0, z0) → c4(C(c(z0))) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0)))
POL(0) = [3] 14.98/6.90
POL(A(x1, x2)) = x2 14.98/6.90
POL(A1(x1, x2)) = [1] + x1 + [5]x2 14.98/6.90
POL(C(x1)) = x1 14.98/6.90
POL(a(x1, x2)) = [3] + [3]x1 + [4]x2 14.98/6.90
POL(b(x1)) = x1 14.98/6.90
POL(c(x1)) = [4] + [2]x1 14.98/6.90
POL(c1(x1, x2)) = x1 + x2 14.98/6.90
POL(c2(x1)) = x1 14.98/6.90
POL(c3(x1)) = x1 14.98/6.90
POL(c4(x1)) = x1
Tuples:
c(c(b(c(z0)))) → b(a(0, c(z0))) 14.98/6.90
c(c(z0)) → b(c(b(c(z0)))) 14.98/6.90
a(0, z0) → c(c(z0))
S tuples:
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
A1(0, z0) → c4(C(c(z0))) 14.98/6.90
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0)))
K tuples:
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0)))
Defined Rule Symbols:
A1(0, z0) → c4(C(c(z0))) 14.98/6.90
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0))
c, a
C, A1, A
c1, c2, c4, c3
Now S is empty
A(0, c(b(c(z0)))) → c3(C(c(b(c(z0))))) 14.98/6.90
A(0, c(z0)) → c3(C(c(z0))) 14.98/6.90
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0)) 14.98/6.90
C(c(b(c(z0)))) → c1(A(0, c(z0)), C(z0)) 14.98/6.90
C(c(z0)) → c2(C(z0))