WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a__f(X) -> f(X) a__f(f(a())) -> c(f(g(f(a())))) mark(a()) -> a() mark(c(X)) -> c(X) mark(f(X)) -> a__f(mark(X)) mark(g(X)) -> g(mark(X)) - Signature: {a__f/1,mark/1} / {a/0,c/1,f/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__f,mark} and constructors {a,c,f,g} + Applied Processor: NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(a__f) = {1}, uargs(g) = {1} Following symbols are considered usable: {a__f,mark} TcT has computed the following interpretation: p(a) = 1 p(a__f) = 4 + x1 p(c) = 1 p(f) = 1 + x1 p(g) = 2 + x1 p(mark) = 8 + 8*x1 Following rules are strictly oriented: a__f(X) = 4 + X > 1 + X = f(X) a__f(f(a())) = 6 > 1 = c(f(g(f(a())))) mark(a()) = 16 > 1 = a() mark(c(X)) = 16 > 1 = c(X) mark(f(X)) = 16 + 8*X > 12 + 8*X = a__f(mark(X)) mark(g(X)) = 24 + 8*X > 10 + 8*X = g(mark(X)) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))