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

Proof:
 Open