Certificate for #6260 ⟨a, b | aaa=a, abbab=a⟩

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

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [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=aab

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

abb ab abba

Critical pair: abbabab=aba.

Reduce LHS:

[3](abba)bab
[4]⇒ (ababb)ab
⇒ aab

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7].

[6] abbb=aa

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

abb ab aba

Critical pair: abbaab=aa.

Reduce LHS:

[3](abba)ab
[5]⇒ (aba)bab
[3]⇒ a(abba)b
[5]⇒ a(aba)bb
[1]⇒ (aaa)bbb
⇒ abbb

Defines rule #4.

[7] abba=aabb

Simplify [3] abba=abab.

Reduce RHS:

[5](aba)b
⇒ aabb

Defines rule #3.