(VAR x y z)
(RULES
  e(x) -> ++(x,e(+(x,x)))

  ++(++(x,y),z) -> ++(x,++(y,z))
  ++(x,++(y,z)) -> ++(++(x,y),z)
  ++(0,x) -> x

  +(x,y)      -> +(y,x)
  +(+(x,y),z) -> +(x,+(y,z))
  +(0,x) -> x
  +(s(x),y) -> s(+(x,y))
)
(COMMENT
  there are no composable subsystems
)