Certificate for #2750 ⟨a, b | baaba=abaab⟩

Back:⟨a, b | baaba=abaab⟩

Completion settings:

[1] baaba=abaab

Axiom: baaba=abaab.

Referenced by [3].

[2] baa=c

Axiom: baa=c.

Defines rule #4.

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

[3] baaba=acb

Simplify [1] baaba=abaab.

Reduce RHS:

[2]a(baa)b
⇒ acb

Referenced by [4].

[4] acb=cba

Overlap of [3] baaba=acb with [2] baa=c:

baaba baa

Critical pair: cba=acb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

[5] bcc=ccb

Overlap of [2] baa=c with [4] acb=cba:

ba a acb

Critical pair: bacba=ccb.

Reduce LHS:

[4]b(acb)a
[2]⇒ bc(baa)
⇒ bcc

Defines rule #3.

[6] acc=cca

Overlap of [4] acb=cba with [2] baa=c:

ac b baa

Critical pair: acc=cbaaa.

Reduce RHS:

[2]c(baa)a
⇒ cca

Defines rule #1.