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