Certificate for #5868 ⟨a, b | ababab=abaaa⟩

Completion settings:

• Auxiliary generators:
  1. c = abaaa
• Reduction order:
  • Left-to-right recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1

Axiom: ababab=abaaa.

Referenced by [3].

Axiom: abaaa=c.

Defines rule #6.

Referenced by [3], [4], [6], [7], [9], [11], [12], [15].

Simplify [1] ababab=abaaa.

Reduce RHS:

Defines rule #16.

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

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

Critical pair: abaac=cbaaa.

Flip LHS and RHS.

Defines rule #9.

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

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [8], [9], [14], [17].

Overlap of [3] ababab=c with [2] abaaa=c:

Critical pair: ababc=caaa.

Defines rule #14.

Referenced by [8], [10], [12], [13], [14], [17].

Overlap of [2] abaaa=c with [3] ababab=c:

Critical pair: abaac=cbabab.

Flip LHS and RHS.

Defines rule #17.

Overlap of [5] cab=abc with [3] ababab=c:

Critical pair: cc=abcabab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [14], [16].

Overlap of [5] cab=abc with [2] abaaa=c:

Critical pair: cc=abcaaa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [10], [11], [13], [18].

Overlap of [3] ababab=c with [9] abcaaa=cc:

Critical pair: ababcc=ccaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18].

Overlap of [2] abaaa=c with [9] abcaaa=cc:

Critical pair: abaacc=cbcaaa.

Flip LHS and RHS.

Defines rule #10.

Overlap of [2] abaaa=c with [6] ababc=caaa:

Critical pair: abaacaaa=cbabc.

Flip LHS and RHS.

Defines rule #15.

Overlap of [6] ababc=caaa with [9] abcaaa=cc:

Critical pair: abcc=caaaaaa.

Defines rule #5.

Referenced by [14], [15], [16], [17], [18].

Overlap of [8] caaaab=cc with [6] ababc=caaa:

Critical pair: caaacaaa=ccabc.

Reduce RHS:

Defines rule #2.

Referenced by [16].

Overlap of [2] abaaa=c with [13] abcc=caaaaaa:

Critical pair: abaacaaaaaa=cbcc.

Flip LHS and RHS.

Defines rule #8.

Overlap of [8] caaaab=cc with [13] abcc=caaaaaa:

Critical pair: caaacaaaaaa=cccc.

Reduce LHS:

Defines rule #4.

Overlap of [13] abcc=caaaaaa with [5] cab=abc:

Critical pair: abcabc=caaaaaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [13] abcc=caaaaaa with [10] ccaaa=caaac:

Critical pair: abcaaac=caaaaaaaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.