Certificate for #3792 ⟨a, b | ababbbbaab=b⟩

Back:⟨a, b | ababbbbaab=b⟩

Completion settings:

[1] ababbbbaab=b

Axiom: ababbbbaab=b.

Defines rule #3.

Referenced by [2], [3].

[2] ababbbbab=babbbbaab

Overlap of [1] ababbbbaab=b with [1] ababbbbaab=b:

ababbbba ab ababbbbaab

Critical pair: ababbbbab=babbbbaab.

Defines rule #2.

Referenced by [3].

[3] ababbbbb=babbbbab

Overlap of [2] ababbbbab=babbbbaab with [1] ababbbbaab=b:

ababbbb ab ababbbbaab

Critical pair: ababbbbb=babbbbaababbbbaab.

Reduce RHS:

[1]babbbba(ababbbbaab)
⇒ babbbbab

Defines rule #1.