Certificate for #6712 ⟨a, b | aab=b, bbaa=ba⟩

Back:⟨a, b | aab=b, bbaa=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3], [4].

[2] bbaa=ba

Axiom: bbaa=ba.

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

[3] bab=bbb

Overlap of [2] bbaa=ba with [1] aab=b:

bb aa aab

Critical pair: bbb=bab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [4], [5].

[4] bbbb=bb

Overlap of [2] bbaa=ba with [1] aab=b:

bba a aab

Critical pair: bbab=baab.

Reduce LHS:

[3]b(bab)
⇒ bbbb

Reduce RHS:

[1]b(aab)
⇒ bb

Defines rule #4.

Referenced by [5].

[5] bbba=ba

Overlap of [3] bab=bbb with [2] bbaa=ba:

ba b bbaa

Critical pair: baba=bbbbaa.

Reduce LHS:

[3](bab)a
⇒ bbba

Reduce RHS:

[4](bbbb)aa
[2]⇒ (bbaa)
⇒ ba

Defines rule #5.

Referenced by [6].

[6] baa=bba

Overlap of [5] bbba=ba with [2] bbaa=ba:

b bba bbaa

Critical pair: bba=baa.

Flip LHS and RHS.

Defines rule #2.