---- CR(R cup S)
---- [Klein and Hirokawa, 2012]
R:
eq(n,xs,xs) -> T()
eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
S:
nats() -> c(0(),inc(nats()))
inc(c(x,xs)) -> c(s(x),inc(xs))
CP_S(R):
T() -> eq(___y21279,___y21281,___y21281)
eq(___y21305,___y21308,___y21308) -> T()
CR(S):
see below.

---- CR(R)
---- [Hirokawa and Middeldorp, 2011]
R:
nats() -> c(0(),inc(nats()))
inc(c(x,xs)) -> c(s(x),inc(xs))
CPS'(R):

CP(R):