Certificate for #27079 ⟨a, b | aa=1, aabbbba=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [2], [3].

[2] bbbba=bb

Axiom: aabbbba=bb.

Reduce LHS:

[1](aa)bbbba
⇒ bbbba

Referenced by [3].

[3] bbbb=bba

Overlap of [2] bbbba=bb with [1] aa=1:

bbbb a aa

Critical pair: bbbb=bba.

Defines rule #2.

Referenced by [4].

[4] bbab=bbba

Overlap of [3] bbbb=bba with [3] bbbb=bba:

b bbb bbbb

Critical pair: bbba=bbab.

Flip LHS and RHS.

Defines rule #3.