Certificate for #2597 ⟨a, b | ababab=baba⟩

Back:⟨a, b | ababab=baba⟩

Completion settings:

[1] ababab=baba

Axiom: ababab=baba.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #2.

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

[3] ababab=bca

Simplify [1] ababab=baba.

Reduce RHS:

[2]b(ab)a
⇒ bca

Referenced by [4].

[4] bca=ccc

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

ababab ab

Critical pair: cabab=bca.

Reduce LHS:

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

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] cca=accc

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

a b bca

Critical pair: accc=cca.

Flip LHS and RHS.

Defines rule #4.

[6] cccb=bcc

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

bc a ab

Critical pair: bcc=cccb.

Flip LHS and RHS.

Defines rule #1.