Certificate for #2125 ⟨a, b | aaaabaa=baa⟩

Back:⟨a, b | aaaabaa=baa⟩

Completion settings:

[1] aaaabaa=baa

Axiom: aaaabaa=baa.

Referenced by [3].

[2] baa=c

Axiom: baa=c.

Defines rule #3.

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

[3] aaaabaa=c

Simplify [1] aaaabaa=baa.

Reduce RHS:

[2](baa)
⇒ c

Referenced by [4].

[4] aaaac=c

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

aaaa baa baa

Critical pair: aaaac=c.

Defines rule #1.

Referenced by [5], [6].

[5] bc=caac

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

b aa aaaac

Critical pair: bc=caac.

Defines rule #2.

[6] bac=caaac

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

ba a aaaac

Critical pair: bac=caaac.

Defines rule #4.