Certificate for #6660 ⟨a, b | aab=a, bbbb=ba⟩

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

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] ba=bbbb

Axiom: bbbb=ba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aa=abbb

Overlap of [1] aab=a with [2] ba=bbbb:

aa b ba

Critical pair: aabbbb=aa.

Reduce LHS:

[1](aab)bbb
⇒ abbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[4] bbbbbbbb=bbbb

Overlap of [2] ba=bbbb with [1] aab=a:

b a aab

Critical pair: ba=bbbbab.

Reduce LHS:

[2](ba)
⇒ bbbb

Reduce RHS:

[2]bbb(ba)b
⇒ bbbbbbbb

Flip LHS and RHS.

Defines rule #1.

[5] abbbb=a

Overlap of [1] aab=a with [3] aa=abbb:

aab aa

Critical pair: abbbb=a.

Defines rule #2.