Certificate for #5740 ⟨a, b | aabbaa=baabb⟩

Completion settings:

• Auxiliary generators:
  1. c = baa
• Reduction order:
  • Right-to-left shortlex with a < c < b

Axiom: aabbaa=baabb.

Referenced by [3].

Axiom: baa=c.

Defines rule #1.

Referenced by [3], [4], [5], [6], [8], [12].

Simplify [1] aabbaa=baabb.

Reduce RHS:

Referenced by [4].

Overlap of [3] aabbaa=cbb with [2] baa=c:

Critical pair: aabc=cbb.

Defines rule #2.

Referenced by [5], [6], [7], [10], [11], [15], [28], [29], [30], [31], [32], [33], [34], [35].

Overlap of [2] baa=c with [4] aabc=cbb:

Critical pair: bcbb=cbc.

Defines rule #3.

Referenced by [7], [8], [9], [13], [16], [20].

Overlap of [2] baa=c with [4] aabc=cbb:

Critical pair: bacbb=cabc.

Defines rule #5.

Referenced by [12], [13], [14].

Overlap of [4] aabc=cbb with [5] bcbb=cbc:

Critical pair: aacbc=cbbbb.

Flip LHS and RHS.

Defines rule #6.

Overlap of [5] bcbb=cbc with [2] baa=c:

Critical pair: bcbc=cbcaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [17], [21].

Overlap of [5] bcbb=cbc with [5] bcbb=cbc:

Critical pair: bcbcbc=cbccbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [18], [22].

Overlap of [4] aabc=cbb with [8] cbcaa=bcbc:

Critical pair: aabbcbc=cbbbcaa.

Defines rule #9.

Referenced by [16], [17], [18], [19], [24], [26].

Overlap of [8] cbcaa=bcbc with [4] aabc=cbb:

Critical pair: cbcacbb=bcbcabc.

Defines rule #10.

Referenced by [19], [23].

Overlap of [6] bacbb=cabc with [2] baa=c:

Critical pair: bacbc=cabcaa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [15].

Overlap of [6] bacbb=cabc with [5] bcbb=cbc:

Critical pair: bacbcbc=cabccbb.

Flip LHS and RHS.

Defines rule #11.

Overlap of [6] bacbb=cabc with [6] bacbb=cabc:

Critical pair: bacbcabc=cabcacbb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [4] aabc=cbb with [12] cabcaa=bacbc:

Critical pair: aabbacbc=cbbabcaa.

Defines rule #12.

Referenced by [20], [21], [22], [23], [25], [27].

Overlap of [10] aabbcbc=cbbbcaa with [5] bcbb=cbc:

Critical pair: aabbccbc=cbbbcaabb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [24], [25].

Overlap of [10] aabbcbc=cbbbcaa with [8] cbcaa=bcbc:

Critical pair: aabbbcbc=cbbbcaaaa.

Flip LHS and RHS.

Defines rule #14.

Overlap of [10] aabbcbc=cbbbcaa with [9] cbccbb=bcbcbc:

Critical pair: aabbbcbcbc=cbbbcaacbb.

Flip LHS and RHS.

Defines rule #18.

Overlap of [10] aabbcbc=cbbbcaa with [11] cbcacbb=bcbcabc:

Critical pair: aabbbcbcabc=cbbbcaaacbb.

Flip LHS and RHS.

Defines rule #19.

Overlap of [15] aabbacbc=cbbabcaa with [5] bcbb=cbc:

Critical pair: aabbaccbc=cbbabcaabb.

Flip LHS and RHS.

Defines rule #17.

Referenced by [26], [27].

Overlap of [15] aabbacbc=cbbabcaa with [8] cbcaa=bcbc:

Critical pair: aabbabcbc=cbbabcaaaa.

Flip LHS and RHS.

Defines rule #16.

Overlap of [15] aabbacbc=cbbabcaa with [9] cbccbb=bcbcbc:

Critical pair: aabbabcbcbc=cbbabcaacbb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [15] aabbacbc=cbbabcaa with [11] cbcacbb=bcbcabc:

Critical pair: aabbabcbcabc=cbbabcaaacbb.

Flip LHS and RHS.

Defines rule #22.

Overlap of [16] cbbbcaabb=aabbccbc with [10] aabbcbc=cbbbcaa:

Critical pair: cbbbccbbbcaa=aabbccbccbc.

Defines rule #21.

Referenced by [28], [29].

Overlap of [16] cbbbcaabb=aabbccbc with [15] aabbacbc=cbbabcaa:

Critical pair: cbbbccbbabcaa=aabbccbcacbc.

Defines rule #23.

Referenced by [30], [31].

Overlap of [20] cbbabcaabb=aabbaccbc with [10] aabbcbc=cbbbcaa:

Critical pair: cbbabccbbbcaa=aabbaccbccbc.

Defines rule #24.

Referenced by [32], [33].

Overlap of [20] cbbabcaabb=aabbaccbc with [15] aabbacbc=cbbabcaa:

Critical pair: cbbabccbbabcaa=aabbaccbcacbc.

Defines rule #26.

Referenced by [34], [35].

Overlap of [24] cbbbccbbbcaa=aabbccbccbc with [4] aabc=cbb:

Critical pair: cbbbccbbbccbb=aabbccbccbcbc.

Defines rule #25.

Overlap of [24] cbbbccbbbcaa=aabbccbccbc with [4] aabc=cbb:

Critical pair: cbbbccbbbcacbb=aabbccbccbcabc.

Defines rule #27.

Overlap of [25] cbbbccbbabcaa=aabbccbcacbc with [4] aabc=cbb:

Critical pair: cbbbccbbabccbb=aabbccbcacbcbc.

Defines rule #28.

Overlap of [25] cbbbccbbabcaa=aabbccbcacbc with [4] aabc=cbb:

Critical pair: cbbbccbbabcacbb=aabbccbcacbcabc.

Defines rule #30.

Overlap of [26] cbbabccbbbcaa=aabbaccbccbc with [4] aabc=cbb:

Critical pair: cbbabccbbbccbb=aabbaccbccbcbc.

Defines rule #29.

Overlap of [26] cbbabccbbbcaa=aabbaccbccbc with [4] aabc=cbb:

Critical pair: cbbabccbbbcacbb=aabbaccbccbcabc.

Defines rule #31.

Overlap of [27] cbbabccbbabcaa=aabbaccbcacbc with [4] aabc=cbb:

Critical pair: cbbabccbbabccbb=aabbaccbcacbcbc.

Defines rule #32.

Overlap of [27] cbbabccbbabcaa=aabbaccbcacbc with [4] aabc=cbb:

Critical pair: cbbabccbbabcacbb=aabbaccbcacbcabc.

Defines rule #33.