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