Certificate for #3826 ⟨a, b | abbbaabbba=b⟩

Back:⟨a, b | abbbaabbba=b⟩

Completion settings:

[1] abbbaabbba=b

Axiom: abbbaabbba=b.

Referenced by [3].

[2] bbba=c

Axiom: bbba=c.

Referenced by [3], [4].

[3] b=acac

Overlap of [1] abbbaabbba=b with [2] bbba=c:

a bbbaabbba bbba

Critical pair: acabbba=b.

Reduce LHS:

[2]aca(bbba)
⇒ acac

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] acacacacacaca=c

Overlap of [2] bbba=c with [3] b=acac:

bbba b

Critical pair: acacbba=c.

Reduce LHS:

[3]acac(b)ba
[3]⇒ acacacac(b)a
⇒ acacacacacaca

Defines rule #2.

Referenced by [5].

[5] cca=acc

Overlap of [4] acacacacacaca=c with [4] acacacacacaca=c:

ac acacacacaca acacacacacaca

Critical pair: acc=cca.

Flip LHS and RHS.

Defines rule #1.