Certification Problem

Input

We consider two TRSs R and S where R contains the rules

f(f(x)) → f(g(f(x),f(x))) (A)
a → c (C)
b → d (D)
e1 → d (H)
e2 → d (I)

and S contains the following rules:

f(f(x)) → f(g(f(x),f(x))) (A)
a → b (B)
c → d (E)
c → e1 (F)
e1 → e2 (G)
e2 → d (I)

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 commutation.

Answer / Result

Yes.

Proof (by confluence proof of csi + manual change into commutation proof)

1 Simultaneous Critical Pairs Closed

Commutation is proven by a generalization of Okui's criterion to commutation, that all simultaneous critical pairs u ⇐R . →S v are development closed: u →S* . ⇐R v. 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. />