WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) - Signature: {a/1,u/1,v/1,w/1} / {b/1,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,u,v,w} and constructors {b,c,d} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(u) = {1} Following symbols are considered usable: {a,u,v,w} TcT has computed the following interpretation: p(a) = [2] x1 + [2] p(b) = [0] p(c) = [1] x1 + [1] p(d) = [1] x1 + [4] p(u) = [2] x1 + [12] p(v) = [4] x1 + [4] p(w) = [4] x1 + [4] Following rules are strictly oriented: a(c(d(x))) = [2] x + [12] > [1] x + [1] = c(x) u(b(d(d(x)))) = [12] > [0] = b(x) v(a(a(x))) = [16] x + [28] > [8] x + [20] = u(v(x)) v(a(c(x))) = [8] x + [20] > [12] = u(b(d(x))) v(c(x)) = [4] x + [8] > [0] = b(x) w(a(a(x))) = [16] x + [28] > [8] x + [20] = u(w(x)) w(a(c(x))) = [8] x + [20] > [12] = u(b(d(x))) w(c(x)) = [4] x + [8] > [0] = b(x) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))