Certificate for #6632 ⟨a, b, c | aa=1, aabca=b⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [2], [3].

[2] bca=b

Axiom: aabca=b.

Reduce LHS:

[1](aa)bca
⇒ bca

Referenced by [3].

[3] bc=ba

Overlap of [2] bca=b with [1] aa=1:

bc a aa

Critical pair: bc=ba.

Defines rule #2.