Certificate for #1790 ⟨a, b | ababbaaab=b⟩

Back:⟨a, b | ababbaaab=b⟩

Completion settings:

[1] ababbaaab=b

Axiom: ababbaaab=b.

Defines rule #4.

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

[2] ababbaab=babbaaab

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

ababbaa ab ababbaaab

Critical pair: ababbaab=babbaaab.

Defines rule #3.

Referenced by [3].

[3] ababbab=babbaab

Overlap of [2] ababbaab=babbaaab with [1] ababbaaab=b:

ababba ab ababbaaab

Critical pair: ababbab=babbaaababbaaab.

Reduce RHS:

[1]babbaa(ababbaaab)
⇒ babbaab

Defines rule #2.

Referenced by [4].

[4] ababbb=babbab

Overlap of [3] ababbab=babbaab with [1] ababbaaab=b:

ababb ab ababbaaab

Critical pair: ababbb=babbaababbaaab.

Reduce RHS:

[1]babba(ababbaaab)
⇒ babbab

Defines rule #1.