Certification Problem

Input (COPS 977)

We consider the TRS containing the following rules:

foo(0(x)) 0(s(p(p(p(s(s(s(p(s(x)))))))))) (1)
foo(s(x)) p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x)))))))))))))))))))))))))) (2)
bar(0(x)) 0(p(s(s(s(x))))) (3)
bar(s(x)) p(s(p(p(s(s(foo(s(p(p(s(s(x)))))))))))) (4)
p(p(s(x))) p(x) (5)
p(s(x)) x (6)
p(0(x)) 0(s(s(s(s(x))))) (7)

The underlying signature is as follows:

{foo/1, 0/1, s/1, p/1, bar/1}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ACP @ CoCo 2020)

1 Strongly closed

Confluence is proven since the TRS is strongly closed. The joins can be performed using 0 step(s).