WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a(y,x) -> y a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0()) b(x,y) -> c(a(c(y),a(0(),x))) - Signature: {a/2,b/2} / {0/0,c/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,b} and constructors {0,c} + 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): The following argument positions are considered usable: uargs(a) = {1,2}, uargs(b) = {1}, uargs(c) = {1} Following symbols are considered usable: {a,b} TcT has computed the following interpretation: p(0) = [0] [1] p(a) = [1 0] x1 + [1 0] x2 + [1] [0 2] [1 2] [0] p(b) = [1 4] x1 + [1 0] x2 + [4] [0 0] [4 0] [0] p(c) = [1 0] x1 + [0] [0 0] [0] Following rules are strictly oriented: a(y,x) = [1 0] x + [1 0] y + [1] [1 2] [0 2] [0] > [1 0] y + [0] [0 1] [0] = y a(y,c(b(a(0(),x),0()))) = [5 8] x + [1 0] y + [14] [5 8] [0 2] [13] > [5 8] x + [1 0] y + [13] [0 0] [0 0] [0] = b(a(c(b(0(),y)),x),0()) b(x,y) = [1 4] x + [1 0] y + [4] [0 0] [4 0] [0] > [1 0] x + [1 0] y + [2] [0 0] [0 0] [0] = c(a(c(y),a(0(),x))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))