Certificate for #5768 ⟨a, b, c | aa=b, cbc=bc⟩

Completion settings:

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

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

Axiom: cbc=bc.

Reduce LHS:

[1]	c(b)c
	⇒ caac

Reduce RHS:

[1]	(b)c
	⇒ aac

Referenced by [4].

Axiom: ac=d.

Defines rule #1.

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

Reduce RHS:

[3]	a(ac)
	⇒ ad

Referenced by [5].

ca ac ac

Critical pair: cad=ad.

Defines rule #2.

Referenced by [6].

a c cad

Critical pair: aad=dad.

Defines rule #3.