Certificate for #188 ⟨a, b | abaaab=b⟩

Back:⟨a, b | abaaab=b⟩

Completion settings:

[1] abaaab=b

Axiom: abaaab=b.

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

[2] baaab=abaab

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

abaa ab abaaab

Critical pair: abaab=baaab.

Flip LHS and RHS.

Referenced by [3], [5], [6].

[3] baab=abab

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

baa ab abaaab

Critical pair: baab=abaabaaab.

Reduce RHS:

[1]aba(abaaab)
⇒ abab

Referenced by [4], [5], [6], [7].

[4] bab=abb

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

ba ab abaaab

Critical pair: bab=ababaaab.

Reduce RHS:

[1]ab(abaaab)
⇒ abb

Defines rule #1.

Referenced by [5], [6], [7].

[5] aaaabb=b

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

a baaab baaab

Critical pair: aabaab=b.

Reduce LHS:

[3]aa(baab)
[4]⇒ aaa(bab)
⇒ aaaabb

Defines rule #4.

[6] baaab=aaabb

Simplify [2] baaab=abaab.

Reduce RHS:

[3]a(baab)
[4]⇒ aa(bab)
⇒ aaabb

Defines rule #3.

[7] baab=aabb

Simplify [3] baab=abab.

Reduce RHS:

[4]a(bab)
⇒ aabb

Defines rule #2.