Certificate for #13245 ⟨a, b | bab=aaa, bba=ab⟩

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

Completion settings:

[1] aaa=bab

Axiom: bab=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] aaa=bbba

Simplify [1] aaa=bab.

Reduce RHS:

[2]b(ab)
⇒ bbba

Defines rule #4.

Referenced by [4], [5].

[4] bbbbbbaa=bbbaa

Overlap of [3] aaa=bbba with [3] aaa=bbba:

a aa aaa

Critical pair: abbba=bbbaa.

Reduce LHS:

[2](ab)bba
[2]⇒ bb(ab)ba
[2]⇒ bbbb(ab)a
⇒ bbbbbbaa

Defines rule #3.

Referenced by [5].

[5] bbbbbbbba=bbbbba

Overlap of [3] aaa=bbba with [2] ab=bba:

aa a ab

Critical pair: aabba=bbbab.

Reduce LHS:

[2]a(ab)ba
[2]⇒ (ab)baba
[2]⇒ bb(ab)aba
[2]⇒ bbbba(ab)a
[2]⇒ bbbb(ab)baa
[2]⇒ bbbbbb(ab)aa
[4]⇒ bb(bbbbbbaa)a
[3]⇒ bbbbb(aaa)
⇒ bbbbbbbba

Reduce RHS:

[2]bbb(ab)
⇒ bbbbba

Defines rule #1.