Certificate for #4822 ⟨a, b | abababab=baa⟩

Back:⟨a, b | abababab=baa⟩

Completion settings:

[1] abababab=baa

Axiom: abababab=baa.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] abababab=ca

Simplify [1] abababab=baa.

Reduce RHS:

[2](ba)a
⇒ ca

Referenced by [4].

[4] ca=acccb

Overlap of [3] abababab=ca with [2] ba=c:

a bababab ba

Critical pair: acbabab=ca.

Reduce LHS:

[2]ac(ba)bab
[2]⇒ acc(ba)b
⇒ acccb

Flip LHS and RHS.

Defines rule #2.