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))
  , *(x, 1()) -> x
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(1(), y) -> y }
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(*) = {}, safe(+) = {1, 2}, safe(1) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {*}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

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

Hurray, we answered YES(?,ELEMENTARY)