WORST_CASE(?,O(n^1)) * Step 1: NaturalPI 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: 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(g) = {1}, uargs(s) = {1} Following symbols are considered usable: {f,norm,rem} TcT has computed the following interpretation: p(0) = 0 p(f) = x1 + 8*x2 p(g) = 2 + x1 p(nil) = 1 p(norm) = 4*x1 p(rem) = 8 + 2*x1 + 2*x2 p(s) = 2 + x1 Following rules are strictly oriented: f(x,g(y,z)) = 16 + x + 8*y > 2 + x + 8*y = g(f(x,y),z) f(x,nil()) = 8 + x > 3 = g(nil(),x) norm(g(x,y)) = 8 + 4*x > 2 + 4*x = s(norm(x)) norm(nil()) = 4 > 0 = 0() rem(g(x,y),0()) = 12 + 2*x > 2 + x = g(x,y) rem(g(x,y),s(z)) = 16 + 2*x + 2*z > 8 + 2*x + 2*z = rem(x,z) rem(nil(),y) = 10 + 2*y > 1 = nil() Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))