Certificate for #1847 ⟨a, b, c | aba=ac, ccc=1⟩

Back:⟨a, b, c | aba=ac, ccc=1⟩

Completion settings:

[1] ac=aba

Axiom: aba=ac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] ccc=1

Axiom: ccc=1.

Defines rule #3.

Referenced by [3].

[3] abababa=a

Overlap of [1] ac=aba with [2] ccc=1:

a c ccc

Critical pair: a=abacc.

Reduce RHS:

[1]ab(ac)c
[1]⇒ abab(ac)
⇒ abababa

Flip LHS and RHS.

Defines rule #1.