Certificate for #408 ⟨a, b | abbaaab=b⟩

Back:⟨a, b | abbaaab=b⟩

Completion settings:

[1] abbaaab=b

Axiom: abbaaab=b.

Defines rule #4.

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

[2] abbaab=bbaaab

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

abbaa ab abbaaab

Critical pair: abbaab=bbaaab.

Defines rule #3.

Referenced by [3].

[3] abbab=bbaab

Overlap of [2] abbaab=bbaaab with [1] abbaaab=b:

abba ab abbaaab

Critical pair: abbab=bbaaabbaaab.

Reduce RHS:

[1]bbaa(abbaaab)
⇒ bbaab

Defines rule #2.

Referenced by [4].

[4] abbb=bbab

Overlap of [3] abbab=bbaab with [1] abbaaab=b:

abb ab abbaaab

Critical pair: abbb=bbaabbaaab.

Reduce RHS:

[1]bba(abbaaab)
⇒ bbab

Defines rule #1.