Certificate for #20246 ⟨a, b | aba=a, bbbb=bab⟩

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

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #5.

Referenced by [3], [4].

[2] bab=bbbb

Axiom: bbbb=bab.

Flip LHS and RHS.

Defines rule #3.

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

[3] abbbb=ab

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

a ba bab

Critical pair: abbbb=ab.

Defines rule #2.

Referenced by [5].

[4] bbbba=ba

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

b ab aba

Critical pair: ba=bbbba.

Flip LHS and RHS.

Defines rule #4.

[5] bbbbbbb=bbbb

Overlap of [2] bab=bbbb with [3] abbbb=ab:

b ab abbbb

Critical pair: bab=bbbbbbb.

Reduce LHS:

[2](bab)
⇒ bbbb

Flip LHS and RHS.

Defines rule #1.