Certificate for #3871 ⟨a, b | aaba=ba, bbbb=1⟩

Back:⟨a, b | aaba=ba, bbbb=1⟩

Completion settings:

[1] aaba=ba

Axiom: aaba=ba.

Defines rule #2.

Referenced by [3], [4].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #3.

Referenced by [5].

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

[4] aabbba=bbba

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

aab a aabba

Critical pair: aabbba=baabba.

Reduce RHS:

[3]b(aabba)
⇒ bbba

Defines rule #5.

[5] aaa=a

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

aabb a aabba

Critical pair: aabbbba=bbaabba.

Reduce LHS:

[2]aa(bbbb)a
⇒ aaa

Reduce RHS:

[3]bb(aabba)
[2]⇒ (bbbb)a
⇒ a

Defines rule #1.