Certificate for #9180 ⟨a, b | aa=a, bbbb=aba⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #4.

Referenced by [3], [4].

[2] aba=bbbb

Axiom: bbbb=aba.

Flip LHS and RHS.

Defines rule #5.

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

[3] abbbb=bbbb

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

a a aba

Critical pair: abbbb=aba.

Reduce RHS:

[2](aba)
⇒ bbbb

Defines rule #2.

Referenced by [5].

[4] bbbba=bbbb

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

ab a aa

Critical pair: aba=bbbba.

Reduce LHS:

[2](aba)
⇒ bbbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbbbbb=bbbbb

Overlap of [2] aba=bbbb with [3] abbbb=bbbb:

ab a abbbb

Critical pair: abbbbb=bbbbbbbb.

Reduce LHS:

[3](abbbb)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #1.