(VAR x y z)
(RULES
  a -> b
  b -> c
  c -> a
  f(s(a)) -> a
  f(s(b)) -> f(s(a))
  f(s(c)) -> f(s(b))

  +(x,y) -> +(y,x)
  +(x,+(y,z)) -> +(+(x,y),z)
  +(+(x,y),z) -> +(x,+(y,z))
  +(0,x) -> x
  +(s(x),y) -> s(+(x,y))
)
(COMMENT
  construtor sharing
)