77.41/45.72
77.41/45.72
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
77.41/45.72
a__tail(cons(X, XS)) → mark(XS)
77.41/45.72
mark(zeros) → a__zeros
77.41/45.72
mark(tail(X)) → a__tail(mark(X))
77.41/45.72
mark(cons(X1, X2)) → cons(mark(X1), X2)
77.41/45.72
mark(0) → 0
77.41/45.72
a__zeros → zeros
77.41/45.72
a__tail(X) → tail(X)
Rewrite Strategy: INNERMOST
77.41/45.72
77.41/45.72
(1) 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
77.41/45.72
77.41/45.72
(2) BOUNDS(O(1), O(n^1))
77.41/45.72