YES(O(1), O(n^1)) 2.50/1.04 YES(O(1), O(n^1)) 2.50/1.06 2.50/1.06 2.50/1.06
2.50/1.06 2.50/1.060 CpxTRS2.50/1.06
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.50/1.06
↳2 CdtProblem2.50/1.06
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))2.50/1.06
↳4 CdtProblem2.50/1.06
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))2.50/1.06
↳6 CdtProblem2.50/1.06
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.50/1.06
↳8 CdtProblem2.50/1.06
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.50/1.06
↳10 CdtProblem2.50/1.06
↳11 CdtKnowledgeProof (⇔)2.50/1.06
↳12 BOUNDS(O(1), O(1))2.50/1.06
a__f(f(X)) → a__c(f(g(f(X)))) 2.50/1.06
a__c(X) → d(X) 2.50/1.06
a__h(X) → a__c(d(X)) 2.50/1.06
mark(f(X)) → a__f(mark(X)) 2.50/1.06
mark(c(X)) → a__c(X) 2.50/1.06
mark(h(X)) → a__h(mark(X)) 2.50/1.06
mark(g(X)) → g(X) 2.50/1.06
mark(d(X)) → d(X) 2.50/1.06
a__f(X) → f(X) 2.50/1.06
a__c(X) → c(X) 2.50/1.06
a__h(X) → h(X)
Tuples:
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.06
a__f(z0) → f(z0) 2.50/1.06
a__c(z0) → d(z0) 2.50/1.06
a__c(z0) → c(z0) 2.50/1.06
a__h(z0) → a__c(d(z0)) 2.50/1.06
a__h(z0) → h(z0) 2.50/1.06
mark(f(z0)) → a__f(mark(z0)) 2.50/1.06
mark(c(z0)) → a__c(z0) 2.50/1.06
mark(h(z0)) → a__h(mark(z0)) 2.50/1.06
mark(g(z0)) → g(z0) 2.50/1.06
mark(d(z0)) → d(z0)
S tuples:
A__F(f(z0)) → c1(A__C(f(g(f(z0))))) 2.50/1.06
A__H(z0) → c5(A__C(d(z0))) 2.50/1.06
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.06
MARK(c(z0)) → c8(A__C(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0))
K tuples:none
A__F(f(z0)) → c1(A__C(f(g(f(z0))))) 2.50/1.07
A__H(z0) → c5(A__C(d(z0))) 2.50/1.07
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(c(z0)) → c8(A__C(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0))
a__f, a__c, a__h, mark
A__F, A__H, MARK
c1, c5, c7, c8, c9
Tuples:
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0)
S tuples:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
K tuples:none
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
a__f, a__c, a__h, mark
MARK, A__F, A__H
c7, c9, c1, c5, c8
A__H(z0) → c5 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
MARK(c(z0)) → c8
Tuples:
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0)
S tuples:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
K tuples:none
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
a__f, a__c, a__h, mark
MARK, A__F, A__H
c7, c9, c1, c5, c8
We considered the (Usable) Rules:
MARK(c(z0)) → c8
And the Tuples:
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
POL(A__F(x1)) = 0 2.50/1.07
POL(A__H(x1)) = 0 2.50/1.07
POL(MARK(x1)) = [3] 2.50/1.07
POL(a__c(x1)) = x1 2.50/1.07
POL(a__f(x1)) = [5] + x1 2.50/1.07
POL(a__h(x1)) = [4] 2.50/1.07
POL(c(x1)) = x1 2.50/1.07
POL(c1) = 0 2.50/1.07
POL(c5) = 0 2.50/1.07
POL(c7(x1, x2)) = x1 + x2 2.50/1.07
POL(c8) = 0 2.50/1.07
POL(c9(x1, x2)) = x1 + x2 2.50/1.07
POL(d(x1)) = 0 2.50/1.07
POL(f(x1)) = [3] + x1 2.50/1.07
POL(g(x1)) = [5] 2.50/1.07
POL(h(x1)) = [2] 2.50/1.07
POL(mark(x1)) = [3]x1
Tuples:
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0)
S tuples:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
K tuples:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5
Defined Rule Symbols:
MARK(c(z0)) → c8
a__f, a__c, a__h, mark
MARK, A__F, A__H
c7, c9, c1, c5, c8
We considered the (Usable) Rules:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__H(z0) → c5
And the Tuples:
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
POL(A__F(x1)) = 0 2.50/1.07
POL(A__H(x1)) = [3] 2.50/1.07
POL(MARK(x1)) = [2]x1 2.50/1.07
POL(a__c(x1)) = x1 2.50/1.07
POL(a__f(x1)) = [5] + x1 2.50/1.07
POL(a__h(x1)) = [2] + x1 2.50/1.07
POL(c(x1)) = x1 2.50/1.07
POL(c1) = 0 2.50/1.07
POL(c5) = 0 2.50/1.07
POL(c7(x1, x2)) = x1 + x2 2.50/1.07
POL(c8) = 0 2.50/1.07
POL(c9(x1, x2)) = x1 + x2 2.50/1.07
POL(d(x1)) = 0 2.50/1.07
POL(f(x1)) = [3] + x1 2.50/1.07
POL(g(x1)) = [5] 2.50/1.07
POL(h(x1)) = [2] + x1 2.50/1.07
POL(mark(x1)) = [2] + [5]x1
Tuples:
a__f(f(z0)) → a__c(f(g(f(z0)))) 2.50/1.07
a__f(z0) → f(z0) 2.50/1.07
a__c(z0) → d(z0) 2.50/1.07
a__c(z0) → c(z0) 2.50/1.07
a__h(z0) → a__c(d(z0)) 2.50/1.07
a__h(z0) → h(z0) 2.50/1.07
mark(f(z0)) → a__f(mark(z0)) 2.50/1.07
mark(c(z0)) → a__c(z0) 2.50/1.07
mark(h(z0)) → a__h(mark(z0)) 2.50/1.07
mark(g(z0)) → g(z0) 2.50/1.07
mark(d(z0)) → d(z0)
S tuples:
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__F(f(z0)) → c1 2.50/1.07
A__H(z0) → c5 2.50/1.07
MARK(c(z0)) → c8
K tuples:
A__F(f(z0)) → c1
Defined Rule Symbols:
MARK(c(z0)) → c8 2.50/1.07
MARK(f(z0)) → c7(A__F(mark(z0)), MARK(z0)) 2.50/1.07
MARK(h(z0)) → c9(A__H(mark(z0)), MARK(z0)) 2.50/1.07
A__H(z0) → c5
a__f, a__c, a__h, mark
MARK, A__F, A__H
c7, c9, c1, c5, c8
Now S is empty
A__F(f(z0)) → c1