Certificate for #1794 ⟨a, b | ababbbaab=b⟩

Back:⟨a, b | ababbbaab=b⟩

Completion settings:

[1] ababbbaab=b

Axiom: ababbbaab=b.

Defines rule #3.

Referenced by [2], [3].

[2] ababbbab=babbbaab

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

ababbba ab ababbbaab

Critical pair: ababbbab=babbbaab.

Defines rule #2.

Referenced by [3].

[3] ababbbb=babbbab

Overlap of [2] ababbbab=babbbaab with [1] ababbbaab=b:

ababbb ab ababbbaab

Critical pair: ababbbb=babbbaababbbaab.

Reduce RHS:

[1]babbba(ababbbaab)
⇒ babbbab

Defines rule #1.