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

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [5], [6].

[2] abbab=a

Axiom: abbab=a.

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

[3] abba=abab

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

abb ab abbab

Critical pair: abba=abab.

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

[4] ababb=a

Overlap of [2] abbab=a with [3] abba=abab:

abbab abba

Critical pair: ababb=a.

Referenced by [5].

[5] aba=ab

Overlap of [2] abbab=a with [3] abba=abab:

abb ab abba

Critical pair: abbabab=aba.

Reduce LHS:

[3](abba)bab
[4]⇒ (ababb)ab
[1]⇒ (aa)b
⇒ ab

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7].

[6] abbb=a

Overlap of [2] abbab=a with [5] aba=ab:

abb ab aba

Critical pair: abbab=aa.

Reduce LHS:

[3](abba)b
[5]⇒ (aba)bb
⇒ abbb

Reduce RHS:

[1](aa)
⇒ a

Defines rule #4.

[7] abba=abb

Simplify [3] abba=abab.

Reduce RHS:

[5](aba)b
⇒ abb

Defines rule #3.