Certificate for #2986 ⟨a, b, c | aab=c, bca=b⟩

Back:⟨a, b, c | aab=c, bca=b⟩

Completion settings:

[1] c=aab

Axiom: aab=c.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

[2] baaba=b

Axiom: bca=b.

Reduce LHS:

[1]b(c)a
⇒ baaba

Defines rule #3.

Referenced by [3], [4].

[3] baba=baab

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

baa ba baaba

Critical pair: baab=baba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] bba=bab

Overlap of [2] baaba=b with [3] baba=baab:

baa ba baba

Critical pair: baabaab=bba.

Reduce LHS:

[2](baaba)ab
⇒ bab

Flip LHS and RHS.

Defines rule #1.