Certificate for #1037 ⟨a, b | aaabaa=baa⟩

Back:⟨a, b | aaabaa=baa⟩

Completion settings:

[1] aaabaa=baa

Axiom: aaabaa=baa.

Referenced by [3].

[2] baa=c

Axiom: baa=c.

Defines rule #3.

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

[3] aaabaa=c

Simplify [1] aaabaa=baa.

Reduce RHS:

[2](baa)
⇒ c

Referenced by [4].

[4] aaac=c

Overlap of [3] aaabaa=c with [2] baa=c:

aaa baa baa

Critical pair: aaac=c.

Defines rule #1.

Referenced by [5], [6].

[5] bc=cac

Overlap of [2] baa=c with [4] aaac=c:

b aa aaac

Critical pair: bc=cac.

Defines rule #2.

[6] bac=caac

Overlap of [2] baa=c with [4] aaac=c:

ba a aaac

Critical pair: bac=caac.

Defines rule #4.