YES

Problem:
 *(i(x),x) -> 1()
 *(1(),y) -> y
 *(x,0()) -> 0()
 *(*(x,y),z) -> *(x,*(y,z))

Proof:
 Polynomial Interpretation Processor:
  dimension: 1
  interpretation:
   [0] = 4,
   
   [1] = 4,
   
   [*](x0, x1) = 4x0 + x1 + 2,
   
   [i](x0) = 4x0 + 4x0x0 + 1
  orientation:
   *(i(x),x) = 17x + 16x*x + 6 >= 4 = 1()
   
   *(1(),y) = y + 18 >= y = y
   
   *(x,0()) = 4x + 6 >= 4 = 0()
   
   *(*(x,y),z) = 16x + 4y + z + 10 >= 4x + 4y + z + 4 = *(x,*(y,z))
  problem:
   
  Qed