Certificate for #25909 ⟨a, b | ab=a, bbbb=bbaa⟩

Back:⟨a, b | ab=a, bbbb=bbaa⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [4].

[2] bbbb=bbaa

Axiom: bbbb=bbaa.

Defines rule #4.

Referenced by [3], [4].

[3] aaa=a

Overlap of [1] ab=a with [2] bbbb=bbaa:

a b bbbb

Critical pair: abbaa=abbb.

Reduce LHS:

[1](ab)baa
[1]⇒ (ab)aa
⇒ aaa

Reduce RHS:

[1](ab)bb
[1]⇒ (ab)b
[1]⇒ (ab)
⇒ a

Defines rule #2.

Referenced by [5].

[4] bbbaa=bbaa

Overlap of [2] bbbb=bbaa with [2] bbbb=bbaa:

b bbb bbbb

Critical pair: bbbaa=bbaab.

Reduce RHS:

[1]bba(ab)
⇒ bbaa

Referenced by [5].

[5] bbba=bba

Overlap of [4] bbbaa=bbaa with [3] aaa=a:

bbb aa aaa

Critical pair: bbba=bbaaa.

Reduce RHS:

[3]bb(aaa)
⇒ bba

Defines rule #3.