Certificate for #2629 ⟨a, b | abbbba=abab⟩

Back:⟨a, b | abbbba=abab⟩

Completion settings:

[1] abbbba=abab

Axiom: abbbba=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #5.

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

[3] abbbba=c

Simplify [1] abbbba=abab.

Reduce RHS:

[2](abab)
⇒ c

Defines rule #6.

Referenced by [5], [6], [7].

[4] cab=abc

Overlap of [2] abab=c with [2] abab=c:

ab ab abab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #1.

[5] cbbbba=abbbbc

Overlap of [3] abbbba=c with [3] abbbba=c:

abbbb a abbbba

Critical pair: abbbbc=cbbbba.

Flip LHS and RHS.

Defines rule #4.

[6] cbab=abbbbc

Overlap of [3] abbbba=c with [2] abab=c:

abbbb a abab

Critical pair: abbbbc=cbab.

Flip LHS and RHS.

Defines rule #2.

[7] cbbba=abc

Overlap of [2] abab=c with [3] abbbba=c:

ab ab abbbba

Critical pair: abc=cbbba.

Flip LHS and RHS.

Defines rule #3.