YES(O(1), O(n^1)) 11.45/3.67 YES(O(1), O(n^1)) 11.86/3.71 11.86/3.71 11.86/3.71
11.86/3.71 11.86/3.710 CpxTRS11.86/3.71
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳2 CdtProblem11.86/3.71
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳4 CdtProblem11.86/3.71
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))11.86/3.71
↳6 CdtProblem11.86/3.71
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))11.86/3.71
↳8 CdtProblem11.86/3.71
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))11.86/3.71
↳10 CdtProblem11.86/3.71
↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳12 CdtProblem11.86/3.71
↳13 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳14 CdtProblem11.86/3.71
↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳16 CdtProblem11.86/3.71
↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳18 CdtProblem11.86/3.71
↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳20 CdtProblem11.86/3.71
↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳22 CdtProblem11.86/3.71
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))11.86/3.71
↳24 CdtProblem11.86/3.71
↳25 SIsEmptyProof (BOTH BOUNDS(ID, ID))11.86/3.71
↳26 BOUNDS(O(1), O(1))11.86/3.71
a__f(0) → cons(0, f(s(0))) 11.86/3.71
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.71
a__p(s(0)) → 0 11.86/3.71
mark(f(X)) → a__f(mark(X)) 11.86/3.71
mark(p(X)) → a__p(mark(X)) 11.86/3.71
mark(0) → 0 11.86/3.71
mark(cons(X1, X2)) → cons(mark(X1), X2) 11.86/3.71
mark(s(X)) → s(mark(X)) 11.86/3.71
a__f(X) → f(X) 11.86/3.71
a__p(X) → p(X)
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.71
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.71
a__f(z0) → f(z0) 11.86/3.71
a__p(s(0)) → 0 11.86/3.71
a__p(z0) → p(z0) 11.86/3.71
mark(f(z0)) → a__f(mark(z0)) 11.86/3.71
mark(p(z0)) → a__p(mark(z0)) 11.86/3.71
mark(0) → 0 11.86/3.71
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
A__F(s(0)) → c1(A__F(a__p(s(0))), A__P(s(0))) 11.86/3.72
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(A__P(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0))
K tuples:none
A__F(s(0)) → c1(A__F(a__p(s(0))), A__P(s(0))) 11.86/3.72
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(A__P(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0))
a__f, a__p, mark
A__F, MARK
c1, c5, c6, c8, c9
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
K tuples:none
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
a__f, a__p, mark
MARK, A__F
c5, c8, c9, c1, c6
We considered the (Usable) Rules:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
And the Tuples:
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0)) 11.86/3.72
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
POL(0) = 0 11.86/3.72
POL(A__F(x1)) = [2] 11.86/3.72
POL(MARK(x1)) = [4]x1 11.86/3.72
POL(a__f(x1)) = [4] + x1 11.86/3.72
POL(a__p(x1)) = 0 11.86/3.72
POL(c1(x1)) = x1 11.86/3.72
POL(c5(x1, x2)) = x1 + x2 11.86/3.72
POL(c6(x1)) = x1 11.86/3.72
POL(c8(x1)) = x1 11.86/3.72
POL(c9(x1)) = x1 11.86/3.72
POL(cons(x1, x2)) = x1 11.86/3.72
POL(f(x1)) = [2] + x1 11.86/3.72
POL(mark(x1)) = [2]x1 11.86/3.72
POL(p(x1)) = [1] + x1 11.86/3.72
POL(s(x1)) = x1
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
K tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
a__f, a__p, mark
MARK, A__F
c5, c8, c9, c1, c6
We considered the (Usable) Rules:
MARK(s(z0)) → c9(MARK(z0))
And the Tuples:
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0)) 11.86/3.72
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
POL(0) = 0 11.86/3.72
POL(A__F(x1)) = [4] 11.86/3.72
POL(MARK(x1)) = [2]x1 11.86/3.72
POL(a__f(x1)) = [3] 11.86/3.72
POL(a__p(x1)) = 0 11.86/3.72
POL(c1(x1)) = x1 11.86/3.72
POL(c5(x1, x2)) = x1 + x2 11.86/3.72
POL(c6(x1)) = x1 11.86/3.72
POL(c8(x1)) = x1 11.86/3.72
POL(c9(x1)) = x1 11.86/3.72
POL(cons(x1, x2)) = x1 11.86/3.72
POL(f(x1)) = [5] + x1 11.86/3.72
POL(mark(x1)) = 0 11.86/3.72
POL(p(x1)) = [5] + x1 11.86/3.72
POL(s(x1)) = [1] + x1
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
K tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0))
a__f, a__p, mark
MARK, A__F
c5, c8, c9, c1, c6
We considered the (Usable) Rules:
MARK(cons(z0, z1)) → c8(MARK(z0))
And the Tuples:
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0)) 11.86/3.72
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
POL(0) = [4] 11.86/3.72
POL(A__F(x1)) = [1] 11.86/3.72
POL(MARK(x1)) = x1 11.86/3.72
POL(a__f(x1)) = [2] + x1 11.86/3.72
POL(a__p(x1)) = 0 11.86/3.72
POL(c1(x1)) = x1 11.86/3.72
POL(c5(x1, x2)) = x1 + x2 11.86/3.72
POL(c6(x1)) = x1 11.86/3.72
POL(c8(x1)) = x1 11.86/3.72
POL(c9(x1)) = x1 11.86/3.72
POL(cons(x1, x2)) = [2] + x1 11.86/3.72
POL(f(x1)) = [2] + x1 11.86/3.72
POL(mark(x1)) = x1 11.86/3.72
POL(p(x1)) = [2] + x1 11.86/3.72
POL(s(x1)) = x1
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0))
K tuples:
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c5, c8, c9, c1, c6
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(0)) → c5(A__F(0), MARK(0)) 11.86/3.72
MARK(f(cons(z0, z1))) → c5(A__F(cons(mark(z0), z1)), MARK(cons(z0, z1))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0)))
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(0)) → c5(A__F(0), MARK(0)) 11.86/3.72
MARK(f(cons(z0, z1))) → c5(A__F(cons(mark(z0), z1)), MARK(cons(z0, z1))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0)))
K tuples:
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c1, c6, c5
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1)))
K tuples:
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(f(z0)) → c5(A__F(mark(z0)), MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c1, c6, c5, c5, c5
MARK(f(0)) → c5
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1(A__F(a__p(s(0)))) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1)))
K tuples:
A__F(s(0)) → c1(A__F(a__p(s(0))))
Defined Rule Symbols:
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c1, c6, c5, c5, c5
A__F(s(0)) → c1(A__F(0)) 11.86/3.72
A__F(s(0)) → c1(A__F(p(s(0))))
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1))) 11.86/3.72
A__F(s(0)) → c1(A__F(0)) 11.86/3.72
A__F(s(0)) → c1(A__F(p(s(0))))
K tuples:
A__F(s(0)) → c1(A__F(0)) 11.86/3.72
A__F(s(0)) → c1(A__F(p(s(0))))
Defined Rule Symbols:
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c6, c5, c5, c5, c1
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1))) 11.86/3.72
A__F(s(0)) → c1
K tuples:
A__F(s(0)) → c1
Defined Rule Symbols:
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c6, c5, c5, c5, c1
MARK(f(0)) → c5
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1))) 11.86/3.72
A__F(s(0)) → c1
K tuples:
A__F(s(0)) → c1
Defined Rule Symbols:
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0))
a__f, a__p, mark
MARK, A__F
c8, c9, c6, c5, c5, c5, c1
We considered the (Usable) Rules:
A__F(s(0)) → c1
And the Tuples:
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0)) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0)
The order we found is given by the following interpretation:
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1))) 11.86/3.72
A__F(s(0)) → c1
POL(0) = 0 11.86/3.72
POL(A__F(x1)) = [4] 11.86/3.72
POL(MARK(x1)) = x1 11.86/3.72
POL(a__f(x1)) = 0 11.86/3.72
POL(a__p(x1)) = 0 11.86/3.72
POL(c1) = 0 11.86/3.72
POL(c5) = 0 11.86/3.72
POL(c5(x1)) = x1 11.86/3.72
POL(c5(x1, x2)) = x1 + x2 11.86/3.72
POL(c6(x1)) = x1 11.86/3.72
POL(c8(x1)) = x1 11.86/3.72
POL(c9(x1)) = x1 11.86/3.72
POL(cons(x1, x2)) = x1 11.86/3.72
POL(f(x1)) = [4] + x1 11.86/3.72
POL(mark(x1)) = 0 11.86/3.72
POL(p(x1)) = x1 11.86/3.72
POL(s(x1)) = x1
Tuples:
a__f(0) → cons(0, f(s(0))) 11.86/3.72
a__f(s(0)) → a__f(a__p(s(0))) 11.86/3.72
a__f(z0) → f(z0) 11.86/3.72
a__p(s(0)) → 0 11.86/3.72
a__p(z0) → p(z0) 11.86/3.72
mark(f(z0)) → a__f(mark(z0)) 11.86/3.72
mark(p(z0)) → a__p(mark(z0)) 11.86/3.72
mark(0) → 0 11.86/3.72
mark(cons(z0, z1)) → cons(mark(z0), z1) 11.86/3.72
mark(s(z0)) → s(mark(z0))
S tuples:none
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(f(f(z0))) → c5(A__F(a__f(mark(z0))), MARK(f(z0))) 11.86/3.72
MARK(f(p(z0))) → c5(A__F(a__p(mark(z0))), MARK(p(z0))) 11.86/3.72
MARK(f(s(z0))) → c5(A__F(s(mark(z0))), MARK(s(z0))) 11.86/3.72
MARK(f(0)) → c5 11.86/3.72
MARK(f(cons(z0, z1))) → c5(MARK(cons(z0, z1))) 11.86/3.72
A__F(s(0)) → c1
Defined Rule Symbols:
MARK(p(z0)) → c6(MARK(z0)) 11.86/3.72
MARK(s(z0)) → c9(MARK(z0)) 11.86/3.72
MARK(cons(z0, z1)) → c8(MARK(z0)) 11.86/3.72
A__F(s(0)) → c1
a__f, a__p, mark
MARK, A__F
c8, c9, c6, c5, c5, c5, c1