Certificate for #2522 ⟨a, b | aabbaa=aaab⟩

Completion settings:

• Auxiliary generators:
  1. c = aaab
• Reduction order:
  • Left-to-right shortlex with b < c < a

Axiom: aabbaa=aaab.

Referenced by [3].

Axiom: aaab=c.

Defines rule #3.

Referenced by [3], [5], [6], [7], [9], [12], [13], [23], [24].

Simplify [1] aabbaa=aaab.

Reduce RHS:

Defines rule #16.

Referenced by [4], [5], [6], [7], [8], [11], [22].

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

Critical pair: aabbc=cbbaa.

Referenced by [5], [19].

Overlap of [3] aabbaa=c with [2] aaab=c:

Critical pair: aabbc=cab.

Reduce LHS:

Defines rule #4.

Referenced by [8], [11], [12], [13], [14], [16], [19], [29].

Overlap of [3] aabbaa=c with [2] aaab=c:

Critical pair: aabbac=caab.

Defines rule #15.

Referenced by [20], [29], [30].

Overlap of [2] aaab=c with [3] aabbaa=c:

Critical pair: ac=cbaa.

Flip LHS and RHS.

Defines rule #1.

Referenced by [8], [9], [10], [17], [18], [20].

Overlap of [7] cbaa=ac with [3] aabbaa=c:

Critical pair: cbc=acbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [14], [15], [26].

Overlap of [7] cbaa=ac with [2] aaab=c:

Critical pair: cbac=acaab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [16], [17], [27].

Overlap of [7] cbaa=ac with [8] acab=cbc:

Critical pair: cbacbc=accab.

Defines rule #9.

Overlap of [5] cbbaa=cab with [3] aabbaa=c:

Critical pair: cbbc=cabbbaa.

Flip LHS and RHS.

Defines rule #20.

Overlap of [5] cbbaa=cab with [2] aaab=c:

Critical pair: cbbc=cabab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [15], [21].

Overlap of [5] cbbaa=cab with [2] aaab=c:

Critical pair: cbbac=cabaab.

Flip LHS and RHS.

Defines rule #12.

Overlap of [5] cbbaa=cab with [8] acab=cbc:

Critical pair: cbbacbc=cabcab.

Defines rule #17.

Overlap of [8] acab=cbc with [12] cabab=cbbc:

Critical pair: acbbc=cbcab.

Defines rule #6.

Referenced by [18].

Overlap of [5] cbbaa=cab with [9] acaab=cbac:

Critical pair: cbbacbac=cabcaab.

Defines rule #23.

Overlap of [7] cbaa=ac with [9] acaab=cbac:

Critical pair: cbacbac=accaab.

Defines rule #18.

Overlap of [15] acbbc=cbcab with [7] cbaa=ac:

Critical pair: acbbac=cbcabbaa.

Flip LHS and RHS.

Referenced by [28].

Simplify [4] aabbc=cbbaa.

Reduce RHS:

Defines rule #8.

Referenced by [20], [21], [25].

Overlap of [19] aabbc=cab with [7] cbaa=ac:

Critical pair: aabbac=cabbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [22], [23], [24], [25], [26], [27], [28], [30].

Overlap of [19] aabbc=cab with [12] cabab=cbbc:

Critical pair: aabbcbbc=cababab.

Reduce LHS:

Reduce RHS:

Defines rule #10.

Overlap of [20] cabbaa=caab with [3] aabbaa=c:

Critical pair: cabbc=caabbbaa.

Flip LHS and RHS.

Defines rule #26.

Overlap of [20] cabbaa=caab with [2] aaab=c:

Critical pair: cabbc=caabab.

Flip LHS and RHS.

Defines rule #13.

Overlap of [20] cabbaa=caab with [2] aaab=c:

Critical pair: cabbac=caabaab.

Flip LHS and RHS.

Defines rule #22.

Overlap of [20] cabbaa=caab with [19] aabbc=cab:

Critical pair: cabbcab=caabbbc.

Flip LHS and RHS.

Defines rule #21.

Overlap of [20] cabbaa=caab with [8] acab=cbc:

Critical pair: cabbacbc=caabcab.

Defines rule #24.

Overlap of [20] cabbaa=caab with [9] acaab=cbac:

Critical pair: cabbacbac=caabcaab.

Defines rule #27.

Overlap of [18] cbcabbaa=acbbac with [20] cabbaa=caab:

Critical pair: cbcaab=acbbac.

Flip LHS and RHS.

Defines rule #14.

Overlap of [5] cbbaa=cab with [6] aabbac=caab:

Critical pair: cbbcaab=cabbbac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [20] cabbaa=caab with [6] aabbac=caab:

Critical pair: cabbcaab=caabbbac.

Flip LHS and RHS.

Defines rule #25.