YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

Strict Trs: { *(x, +(y, z)) -> +(*(x, y), *(x, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(*) = {1}, safe(+) = {1, 2}

and precedence

 empty .

Following symbols are considered recursive:

 {*}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

  *(+(; y,  z); x) > +(; *(y; x),  *(z; x))
                                           

Hurray, we answered YES(?,ELEMENTARY)