---- CR(R)
---- [van Oostrom, RTA 2008].
R:
p(x) -> q(x)
p(x) -> r(x)
q(x) -> s(p(x))
r(x) -> s(p(x))
s(x) -> f(p(x))

Label:
[p(x) -> q(x)] = 1
[p(x) -> r(x)] = 2
[q(x) -> s(p(x))] = 0
[r(x) -> s(p(x))] = 0
[s(x) -> f(p(x))] = 0