* Step 1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: :(z,+(x,f(y))) -> :(g(z,y),+(x,a())) :(+(x,y),z) -> +(:(x,z),:(y,z)) :(:(x,y),z) -> :(x,:(y,z)) - Signature: {:/2} / {+/2,a/0,f/1,g/2} - Obligation: runtime complexity wrt. defined symbols {:} and constructors {+,a,f,g} + 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(+) = {1,2}, uargs(:) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = 1 + x1 + x2 p(:) = 2*x1 + 2*x1*x2 + x2 p(a) = 0 p(f) = 0 p(g) = 0 Following rules are strictly oriented: :(+(x,y),z) = 2 + 2*x + 2*x*z + 2*y + 2*y*z + 3*z > 1 + 2*x + 2*x*z + 2*y + 2*y*z + 2*z = +(:(x,z),:(y,z)) Following rules are (at-least) weakly oriented: :(z,+(x,f(y))) = 1 + x + 2*x*z + 4*z >= 1 + x = :(g(z,y),+(x,a())) :(:(x,y),z) = 4*x + 4*x*y + 4*x*y*z + 4*x*z + 2*y + 2*y*z + z >= 2*x + 4*x*y + 4*x*y*z + 2*x*z + 2*y + 2*y*z + z = :(x,:(y,z)) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: :(z,+(x,f(y))) -> :(g(z,y),+(x,a())) :(:(x,y),z) -> :(x,:(y,z)) - Weak TRS: :(+(x,y),z) -> +(:(x,z),:(y,z)) - Signature: {:/2} / {+/2,a/0,f/1,g/2} - Obligation: runtime complexity wrt. defined symbols {:} and constructors {+,a,f,g} + 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(+) = {1,2}, uargs(:) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = 1 + x1 + x2 p(:) = 1 + x1 + x1*x2 + x1^2 + x2 p(a) = 1 p(f) = 1 p(g) = 0 Following rules are strictly oriented: :(:(x,y),z) = 3 + 3*x + 5*x*y + x*y*z + 2*x*y^2 + x*z + 4*x^2 + 4*x^2*y + x^2*y^2 + x^2*z + 2*x^3 + 2*x^3*y + x^4 + 3*y + y*z + y^2 + 2*z > 2 + 2*x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z = :(x,:(y,z)) Following rules are (at-least) weakly oriented: :(z,+(x,f(y))) = 3 + x + x*z + 3*z + z^2 >= 3 + x = :(g(z,y),+(x,a())) :(+(x,y),z) = 3 + 3*x + 2*x*y + x*z + x^2 + 3*y + y*z + y^2 + 2*z >= 3 + x + x*z + x^2 + y + y*z + y^2 + 2*z = +(:(x,z),:(y,z)) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: :(z,+(x,f(y))) -> :(g(z,y),+(x,a())) - Weak TRS: :(+(x,y),z) -> +(:(x,z),:(y,z)) :(:(x,y),z) -> :(x,:(y,z)) - Signature: {:/2} / {+/2,a/0,f/1,g/2} - Obligation: runtime complexity wrt. defined symbols {:} and constructors {+,a,f,g} + 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(+) = {1,2}, uargs(:) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = 1 + x1 + x2 p(:) = 1 + 2*x1 + 2*x1*x2 + 2*x2 p(a) = 0 p(f) = 1 + x1 p(g) = 0 Following rules are strictly oriented: :(z,+(x,f(y))) = 5 + 2*x + 2*x*z + 2*y + 2*y*z + 6*z > 3 + 2*x = :(g(z,y),+(x,a())) Following rules are (at-least) weakly oriented: :(+(x,y),z) = 3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z >= 3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z = +(:(x,z),:(y,z)) :(:(x,y),z) = 3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z >= 3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z = :(x,:(y,z)) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: :(z,+(x,f(y))) -> :(g(z,y),+(x,a())) :(+(x,y),z) -> +(:(x,z),:(y,z)) :(:(x,y),z) -> :(x,:(y,z)) - Signature: {:/2} / {+/2,a/0,f/1,g/2} - Obligation: runtime complexity wrt. defined symbols {:} and constructors {+,a,f,g} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))