Certificate for #19292 ⟨a, b | aaa=a, babab=ab⟩

Back:⟨a, b | aaa=a, babab=ab⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [4].

[2] babab=ab

Axiom: babab=ab.

Defines rule #5.

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

[3] baab=abab

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

ba bab babab

Critical pair: baab=abab.

Defines rule #2.

Referenced by [4], [5].

[4] aabab=bab

Overlap of [3] baab=abab with [2] babab=ab:

baa b babab

Critical pair: baaab=abababab.

Reduce LHS:

[1]b(aaa)b
⇒ bab

Reduce RHS:

[2]a(babab)ab
⇒ aabab

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] bbab=aab

Overlap of [3] baab=abab with [4] aabab=bab:

b aab aabab

Critical pair: bbab=ababab.

Reduce RHS:

[2]a(babab)
⇒ aab

Defines rule #3.