Certificate for #2591 ⟨a, b | ababab=aaba⟩

Back:⟨a, b | ababab=aaba⟩

Completion settings:

[1] ababab=aaba

Axiom: ababab=aaba.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #4.

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

[3] ababab=aca

Simplify [1] ababab=aaba.

Reduce RHS:

[2]a(ab)a
⇒ aca

Referenced by [4].

[4] aca=ccc

Overlap of [3] ababab=aca with [2] ab=c:

ababab ab

Critical pair: cabab=aca.

Reduce LHS:

[2]c(ab)ab
[2]⇒ cc(ab)
⇒ ccc

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] cccb=acc

Overlap of [4] aca=ccc with [2] ab=c:

ac a ab

Critical pair: acc=cccb.

Flip LHS and RHS.

Defines rule #2.

[6] cccca=acccc

Overlap of [4] aca=ccc with [4] aca=ccc:

ac a aca

Critical pair: acccc=cccca.

Flip LHS and RHS.

Defines rule #1.