WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) -> a(f(x,y)) f(b(x),b(y)) -> b(f(x,y)) - Signature: {a/1,f/2} / {b/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,f} and constructors {b} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): Following symbols are considered usable: {a,f} TcT has computed the following interpretation: p(a) = [1 4] x1 + [1] [0 2] [3] p(b) = [1 0] x1 + [1] [0 0] [0] p(f) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] Following rules are strictly oriented: a(a(f(x,y))) = [1 12] x + [1 12] y + [14] [0 4] [0 4] [9] > [1 4] x + [1 4] y + [10] [0 0] [0 0] [6] = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) f(a(x),a(y)) = [1 4] x + [1 4] y + [2] [0 2] [0 2] [6] > [1 4] x + [1 4] y + [1] [0 2] [0 2] [3] = a(f(x,y)) f(b(x),b(y)) = [1 0] x + [1 0] y + [2] [0 0] [0 0] [0] > [1 0] x + [1 0] y + [1] [0 0] [0 0] [0] = b(f(x,y)) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))