YES(O(1), O(n^1)) 0.00/0.77 YES(O(1), O(n^1)) 0.00/0.78 0.00/0.78 0.00/0.78
0.00/0.78 0.00/0.780 CpxTRS0.00/0.78
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.78
↳2 CdtProblem0.00/0.78
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.78
↳4 CdtProblem0.00/0.78
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.78
↳6 CdtProblem0.00/0.78
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.78
↳8 CdtProblem0.00/0.78
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.78
↳10 BOUNDS(O(1), O(1))0.00/0.78
a__f(f(a)) → c(f(g(f(a)))) 0.00/0.78
mark(f(X)) → a__f(mark(X)) 0.00/0.78
mark(a) → a 0.00/0.78
mark(c(X)) → c(X) 0.00/0.78
mark(g(X)) → g(mark(X)) 0.00/0.78
a__f(X) → f(X)
Tuples:
a__f(f(a)) → c(f(g(f(a)))) 0.00/0.78
a__f(z0) → f(z0) 0.00/0.78
mark(f(z0)) → a__f(mark(z0)) 0.00/0.78
mark(a) → a 0.00/0.78
mark(c(z0)) → c(z0) 0.00/0.78
mark(g(z0)) → g(mark(z0))
S tuples:
MARK(f(z0)) → c3(A__F(mark(z0)), MARK(z0)) 0.00/0.78
MARK(g(z0)) → c6(MARK(z0))
K tuples:none
MARK(f(z0)) → c3(A__F(mark(z0)), MARK(z0)) 0.00/0.78
MARK(g(z0)) → c6(MARK(z0))
a__f, mark
MARK
c3, c6
Tuples:
a__f(f(a)) → c(f(g(f(a)))) 0.00/0.78
a__f(z0) → f(z0) 0.00/0.78
mark(f(z0)) → a__f(mark(z0)) 0.00/0.78
mark(a) → a 0.00/0.78
mark(c(z0)) → c(z0) 0.00/0.78
mark(g(z0)) → g(mark(z0))
S tuples:
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
K tuples:none
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
a__f, mark
MARK
c6, c3
We considered the (Usable) Rules:none
MARK(g(z0)) → c6(MARK(z0))
The order we found is given by the following interpretation:
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
POL(MARK(x1)) = [2]x1 0.00/0.78
POL(c3(x1)) = x1 0.00/0.78
POL(c6(x1)) = x1 0.00/0.78
POL(f(x1)) = x1 0.00/0.78
POL(g(x1)) = [1] + x1
Tuples:
a__f(f(a)) → c(f(g(f(a)))) 0.00/0.78
a__f(z0) → f(z0) 0.00/0.78
mark(f(z0)) → a__f(mark(z0)) 0.00/0.78
mark(a) → a 0.00/0.78
mark(c(z0)) → c(z0) 0.00/0.78
mark(g(z0)) → g(mark(z0))
S tuples:
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
K tuples:
MARK(f(z0)) → c3(MARK(z0))
Defined Rule Symbols:
MARK(g(z0)) → c6(MARK(z0))
a__f, mark
MARK
c6, c3
We considered the (Usable) Rules:none
MARK(f(z0)) → c3(MARK(z0))
The order we found is given by the following interpretation:
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
POL(MARK(x1)) = [3]x1 0.00/0.78
POL(c3(x1)) = x1 0.00/0.78
POL(c6(x1)) = x1 0.00/0.78
POL(f(x1)) = [1] + x1 0.00/0.78
POL(g(x1)) = x1
Tuples:
a__f(f(a)) → c(f(g(f(a)))) 0.00/0.78
a__f(z0) → f(z0) 0.00/0.78
mark(f(z0)) → a__f(mark(z0)) 0.00/0.78
mark(a) → a 0.00/0.78
mark(c(z0)) → c(z0) 0.00/0.78
mark(g(z0)) → g(mark(z0))
S tuples:none
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
Defined Rule Symbols:
MARK(g(z0)) → c6(MARK(z0)) 0.00/0.78
MARK(f(z0)) → c3(MARK(z0))
a__f, mark
MARK
c6, c3