Certificate for #25195 ⟨a, b | aa=a, ababb=bab⟩

Back:⟨a, b | aa=a, ababb=bab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] ababb=bab

Axiom: ababb=bab.

Referenced by [3], [4].

[3] abab=bab

Overlap of [1] aa=a with [2] ababb=bab:

a a ababb

Critical pair: abab=ababb.

Reduce RHS:

[2](ababb)
⇒ bab

Defines rule #2.

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

[4] babb=bab

Overlap of [2] ababb=bab with [3] abab=bab:

ababb abab

Critical pair: babb=bab.

Defines rule #3.

Referenced by [6].

[5] abbab=bbab

Overlap of [3] abab=bab with [3] abab=bab:

ab ab abab

Critical pair: abbab=babab.

Reduce RHS:

[3]b(abab)
⇒ bbab

Defines rule #4.

Referenced by [6].

[6] bbbab=bbab

Overlap of [4] babb=bab with [5] abbab=bbab:

b abb abbab

Critical pair: bbbab=babab.

Reduce RHS:

[3]b(abab)
⇒ bbab

Defines rule #5.