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