---- CR(R)
---- [Jouannaud and Kirchner, 1986]
R:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
dbl(x) -> +(x,x)
+(+(x,y),z) -> +(x,+(y,z))
+(x,y) -> +(y,x)
CP_AC(R):
+(x,s(y)) -> s(+(x,0(),y))
s(x) -> s(+(0(),x))
x -> x
+(s(x),y) -> s(+(x,y,0()))
s(x) -> s(+(x,0()))
s(+(x,0(),y)) -> +(x,s(y))
s(+(0(),x)) -> s(x)
s(+(0(),x,y)) -> +(x,s(y))
s(+(0(),x)) -> s(x)
s(+(x,y)) -> s(+(y,x))
s(+(s(x),y,z)) -> s(+(x,y,s(z)))
s(+(s(x),y)) -> s(+(x,s(y)))
x -> x
s(x) -> s(+(0(),x))
+(x,s(y)) -> s(+(0(),x,y))
s(x) -> s(+(x,0()))
+(s(x),y) -> s(+(x,0(),y))
s(+(x,0())) -> s(x)
s(+(x,y,0())) -> +(s(x),y)
s(+(x,y)) -> s(+(y,x))
s(+(x,s(y))) -> s(+(s(x),y))
s(+(x,y,s(z))) -> s(+(s(x),y,z))
s(+(x,0())) -> s(x)
s(+(x,0(),y)) -> +(s(x),y)
+(x,y) -> +(y,x,0())
x -> +(x,0())
+(x,y) -> +(y,0(),x)
x -> +(0(),x)
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(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) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
s(+(x,y,z)) -> +(y,x,s(z))
s(+(x,y)) -> +(x,s(y))
s(+(x,y,z)) -> +(y,s(z),x)
s(+(x,y)) -> +(s(y),x)
s(+(x,y,z,w)) -> +(x,s(w),y,z)
s(+(x,y,z)) -> +(s(z),x,y)
s(+(x,y,z,w)) -> +(x,y,s(w),z)
s(+(x,y,z)) -> +(x,s(z),y)
s(+(x,y,z,w)) -> +(x,y,z,s(w))
s(+(x,y,z)) -> +(x,y,s(z))
+(s(+(x,y,z)),w) -> +(x,s(z),y,w)
+(s(+(x,y)),z) -> +(s(y),x,z)
+(s(+(x,y,z)),w) -> +(x,y,s(z),w)
+(s(+(x,y)),z) -> +(x,s(y),z)
s(+(x,y,z,w)) -> +(x,s(w),y,z)
s(+(x,y,z)) -> +(s(z),x,y)
s(+(x,y,z,w)) -> +(x,y,s(w),z)
s(+(x,y,z)) -> +(x,s(z),y)
s(+(x,y,z,w)) -> +(x,y,z,s(w))
s(+(x,y,z)) -> +(x,y,s(z))
+(x,s(+(y,z,w))) -> +(x,y,s(w),z)
+(x,s(+(y,z))) -> +(x,s(z),y)
+(x,s(+(y,z,w))) -> +(x,y,z,s(w))
+(x,s(+(y,z))) -> +(x,y,s(z))
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)
s(+(x,y)) -> +(s(x),y)
s(+(x,y,z)) -> +(s(x),z,y)
s(+(x,y)) -> +(y,s(x))
s(+(x,y,z)) -> +(z,s(x),y)
s(+(x,y,z)) -> +(y,z,s(x))
s(+(x,y,z,w)) -> +(y,z,s(x),w)
s(+(x,y,z)) -> +(y,s(x),z)
s(+(x,y,z,w)) -> +(y,s(x),z,w)
s(+(x,y,z)) -> +(s(x),y,z)
s(+(x,y,z,w)) -> +(s(x),y,z,w)
+(s(+(x,y)),z) -> +(y,s(x),z)
+(s(+(x,y,z)),w) -> +(y,s(x),z,w)
+(s(+(x,y)),z) -> +(s(x),y,z)
+(s(+(x,y,z)),w) -> +(s(x),y,z,w)
s(+(x,y,z)) -> +(y,z,s(x))
s(+(x,y,z,w)) -> +(y,z,s(x),w)
s(+(x,y,z)) -> +(y,s(x),z)
s(+(x,y,z,w)) -> +(y,s(x),z,w)
s(+(x,y,z)) -> +(s(x),y,z)
s(+(x,y,z,w)) -> +(s(x),y,z,w)
+(x,s(+(y,z))) -> +(x,z,s(y))
+(x,s(+(y,z,w))) -> +(x,z,s(y),w)
+(x,s(+(y,z))) -> +(x,s(y),z)
+(x,s(+(y,z,w))) -> +(x,s(y),z,w)