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