Certification Problem

Input

We consider the TRS containing the following rules:

f(f(x))	→	f(g(f(x),f(x)))
a	→	b
a	→	c
b	→	d
c	→	d
c	→	e1
e1	→	e2
e1	→	d
e2	→	d

The underlying signature is as follows:

{f/1, g/2, a/0, b/0, c/0, d/0, e1/0, e2/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi + manual amendments)

1 Simultaneous Critical Pairs Closed

Confluence is proven by Okui's criterion, that all simultaneous critical pairs are development closed. The simultaneous critical pairs can be joined as follows. Here, ↔ is always chosen as an appropriate rewrite relation which is automatically inferred by the certifier.

The critical peak s = f(f(g(f(x11),f(x11))))⇐→ f(g(f(f(x11)),f(f(x11)))) = t can be joined as follows.
s ↔ f(g(f(g(f(x11),f(x11))),f(g(f(x11),f(x11))))) ↔ t
The critical peak s = f(g(f(f(x)),f(f(x))))⇐→ f(f(g(f(x),f(x)))) = t can be joined as follows.
s ↔ f(g(f(g(f(x),f(x))),f(g(f(x),f(x))))) ↔ t
The critical peak s = f(g(f(f(g(f(x14),f(x14)))),f(f(g(f(x14),f(x14))))))⇐→ f(f(g(f(f(x14)),f(f(x14))))) = t can be joined as follows.
s ↔ f(g(f(g(f(g(f(x14),f(x14))),f(g(f(x14),f(x14))))),f(g(f(g(f(x14),f(x14))),f(g(f(x14),f(x14))))))) ↔ t
The critical peak s = c⇐→ b = t can be joined as follows.
s ↔ e1 ↔ e2 ↔ d ↔ t
The critical peak s = b⇐→ c = t can be joined as follows.
s ↔ d ↔ t
The critical peak s = e1⇐→ d = t can be joined as follows.
s ↔ t
The critical peak s = d⇐→ e1 = t can be joined as follows.
s ↔ t
The critical peak s = d⇐→ e2 = t can be joined as follows.
s ↔ t
The critical peak s = e2⇐→ d = t can be joined as follows.
s ↔ t