Certificate for #25699 ⟨a, b | aa=a, baba=abbb⟩

Back:⟨a, b | aa=a, baba=abbb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [5].

[2] abbb=baba

Axiom: baba=abbb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [5].

[3] ababa=baba

Overlap of [1] aa=a with [2] abbb=baba:

a a abbb

Critical pair: ababa=abbb.

Reduce RHS:

[2](abbb)
⇒ baba

Defines rule #3.

Referenced by [4], [5].

[4] abbaba=bbaba

Overlap of [3] ababa=baba with [3] ababa=baba:

ab aba ababa

Critical pair: abbaba=bababa.

Reduce RHS:

[3]b(ababa)
⇒ bbaba

Defines rule #5.

Referenced by [5].

[5] bbbaba=bbaba

Overlap of [4] abbaba=bbaba with [3] ababa=baba:

abb aba ababa

Critical pair: abbbaba=bbababa.

Reduce LHS:

[2](abbb)aba
[1]⇒ bab(aa)ba
[3]⇒ b(ababa)
⇒ bbaba

Reduce RHS:

[3]bb(ababa)
⇒ bbbaba

Flip LHS and RHS.

Defines rule #4.