Certificate for #4829 ⟨a, b | abababba=bba⟩

Back:⟨a, b | abababba=bba⟩

Completion settings:

[1] abababba=bba

Axiom: abababba=bba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #2.

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

[3] abababba=bc

Simplify [1] abababba=bba.

Reduce RHS:

[2]b(ba)
⇒ bc

Referenced by [4].

[4] accbc=bc

Overlap of [3] abababba=bc with [2] ba=c:

a bababba ba

Critical pair: acbabba=bc.

Reduce LHS:

[2]ac(ba)bba
[2]⇒ accb(ba)
⇒ accbc

Defines rule #1.

Referenced by [5].

[5] bbc=cccbc

Overlap of [2] ba=c with [4] accbc=bc:

b a accbc

Critical pair: bbc=cccbc.

Defines rule #3.