Certificate for #12400 ⟨a, b | aaba=ba, bbba=a⟩

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

Completion settings:

[1] aaba=ba

Axiom: aaba=ba.

Defines rule #2.

Referenced by [3], [4].

[2] bbba=a

Axiom: bbba=a.

Defines rule #3.

Referenced by [4].

[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 #4.

Referenced by [4].

[4] aaa=a

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

aab a aabba

Critical pair: aabbba=baabba.

Reduce LHS:

[2]aa(bbba)
⇒ aaa

Reduce RHS:

[3]b(aabba)
[2]⇒ (bbba)
⇒ a

Defines rule #1.