* Step 1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: copy(0(),y,z) -> f(z) copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) f(cons(nil(),y)) -> y - Signature: {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1} - Obligation: runtime complexity wrt. defined symbols {copy,f} and constructors {0,cons,n,nil,s} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(copy) = {2,3}, uargs(f) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = 0 p(cons) = 1 + x1 + x2 p(copy) = 2 + 4*x1 + x1*x2 + 2*x1^2 + x2 + x3 p(f) = x1 p(n) = 0 p(nil) = 0 p(s) = 1 + x1 Following rules are strictly oriented: copy(0(),y,z) = 2 + y + z > z = f(z) copy(s(x),y,z) = 8 + 8*x + x*y + 2*x^2 + 2*y + z > 3 + 4*x + x*y + 2*x^2 + 2*y + z = copy(x,y,cons(f(y),z)) f(cons(nil(),y)) = 1 + y > y = y Following rules are (at-least) weakly oriented: f(cons(f(cons(nil(),y)),z)) = 2 + y + z >= 2 + y + z = copy(n(),y,z) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) - Weak TRS: copy(0(),y,z) -> f(z) copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) f(cons(nil(),y)) -> y - Signature: {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1} - Obligation: runtime complexity wrt. defined symbols {copy,f} and constructors {0,cons,n,nil,s} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(copy) = {2,3}, uargs(f) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = 1 p(cons) = x1 + x2 p(copy) = 2*x1 + 6*x1*x2 + 6*x1^2 + 2*x2 + 2*x3 p(f) = 2 + 2*x1 p(n) = 0 p(nil) = 0 p(s) = 1 + x1 Following rules are strictly oriented: f(cons(f(cons(nil(),y)),z)) = 6 + 4*y + 2*z > 2*y + 2*z = copy(n(),y,z) Following rules are (at-least) weakly oriented: copy(0(),y,z) = 8 + 8*y + 2*z >= 2 + 2*z = f(z) copy(s(x),y,z) = 8 + 14*x + 6*x*y + 6*x^2 + 8*y + 2*z >= 4 + 2*x + 6*x*y + 6*x^2 + 6*y + 2*z = copy(x,y,cons(f(y),z)) f(cons(nil(),y)) = 2 + 2*y >= y = y * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: copy(0(),y,z) -> f(z) copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) f(cons(nil(),y)) -> y - Signature: {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1} - Obligation: runtime complexity wrt. defined symbols {copy,f} and constructors {0,cons,n,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))