(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(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 3.
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, 6, 7]
transitions:
mark0(0) → 0
c0() → 0
X0() → 0
ok0(0) → 0
found0(0) → 0
active0(0) → 1
top0(0) → 2
check0(0) → 3
match0(0, 0) → 4
proper0(0) → 5
f0(0) → 6
start0(0) → 7
check1(0) → 8
top1(8) → 2
X1() → 11
f1(11) → 10
match1(10, 0) → 9
start1(9) → 3
proper1(0) → 4
c1() → 12
ok1(12) → 5
f1(0) → 13
ok1(13) → 6
found1(0) → 7
f1(0) → 14
found1(14) → 6
active1(0) → 15
top1(15) → 2
f1(0) → 16
mark1(16) → 6
c1() → 18
mark1(18) → 17
top1(17) → 2
X2() → 21
f2(21) → 20
match2(20, 0) → 19
start2(19) → 8
ok1(12) → 4
ok1(13) → 13
ok1(13) → 14
ok1(13) → 16
found1(14) → 13
found1(14) → 14
found1(14) → 16
mark1(16) → 13
mark1(16) → 14
mark1(16) → 16
check2(18) → 22
top2(22) → 2
X3() → 25
f3(25) → 24
match3(24, 18) → 23
start3(23) → 22
(2) BOUNDS(1, n^1)