Certificate for #13256 ⟨a, b | bab=aba, bba=ab⟩

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

Completion settings:

[1] aba=bab

Axiom: bab=aba.

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], [6].

[3] aba=bbba

Simplify [1] aba=bab.

Reduce RHS:

[2]b(ab)
⇒ bbba

Referenced by [4].

[4] bbaa=bbba

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

aba ab

Critical pair: bbaa=bbba.

Defines rule #3.

Referenced by [5], [6].

[5] bbbbbbba=bbbbbba

Overlap of [2] ab=bba with [4] bbaa=bbba:

a b bbaa

Critical pair: abbba=bbabaa.

Reduce LHS:

[2](ab)bba
[2]⇒ bb(ab)ba
[2]⇒ bbbb(ab)a
[4]⇒ bbbb(bbaa)
⇒ bbbbbbba

Reduce RHS:

[2]bb(ab)aa
[4]⇒ bb(bbaa)a
[4]⇒ bbb(bbaa)
⇒ bbbbbba

Referenced by [6].

[6] bbbbbba=bbbbba

Overlap of [4] bbaa=bbba with [2] ab=bba:

bba a ab

Critical pair: bbabba=bbbab.

Reduce LHS:

[2]bb(ab)ba
[2]⇒ bbbb(ab)a
[4]⇒ bbbb(bbaa)
[5]⇒ (bbbbbbba)
⇒ bbbbbba

Reduce RHS:

[2]bbb(ab)
⇒ bbbbba

Defines rule #1.