WORST_CASE(?,O(n^1)) * Step 1: NaturalPI 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: NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(s) = {1} Following symbols are considered usable: {+,double} TcT has computed the following interpretation: p(+) = 4*x1 + 8*x2 p(0) = 2 p(double) = 2 + 12*x1 p(s) = 1 + x1 Following rules are strictly oriented: +(x,0()) = 16 + 4*x > x = x +(x,s(y)) = 8 + 4*x + 8*y > 1 + 4*x + 8*y = s(+(x,y)) +(s(x),y) = 4 + 4*x + 8*y > 1 + 4*x + 8*y = s(+(x,y)) double(x) = 2 + 12*x > 12*x = +(x,x) double(0()) = 26 > 2 = 0() double(s(x)) = 14 + 12*x > 4 + 12*x = s(s(double(x))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))