Certificate for #3020 ⟨a, b | aabaaababaa=1⟩

Completion settings:

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

Axiom: aabaaababaa=1.

Referenced by [3].

Axiom: aba=c.

Referenced by [3], [4], [5], [12], [21], [23].

Overlap of [1] aabaaababaa=1 with [2] aba=c:

Critical pair: acaababaa=1.

Reduce LHS:

Referenced by [4], [5], [6], [8], [9], [10], [11], [13].

Overlap of [2] aba=c with [3] acacbaa=1:

Critical pair: ab=ccacbaa.

Flip LHS and RHS.

Referenced by [7].

Overlap of [3] acacbaa=1 with [2] aba=c:

Critical pair: acacbac=ba.

Referenced by [8], [10], [12], [15].

Overlap of [3] acacbaa=1 with [3] acacbaa=1:

Critical pair: acacba=cacbaa.

Flip LHS and RHS.

Referenced by [7].

Simplify [4] ccacbaa=ab.

Reduce LHS:

Referenced by [8], [14].

Overlap of [5] acacbac=ba with [7] cacacba=ab:

Critical pair: acacbaab=baacacba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [3] acacbaa=1 with [8] baacacba=b:

Critical pair: acacb=cacba.

Flip LHS and RHS.

Referenced by [10], [12], [13], [14], [15], [16].

Overlap of [5] acacbac=ba with [9] cacba=acacb:

Critical pair: acacbaacacb=baacba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11], [12].

Overlap of [3] acacbaa=1 with [10] baacba=cacb:

Critical pair: acaccacb=cba.

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [9] cacba=acacb with [10] baacba=cacb:

Critical pair: caccacb=acacbacba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [15], [18], [22], [23], [25].

Overlap of [3] acacbaa=1 with [9] cacba=acacb:

Critical pair: aacacba=1.

Reduce LHS:

Referenced by [18], [25], [26], [27].

Overlap of [7] cacacba=ab with [9] cacba=acacb:

Critical pair: caacacb=ab.

Referenced by [20], [23], [24].

Overlap of [5] acacbac=ba with [9] cacba=acacb:

Critical pair: aacacbc=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [17], [19], [20], [23], [24], [26].

Overlap of [9] cacba=acacb with [11] cba=acaccacb:

Critical pair: caacaccacb=acacb.

Referenced by [19], [20], [22], [23].

Overlap of [11] cba=acaccacb with [15] ba=aacaccaccacb:

Critical pair: caacaccaccacb=acaccacb.

Referenced by [19], [20], [23].

Overlap of [13] aaacacb=1 with [12] bc=caccacb:

Critical pair: aaacaccaccacb=c.

Referenced by [19].

Overlap of [18] aaacaccaccacb=c with [15] ba=aacaccaccacb:

Critical pair: aaacaccaccacaacaccaccacb=ca.

Reduce LHS:

Referenced by [20].

Overlap of [19] aaacaccacacacb=ca with [15] ba=aacaccaccacb:

Critical pair: aaacaccacacacaacaccaccacb=caa.

Reduce LHS:

Referenced by [21], [22].

Overlap of [20] aaacaccaab=caa with [2] aba=c:

Critical pair: aaacaccac=caaa.

Referenced by [23], [26].

Overlap of [20] aaacaccaab=caa with [12] bc=caccacb:

Critical pair: aaacaccaacaccacb=caac.

Reduce LHS:

Referenced by [24].

Overlap of [2] aba=c with [21] aaacaccac=caaa:

Critical pair: abcaaa=caacaccac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [22] aaacacacacb=caac with [15] ba=aacaccaccacb:

Critical pair: aaacacacacaacaccaccacb=caaca.

Reduce LHS:

Defines rule #3.

Referenced by [25], [26].

Overlap of [24] aaacaab=caaca with [12] bc=caccacb:

Critical pair: aaacaacaccacb=caacac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [24] aaacaab=caaca with [15] ba=aacaccaccacb:

Critical pair: aaacaaaacaccaccacb=caacaa.

Reduce LHS:

Defines rule #1.

Referenced by [27].

Overlap of [13] aaacacb=1 with [26] aaacac=caacaa:

Critical pair: caacaab=1.

Defines rule #4.