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 2021)

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 Parallel Closed

Confluence is proven since the TRS is (almost) parallel closed. The joins can be performed using 1 parallel step(s).