```* Step 1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
*(x,*(y,z)) -> *(otimes(x,y),z)
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(1(),y) -> y
- Signature:
{*/2} / {+/2,1/0,oplus/2,otimes/2}
- Obligation:
runtime complexity wrt. defined symbols {*} and constructors {+,1,oplus,otimes}
+ 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(oplus) = {1,2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = x1 + x1*x2 + x2
p(+) = 1 + x1 + x2
p(1) = 1
p(oplus) = 1 + x1 + x2
p(otimes) = x1

Following rules are strictly oriented:
*(1(),y) = 1 + 2*y
> y
= y

Following rules are (at-least) weakly oriented:
*(x,*(y,z)) =  x + x*y + x*y*z + x*z + y + y*z + z
>= x + x*z + z
=  *(otimes(x,y),z)

*(x,oplus(y,z)) =  1 + 2*x + x*y + x*z + y + z
>= 1 + 2*x + x*y + x*z + y + z
=  oplus(*(x,y),*(x,z))

*(+(x,y),z) =  1 + x + x*z + y + y*z + 2*z
>= 1 + x + x*z + y + y*z + 2*z
=  oplus(*(x,z),*(y,z))

* Step 2: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
*(x,*(y,z)) -> *(otimes(x,y),z)
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
- Weak TRS:
*(1(),y) -> y
- Signature:
{*/2} / {+/2,1/0,oplus/2,otimes/2}
- Obligation:
runtime complexity wrt. defined symbols {*} and constructors {+,1,oplus,otimes}
+ 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(oplus) = {1,2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 2*x1 + 2*x1*x2 + 2*x2
p(+) = 1 + x1 + x2
p(1) = 0
p(oplus) = 1 + x1 + x2
p(otimes) = 0

Following rules are strictly oriented:
*(x,oplus(y,z)) = 2 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
> 1 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
= oplus(*(x,y),*(x,z))

*(+(x,y),z) = 2 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z
> 1 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z
= oplus(*(x,z),*(y,z))

Following rules are (at-least) weakly oriented:
*(x,*(y,z)) =  2*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
>= 2*z
=  *(otimes(x,y),z)

*(1(),y) =  2*y
>= y
=  y

* Step 3: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
*(x,*(y,z)) -> *(otimes(x,y),z)
- Weak TRS:
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(1(),y) -> y
- Signature:
{*/2} / {+/2,1/0,oplus/2,otimes/2}
- Obligation:
runtime complexity wrt. defined symbols {*} and constructors {+,1,oplus,otimes}
+ 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(oplus) = {1,2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 1 + 2*x1 + 2*x1*x2 + 2*x2
p(+) = 1 + x1 + x2
p(1) = 0
p(oplus) = 1 + x1 + x2
p(otimes) = x2

Following rules are strictly oriented:
*(x,*(y,z)) = 3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
> 1 + 2*y + 2*y*z + 2*z
= *(otimes(x,y),z)

Following rules are (at-least) weakly oriented:
*(x,oplus(y,z)) =  3 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
>= 3 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
=  oplus(*(x,y),*(x,z))

*(+(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
=  oplus(*(x,z),*(y,z))

*(1(),y) =  1 + 2*y
>= y
=  y

* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
*(x,*(y,z)) -> *(otimes(x,y),z)
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(1(),y) -> y
- Signature:
{*/2} / {+/2,1/0,oplus/2,otimes/2}
- Obligation:
runtime complexity wrt. defined symbols {*} and constructors {+,1,oplus,otimes}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))
```