### (0) Obligation:

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

The TRS R consists of the following rules:

a__zeroscons(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__zeroszeros
a__tail(X) → tail(X)

Rewrite Strategy: FULL

### (1) RcToIrcProof (BOTH BOUNDS(ID, ID) transformation)

Converted rc-obligation to irc-obligation.

As the TRS is a non-duplicating overlay system, we have rc = irc.

### (2) Obligation:

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

The TRS R consists of the following rules:

a__zeroscons(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__zeroszeros
a__tail(X) → tail(X)

Rewrite Strategy: INNERMOST

### (3) 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