Certificate for #3473 ⟨a, b, c | ba=ac, cab=b⟩

Completion settings:

Auxiliary generators:
1. d = aab
Reduction order:
- Right-to-left recursive path with deg(c) = deg(d) = 0, c < d; deg(b) = 1; deg(a) = 2

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Referenced by [4], [12].

[2] cab=b

Axiom: cab=b.

Referenced by [4], [6], [9].

[3] aab=d

Axiom: aab=d.

Referenced by [4], [5].

[4] ab=bd

Overlap of [1] ac=ba with [2] cab=b:

a c cab

Critical pair: ab=baab.

Reduce RHS:

[3]	b(aab)
	⇒ bd

Referenced by [5], [7], [9].

[5] bdd=d

Simplify [3] aab=d.

Reduce LHS:

[4]	a(ab)
[4]	⇒ (ab)d
	⇒ bdd

Referenced by [6], [7], [10].

[6] cad=d

Overlap of [2] cab=b with [5] bdd=d:

ca b bdd

Critical pair: cad=bdd.

Reduce RHS:

[5]	(bdd)
	⇒ d

Referenced by [8].

[7] ad=dd

Overlap of [4] ab=bd with [5] bdd=d:

a b bdd

Critical pair: ad=bddd.

Reduce RHS:

[5]	(bdd)d
	⇒ dd

Defines rule #4.

Referenced by [8].

[8] cdd=d

Simplify [6] cad=d.

Reduce LHS:

[7]	c(ad)
	⇒ cdd

Defines rule #1.

[9] cbd=b

Overlap of [2] cab=b with [4] ab=bd:

c ab ab

Critical pair: cbd=b.

Referenced by [10], [11].

[10] bd=cd

Overlap of [9] cbd=b with [5] bdd=d:

c bd bdd

Critical pair: cd=bd.

Flip LHS and RHS.

Referenced by [11].

[11] b=ccd

Overlap of [9] cbd=b with [10] bd=cd:

c bd bd

Critical pair: ccd=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [12].

[12] ac=ccda

Simplify [1] ac=ba.

Reduce RHS:

[11]	(b)a
	⇒ ccda

Defines rule #3.