Certificate for #14361 ⟨a, b | aaaa=a, babab=a⟩

Back:⟨a, b | aaaa=a, babab=a⟩

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #2.

Referenced by [4], [6].

[2] babab=a

Axiom: babab=a.

Referenced by [3], [5].

[3] baa=aab

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

ba bab babab

Critical pair: baa=aab.

Referenced by [4].

[4] ba=ab

Overlap of [3] baa=aab with [1] aaaa=a:

b aa aaaa

Critical pair: ba=aabaa.

Reduce RHS:

[3]aa(baa)
[1]⇒ (aaaa)b
⇒ ab

Defines rule #1.

Referenced by [5].

[5] aabbb=a

Overlap of [2] babab=a with [4] ba=ab:

babab ba

Critical pair: abbab=a.

Reduce LHS:

[4]ab(ba)b
[4]⇒ a(ba)bb
⇒ aabbb

Referenced by [6].

[6] abbb=aaa

Overlap of [1] aaaa=a with [5] aabbb=a:

aa aa aabbb

Critical pair: aaa=abbb.

Flip LHS and RHS.

Defines rule #3.