Certificate for #3714 ⟨a, b | abaaabaaab=b⟩

Back:⟨a, b | abaaabaaab=b⟩

Completion settings:

[1] abaaabaaab=b

Axiom: abaaabaaab=b.

Defines rule #4.

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

[2] abaab=baaab

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

abaa abaaab abaaabaaab

Critical pair: abaab=baaab.

Defines rule #3.

Referenced by [3].

[3] abab=baab

Overlap of [2] abaab=baaab with [1] abaaabaaab=b:

aba ab abaaabaaab

Critical pair: abab=baaabaaabaaab.

Reduce RHS:

[1]baa(abaaabaaab)
⇒ baab

Defines rule #2.

Referenced by [4].

[4] abb=bab

Overlap of [3] abab=baab with [1] abaaabaaab=b:

ab ab abaaabaaab

Critical pair: abb=baabaaabaaab.

Reduce RHS:

[1]ba(abaaabaaab)
⇒ bab

Defines rule #1.