```* 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))
```