---- CR(R cup S)
---- [Klein and Hirokawa, 2012]
R:
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
S:

CP_S(R):
0() -> 0()
s(___y266) -> s(+(0(),___y266))
s(+(___y274,0())) -> s(___y274)
s(+(___y277,s(___y280))) -> s(+(s(___y277),___y280))
0() -> 0()
s(___y284) -> s(+(___y284,0()))
s(+(0(),___y292)) -> s(___y292)
s(+(s(___y296),___y295)) -> s(+(___y296,s(___y295)))
CR(S):
see below.

---- CR(R)
---- [Hirokawa and Middeldorp, 2011]
R:

CPS'(R):

CP(R):