Certificate for #12386 ⟨a, b | aaba=ba, abbb=a⟩

Back:⟨a, b | aaba=ba, abbb=a⟩

Completion settings:

[1] aaba=ba

Axiom: aaba=ba.

Defines rule #2.

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

[2] abbb=a

Axiom: abbb=a.

Defines rule #3.

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

[3] aabba=bba

Overlap of [1] aaba=ba with [1] aaba=ba:

aab a aaba

Critical pair: aabba=baaba.

Reduce RHS:

[1]b(aaba)
⇒ bba

Defines rule #6.

Referenced by [4], [5].

[4] bbba=aaa

Overlap of [1] aaba=ba with [3] aabba=bba:

aab a aabba

Critical pair: aabbba=baabba.

Reduce LHS:

[2]a(abbb)a
⇒ aaa

Reduce RHS:

[3]b(aabba)
⇒ bbba

Flip LHS and RHS.

Defines rule #5.

Referenced by [5].

[5] baaa=ba

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

aabb a aabba

Critical pair: aabbbba=bbaabba.

Reduce LHS:

[2]a(abbb)ba
[1]⇒ (aaba)
⇒ ba

Reduce RHS:

[3]bb(aabba)
[4]⇒ b(bbba)
⇒ baaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] aaaa=aa

Overlap of [2] abbb=a with [5] baaa=ba:

abb b baaa

Critical pair: abbba=aaaa.

Reduce LHS:

[2](abbb)a
⇒ aa

Flip LHS and RHS.

Defines rule #1.