Certificate for #12363 ⟨a, b | aaba=ab, baaa=b⟩

Back:⟨a, b | aaba=ab, baaa=b⟩

Completion settings:

[1] aaba=ab

Axiom: aaba=ab.

Referenced by [3], [4].

[2] baaa=b

Axiom: baaa=b.

Defines rule #1.

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

[3] aab=abaa

Overlap of [1] aaba=ab with [2] baaa=b:

aa ba baaa

Critical pair: aab=abaa.

Defines rule #2.

[4] baba=bb

Overlap of [2] baaa=b with [1] aaba=ab:

baa a aaba

Critical pair: baaab=baba.

Reduce LHS:

[2](baaa)b
⇒ bb

Flip LHS and RHS.

Referenced by [5].

[5] bab=bbaa

Overlap of [4] baba=bb with [2] baaa=b:

ba ba baaa

Critical pair: bab=bbaa.

Defines rule #3.