Certificate for #89 ⟨a, b | abaab=b⟩

Back:⟨a, b | abaab=b⟩

Completion settings:

[1] abaab=b

Axiom: abaab=b.

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

[2] baab=abab

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

aba ab abaab

Critical pair: abab=baab.

Flip LHS and RHS.

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

[3] bab=abb

Overlap of [2] baab=abab with [1] abaab=b:

ba ab abaab

Critical pair: bab=ababaab.

Reduce RHS:

[1]ab(abaab)
⇒ abb

Defines rule #1.

Referenced by [4], [5].

[4] aaabb=b

Overlap of [1] abaab=b with [2] baab=abab:

a baab baab

Critical pair: aabab=b.

Reduce LHS:

[3]aa(bab)
⇒ aaabb

Defines rule #3.

[5] baab=aabb

Simplify [2] baab=abab.

Reduce RHS:

[3]a(bab)
⇒ aabb

Defines rule #2.