Certificate for #5542 ⟨a, b, c | ab=c, acba=c⟩

Completion settings:

Auxiliary generators:
1. d = cb
Reduction order:
- Left-to-right recursive path with deg(a) = deg(d) = 0, a < d; deg(c) = deg(b) = 1, c < b

[1] ab=c

Axiom: ab=c.

Referenced by [5], [6].

[2] acba=c

Axiom: acba=c.

Referenced by [4].

[3] cb=d

Axiom: cb=d.

Referenced by [4], [5].

[4] c=ada

Overlap of [2] acba=c with [3] cb=d:

a cba cb

Critical pair: ada=c.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] adada=d

Overlap of [3] cb=d with [4] c=ada:

cb c

Critical pair: adab=d.

Reduce LHS:

[1]	ad(ab)
[4]	⇒ ad(c)
	⇒ adada

Defines rule #2.

Referenced by [7], [8].

[6] ab=ada

Simplify [1] ab=c.

Reduce RHS:

[4]	(c)
	⇒ ada

Defines rule #4.

Referenced by [7].

[7] db=dda

Overlap of [5] adada=d with [6] ab=ada:

adad a ab

Critical pair: adadada=db.

Reduce LHS:

[5]	(adada)da
	⇒ dda

Flip LHS and RHS.

Referenced by [9].

[8] dda=add

Overlap of [5] adada=d with [5] adada=d:

ad ada adada

Critical pair: add=dda.

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[9] db=add

Simplify [7] db=dda.

Reduce RHS:

[8]	(dda)
	⇒ add

Defines rule #5.