We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { *(x, 0()) -> 0()
  , *(*(x, y), z) -> *(x, *(y, z))
  , *(i(x), x) -> 1()
  , *(1(), y) -> y }
Obligation:
  runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 1. The enriched problem is
compatible with the following automaton.
{ *_0(2, 2) -> 1
, *_0(2, 3) -> 1
, *_0(2, 4) -> 1
, *_0(3, 2) -> 1
, *_0(3, 3) -> 1
, *_0(3, 4) -> 1
, *_0(4, 2) -> 1
, *_0(4, 3) -> 1
, *_0(4, 4) -> 1
, i_0(2) -> 1
, i_0(2) -> 2
, i_0(3) -> 1
, i_0(3) -> 2
, i_0(4) -> 1
, i_0(4) -> 2
, 1_0() -> 1
, 1_0() -> 3
, 1_1() -> 1
, 0_0() -> 1
, 0_0() -> 4
, 0_1() -> 1 }

Hurray, we answered YES(?,O(n^1))