(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(f(x)) → mark(f(f(x)))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
mat(f(x), f(y)) → f(mat(x, y))
chk(no(c)) → active(c)
mat(f(x), c) → no(c)
f(active(x)) → active(f(x))
f(no(x)) → no(f(x))
f(mark(x)) → mark(f(x))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), 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 2.
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:
mark0(0) → 0
no0(0) → 0
X0() → 0
y0() → 0
c0() → 0
active0(0) → 1
chk0(0) → 2
mat0(0, 0) → 3
f0(0) → 4
tp0(0) → 5
c1() → 6
active1(6) → 2
f1(0) → 7
no1(7) → 4
f1(0) → 8
mark1(8) → 4
X1() → 14
f1(14) → 13
f1(13) → 12
f1(12) → 12
f1(12) → 11
mat1(11, 0) → 10
chk1(10) → 9
tp1(9) → 5
c1() → 15
no1(15) → 10
no1(7) → 7
no1(7) → 8
mark1(8) → 7
mark1(8) → 8
c2() → 16
active2(16) → 9
(2) BOUNDS(1, n^1)