Certificate for #13246 ⟨a, b | bab=aaa, bba=ba⟩

Back:⟨a, b | bab=aaa, bba=ba⟩

Completion settings:

[1] aaa=bab

Axiom: bab=aaa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bba=ba

Axiom: bba=ba.

Defines rule #1.

Referenced by [4].

[3] abab=baba

Overlap of [1] aaa=bab with [1] aaa=bab:

a aa aaa

Critical pair: abab=baba.

Defines rule #3.

Referenced by [4].

[4] babaab=babaa

Overlap of [3] abab=baba with [3] abab=baba:

ab ab abab

Critical pair: abbaba=babaab.

Reduce LHS:

[2]a(bba)ba
[3]⇒ (abab)a
⇒ babaa

Flip LHS and RHS.

Defines rule #4.