Certificate for #25200 ⟨a, b | aa=a, abbab=aba⟩

Back:⟨a, b | aa=a, abbab=aba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abbab=aba

Axiom: abbab=aba.

Defines rule #4.

Referenced by [3].

[3] ababab=aba

Overlap of [2] abbab=aba with [2] abbab=aba:

abb ab abbab

Critical pair: abbaba=ababab.

Reduce LHS:

[2](abbab)a
[1]⇒ ab(aa)
⇒ aba

Flip LHS and RHS.

Referenced by [4], [5].

[4] ababa=abab

Overlap of [3] ababab=aba with [3] ababab=aba:

ab abab ababab

Critical pair: ababa=abaab.

Reduce RHS:

[1]ab(aa)b
⇒ abab

Defines rule #2.

Referenced by [5].

[5] ababb=aba

Overlap of [3] ababab=aba with [4] ababa=abab:

ababab ababa

Critical pair: ababb=aba.

Defines rule #3.