The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳30 CdtProblem
    ↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳32 CdtProblem
    ↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳34 CdtProblem
↳35 CpxTrsMatchBoundsTAProof (⇔, 151 ms)
↳36 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__tail(cons(X, XS)) → mark(XS)
mark(zeros) → a__zeros
mark(tail(X)) → a__tail(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
a__zeros → zeros
a__tail(X) → tail(X)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(zeros) → c4(A__ZEROS)
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(zeros) → c4(A__ZEROS)
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c4, c5, c6

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(zeros) → c4(A__ZEROS)

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c5, c6

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0)) by

MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))
MARK(tail(x0)) → c5

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))
MARK(tail(x0)) → c5
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))
MARK(tail(x0)) → c5
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

MARK(tail(0)) → c5(A__TAIL(0), MARK(0))
MARK(tail(x0)) → c5

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros)) by

MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(zeros)) → c5(A__TAIL(zeros), MARK(zeros))
MARK(tail(zeros)) → c5

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(zeros)) → c5(A__TAIL(zeros), MARK(zeros))
MARK(tail(zeros)) → c5
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(zeros)) → c5(A__TAIL(zeros), MARK(zeros))
MARK(tail(zeros)) → c5
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

MARK(tail(zeros)) → c5
MARK(tail(zeros)) → c5(A__TAIL(zeros), MARK(zeros))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0))) by

MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))
MARK(tail(tail(x0))) → c5

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))
MARK(tail(tail(x0))) → c5
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))
MARK(tail(tail(x0))) → c5
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(tail(tail(x0))) → c5

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0))) by

MARK(tail(tail(0))) → c5(A__TAIL(tail(0)), MARK(tail(0)))
MARK(tail(tail(0))) → c5

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(tail(0)), MARK(tail(0)))
MARK(tail(tail(0))) → c5
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(tail(0)), MARK(tail(0)))
MARK(tail(tail(0))) → c5
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

MARK(tail(tail(0))) → c5(A__TAIL(tail(0)), MARK(tail(0)))
MARK(tail(tail(0))) → c5

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, z1)) → c2(MARK(z1)) by

A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
S tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c6, c5, c2

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)), MARK(zeros))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
S tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c6, c5, c2

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(cons(z0, z1)) → c6(MARK(z0)) by

MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c6

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0))) by

MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c6

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1))) by

A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c6

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0)))) by

A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c6

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1))) by

MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0
Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(cons(y0, y1)))) → c5(A__TAIL(tail(mark(cons(y0, y1)))), MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(y0)))) → c5(A__TAIL(tail(mark(tail(y0)))), MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(A__TAIL(tail(mark(tail(zeros)))), MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(y0))))) → c5(A__TAIL(tail(mark(tail(tail(y0))))), MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(A__TAIL(tail(mark(tail(cons(y0, y1))))), MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c6

(35) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 4.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
cons0(0, 0) → 0
00() → 0
zeros0() → 0
tail0(0) → 0
a__zeros0() → 1
a__tail0(0) → 2
mark0(0) → 3
01() → 4
zeros1() → 5
cons1(4, 5) → 1
mark1(0) → 2
a__zeros1() → 3
mark1(0) → 6
a__tail1(6) → 3
mark1(0) → 7
cons1(7, 0) → 3
01() → 3
zeros1() → 1
tail1(0) → 2
02() → 8
zeros2() → 9
cons2(8, 9) → 3
a__zeros1() → 2
a__zeros1() → 6
a__zeros1() → 7
a__tail1(6) → 2
a__tail1(6) → 6
a__tail1(6) → 7
cons1(7, 0) → 2
cons1(7, 0) → 6
cons1(7, 0) → 7
01() → 2
01() → 6
01() → 7
zeros2() → 3
tail2(6) → 3
cons2(8, 9) → 2
cons2(8, 9) → 6
cons2(8, 9) → 7
mark2(0) → 2
mark2(0) → 3
mark2(0) → 6
mark2(0) → 7
zeros2() → 2
zeros2() → 6
zeros2() → 7
tail2(6) → 2
tail2(6) → 6
tail2(6) → 7
mark2(9) → 2
mark2(9) → 3
mark2(9) → 6
mark2(9) → 7
a__zeros3() → 2
a__zeros3() → 3
a__zeros3() → 6
a__zeros3() → 7
04() → 10
zeros4() → 11
cons4(10, 11) → 2
cons4(10, 11) → 3
cons4(10, 11) → 6
cons4(10, 11) → 7
zeros4() → 2
zeros4() → 3
zeros4() → 6
zeros4() → 7
mark2(11) → 2
mark2(11) → 3
mark2(11) → 6
mark2(11) → 7

(36) BOUNDS(O(1), O(n^1))