(VAR x y z)
(RULES
  +(x,y)      -> +(y,x)
  +(+(x,y),z) -> +(x,+(y,z))
  +(0,x) -> x
  +(s(x),y) -> s(+(x,y))

  fib(x) -> :(x,+(fib(x),fib(s(x))))

  *(x,y) -> *(y,x)
  *(0,y) -> 0
  *(s(x),y) -> +(y,*(x,y))

  .(.(x,y),z) -> .(x,.(y,z))
  .(x,.(y,z)) -> .(.(x,y),z)
  .(a,.(b,a)) -> .(.(b,a),b)
)
(COMMENT
  non-confluent TRS
)