(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(zeros) → mark(cons(0, zeros))
active(tail(cons(X, XS))) → mark(XS)
active(cons(X1, X2)) → cons(active(X1), X2)
active(tail(X)) → tail(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
tail(mark(X)) → mark(tail(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(tail(X)) → tail(proper(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
tail(ok(X)) → ok(tail(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
(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 5.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5]
transitions:
zeros0() → 0
mark0(0) → 0
00() → 0
ok0(0) → 0
active0(0) → 1
cons0(0, 0) → 2
tail0(0) → 3
proper0(0) → 4
top0(0) → 5
01() → 7
zeros1() → 8
cons1(7, 8) → 6
mark1(6) → 1
cons1(0, 0) → 9
mark1(9) → 2
tail1(0) → 10
mark1(10) → 3
zeros1() → 11
ok1(11) → 4
01() → 12
ok1(12) → 4
cons1(0, 0) → 13
ok1(13) → 2
tail1(0) → 14
ok1(14) → 3
proper1(0) → 15
top1(15) → 5
active1(0) → 16
top1(16) → 5
mark1(6) → 16
mark1(9) → 9
mark1(9) → 13
mark1(10) → 10
mark1(10) → 14
ok1(11) → 15
ok1(12) → 15
ok1(13) → 9
ok1(13) → 13
ok1(14) → 10
ok1(14) → 14
proper2(6) → 17
top2(17) → 5
active2(11) → 18
top2(18) → 5
active2(12) → 18
02() → 20
zeros2() → 21
cons2(20, 21) → 19
mark2(19) → 18
proper2(7) → 22
proper2(8) → 23
cons2(22, 23) → 17
zeros2() → 24
ok2(24) → 23
02() → 25
ok2(25) → 22
proper3(19) → 26
top3(26) → 5
proper3(20) → 27
proper3(21) → 28
cons3(27, 28) → 26
cons3(25, 24) → 29
ok3(29) → 17
zeros3() → 30
ok3(30) → 28
03() → 31
ok3(31) → 27
active3(29) → 32
top3(32) → 5
cons4(31, 30) → 33
ok4(33) → 26
active4(25) → 34
cons4(34, 24) → 32
active4(33) → 35
top4(35) → 5
active5(31) → 36
cons5(36, 30) → 35
(2) BOUNDS(O(1), O(n^1))