YES ---- CR(R) ---- [Jouannaud and Kirchner, 1986] R: +(0(),x) -> x +(1(),-(1())) -> 0() -(0()) -> 0() -(-(x)) -> x -(+(x,y)) -> +(-(x),-(y)) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) CP_AC(R): -(x) -> +(-(x),-(0())) -(+(x,y)) -> +(-(x),-(+(0(),y))) -(x) -> +(-(0()),-(x)) -(+(x,y)) -> +(-(+(0(),x)),-(y)) -(0()) -> +(-(-(1())),-(1())) -(0()) -> +(-(1()),-(-(1()))) -(0()) -> 0() -(x) -> -(x) -(+(-(x),-(y))) -> +(x,y) x -> +(0(),x) +(x,y) -> +(0(),y,x) x -> +(x,0()) +(x,y) -> +(y,0(),x) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) 0() -> +(1(),-(1())) 0() -> +(-(1()),1()) +(0(),x) -> +(-(1()),1(),x) +(0(),x) -> +(1(),-(1()),x) +(x,0()) -> +(x,-(1()),1()) +(x,0()) -> +(x,1(),-(1()))