Certificate for #4666 ⟨a, b | aaab=a, baba=b⟩

Back:⟨a, b | aaab=a, baba=b⟩

Completion settings:

[1] aaab=a

Axiom: aaab=a.

Defines rule #3.

Referenced by [3], [4].

[2] baba=b

Axiom: baba=b.

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

[3] aaba=a

Overlap of [1] aaab=a with [2] baba=b:

aaa b baba

Critical pair: aaab=aaba.

Reduce LHS:

[1](aaab)
⇒ a

Flip LHS and RHS.

Referenced by [6].

[4] baab=b

Overlap of [2] baba=b with [1] aaab=a:

bab a aaab

Critical pair: baba=baab.

Reduce LHS:

[2](baba)
⇒ b

Flip LHS and RHS.

Defines rule #4.

[5] bba=bab

Overlap of [2] baba=b with [2] baba=b:

ba ba baba

Critical pair: bab=bba.

Flip LHS and RHS.

Defines rule #2.

[6] aba=aab

Overlap of [3] aaba=a with [2] baba=b:

aa ba baba

Critical pair: aab=aba.

Flip LHS and RHS.

Defines rule #1.