Certificate for #25256 ⟨a, b | aa=a, bbbbb=aba⟩

Back:⟨a, b | aa=a, bbbbb=aba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #4.

Referenced by [3], [4].

[2] aba=bbbbb

Axiom: bbbbb=aba.

Flip LHS and RHS.

Defines rule #5.

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

[3] abbbbb=bbbbb

Overlap of [1] aa=a with [2] aba=bbbbb:

a a aba

Critical pair: abbbbb=aba.

Reduce RHS:

[2](aba)
⇒ bbbbb

Defines rule #2.

Referenced by [5].

[4] bbbbba=bbbbb

Overlap of [2] aba=bbbbb with [1] aa=a:

ab a aa

Critical pair: aba=bbbbba.

Reduce LHS:

[2](aba)
⇒ bbbbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbbbbbbb=bbbbbb

Overlap of [2] aba=bbbbb with [3] abbbbb=bbbbb:

ab a abbbbb

Critical pair: abbbbbb=bbbbbbbbbb.

Reduce LHS:

[3](abbbbb)b
⇒ bbbbbb

Flip LHS and RHS.

Defines rule #1.