Certification Problem

Input (COPS 111)

We consider the TRS containing the following rules:

a b (1)
a c (2)
a e (3)
b d (4)
c a (5)
d a (6)
d e (7)
g(x) h(a) (8)
h(x) e (9)

The underlying signature is as follows:

{a/0, b/0, c/0, e/0, d/0, g/1, h/1}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2020)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

h(x) e (9)
g(x) h(a) (8)
d e (7)
d a (6)
c a (5)
b d (4)
a e (3)
a c (2)
a b (1)
g(x) e (10)
g(x) h(e) (11)
g(x) h(c) (12)
g(x) h(b) (13)
d c (14)
d b (15)
c e (16)
c c (17)
c b (18)
b e (19)
b a (20)
a a (21)
a d (22)

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Strongly closed

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