WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(x,y,s(z)) -> s(f(0(),1(),z)) f(0(),1(),x) -> f(s(x),x,x) g(x,y) -> x g(x,y) -> y - Signature: {f/3,g/2} / {0/0,1/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,s} + 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(s) = {1} Following symbols are considered usable: {f,g} TcT has computed the following interpretation: p(0) = [0] [5] p(1) = [0] [4] p(f) = [0 1] x1 + [2 1] x3 + [0] [0 0] [0 1] [0] p(g) = [4 0] x1 + [2 1] x2 + [5] [1 4] [1 1] [0] p(s) = [1 2] x1 + [4] [0 0] [4] Following rules are strictly oriented: f(x,y,s(z)) = [0 1] x + [2 4] z + [12] [0 0] [0 0] [4] > [2 3] z + [9] [0 0] [4] = s(f(0(),1(),z)) f(0(),1(),x) = [2 1] x + [5] [0 1] [0] > [2 1] x + [4] [0 1] [0] = f(s(x),x,x) g(x,y) = [4 0] x + [2 1] y + [5] [1 4] [1 1] [0] > [1 0] x + [0] [0 1] [0] = x g(x,y) = [4 0] x + [2 1] y + [5] [1 4] [1 1] [0] > [1 0] y + [0] [0 1] [0] = y Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))