Certificate for #5200 ⟨a, b | aababba=baab⟩

Back:⟨a, b | aababba=baab⟩

Completion settings:

[1] aababba=baab

Axiom: aababba=baab.

Referenced by [3].

[2] aaba=c

Axiom: aaba=c.

Defines rule #4.

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

[3] cbba=baab

Overlap of [1] aababba=baab with [2] aaba=c:

aababba aaba

Critical pair: cbba=baab.

Defines rule #1.

Referenced by [5].

[4] caba=aabc

Overlap of [2] aaba=c with [2] aaba=c:

aab a aaba

Critical pair: aabc=caba.

Flip LHS and RHS.

Defines rule #3.

[5] bcba=cbbc

Overlap of [3] cbba=baab with [2] aaba=c:

cbb a aaba

Critical pair: cbbc=baababa.

Reduce RHS:

[2]b(aaba)ba
⇒ bcba

Flip LHS and RHS.

Defines rule #2.