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