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

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

Completion settings:

[1] aab=ba

Axiom: aab=ba.

Referenced by [3].

[2] ab=bbbb

Axiom: bbbb=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] ba=bbbbbbb

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

a ab ab

Critical pair: abbbb=ba.

Reduce LHS:

[2](ab)bbb
⇒ bbbbbbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] bbbbbbbb=bbbbb

Overlap of [3] ba=bbbbbbb with [2] ab=bbbb:

b a ab

Critical pair: bbbbb=bbbbbbbb.

Flip LHS and RHS.

Defines rule #1.