Certificate for #12958 ⟨a, b | aba=aab, bbab=a⟩

Back:⟨a, b | aba=aab, bbab=a⟩

Completion settings:

[1] aba=aab

Axiom: aba=aab.

Defines rule #1.

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

[2] bbab=a

Axiom: bbab=a.

Defines rule #3.

Referenced by [3], [5].

[3] bbaa=aabb

Overlap of [2] bbab=a with [2] bbab=a:

bba b bbab

Critical pair: bbaa=abab.

Reduce RHS:

[1](aba)b
⇒ aabb

Defines rule #2.

Referenced by [5].

[4] aabba=aaabb

Overlap of [1] aba=aab with [1] aba=aab:

ab a aba

Critical pair: abaab=aabba.

Reduce LHS:

[1](aba)ab
[1]⇒ a(aba)b
⇒ aaabb

Flip LHS and RHS.

Defines rule #4.

[5] aabbb=aa

Overlap of [2] bbab=a with [1] aba=aab:

bb ab aba

Critical pair: bbaab=aa.

Reduce LHS:

[3](bbaa)b
⇒ aabbb

Defines rule #5.