Certificate for #20215 ⟨a, b | aba=a, abba=aab⟩

Back:⟨a, b | aba=a, abba=aab⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #2.

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

[2] abba=aab

Axiom: abba=aab.

Defines rule #3.

Referenced by [3], [4].

[3] aaab=aab

Overlap of [2] abba=aab with [1] aba=a:

abb a aba

Critical pair: abba=aabba.

Reduce LHS:

[2](abba)
⇒ aab

Reduce RHS:

[2]a(abba)
⇒ aaab

Flip LHS and RHS.

Referenced by [5].

[4] aabbba=aab

Overlap of [2] abba=aab with [2] abba=aab:

abb a abba

Critical pair: abbaab=aabbba.

Reduce LHS:

[2](abba)ab
[1]⇒ a(aba)b
⇒ aab

Flip LHS and RHS.

Defines rule #4.

[5] aaa=aa

Overlap of [3] aaab=aab with [1] aba=a:

aa ab aba

Critical pair: aaa=aaba.

Reduce RHS:

[1]a(aba)
⇒ aa

Defines rule #1.