Certificate for #19824 ⟨a, b | aaa=a, abbb=baa⟩

Back:⟨a, b | aaa=a, abbb=baa⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [4], [6], [8].

[2] abbb=baa

Axiom: abbb=baa.

Defines rule #3.

Referenced by [3], [6], [7], [8].

[3] aabaa=baa

Overlap of [1] aaa=a with [2] abbb=baa:

aa a abbb

Critical pair: aabaa=abbb.

Reduce RHS:

[2](abbb)
⇒ baa

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

[4] aaba=ba

Overlap of [3] aabaa=baa with [1] aaa=a:

aab aa aaa

Critical pair: aaba=baaa.

Reduce RHS:

[1]b(aaa)
⇒ ba

Defines rule #2.

Referenced by [5], [7].

[5] aabba=bba

Overlap of [3] aabaa=baa with [4] aaba=ba:

aab aa aaba

Critical pair: aabba=baaba.

Reduce RHS:

[4]b(aaba)
⇒ bba

Defines rule #6.

Referenced by [6], [7], [8].

[6] bbba=aba

Overlap of [3] aabaa=baa with [5] aabba=bba:

aab aa aabba

Critical pair: aabbba=baabba.

Reduce LHS:

[2]a(abbb)a
[1]⇒ ab(aaa)
⇒ aba

Reduce RHS:

[5]b(aabba)
⇒ bbba

Flip LHS and RHS.

Defines rule #5.

Referenced by [7], [8].

[7] baba=abba

Overlap of [5] aabba=bba with [5] aabba=bba:

aabb a aabba

Critical pair: aabbbba=bbaabba.

Reduce LHS:

[2]a(abbb)ba
[4]⇒ ab(aaba)
⇒ abba

Reduce RHS:

[5]bb(aabba)
[6]⇒ b(bbba)
⇒ baba

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] babba=ba

Overlap of [6] bbba=aba with [5] aabba=bba:

bbb a aabba

Critical pair: bbbbba=abaabba.

Reduce LHS:

[6]bb(bbba)
[7]⇒ b(baba)
⇒ babba

Reduce RHS:

[5]ab(aabba)
[2]⇒ (abbb)a
[1]⇒ b(aaa)
⇒ ba

Defines rule #7.