MAYBE

Problem:
 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))

Proof:
 Open