Certificate for #2612 ⟨a, b | ababba=bbab⟩

Back:⟨a, b | ababba=bbab⟩

Completion settings:

[1] ababba=bbab

Axiom: ababba=bbab.

Referenced by [3].

[2] bbab=c

Axiom: bbab=c.

Defines rule #4.

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

[3] ababba=c

Simplify [1] ababba=bbab.

Reduce RHS:

[2](bbab)
⇒ c

Defines rule #5.

Referenced by [5], [6].

[4] bbac=cbab

Overlap of [2] bbab=c with [2] bbab=c:

bba b bbab

Critical pair: bbac=cbab.

Defines rule #3.

[5] abac=cb

Overlap of [3] ababba=c with [2] bbab=c:

aba bba bbab

Critical pair: abac=cb.

Defines rule #1.

[6] bbc=cabba

Overlap of [2] bbab=c with [3] ababba=c:

bb ab ababba

Critical pair: bbc=cabba.

Defines rule #2.