Certificate for #5874 ⟨a, b | ababab=baaba⟩

Completion settings:

• Auxiliary generators:
  1. c = ab
  2. d = baacc
  3. e = baa
• Reduction order:
  • Left-to-right recursive path with deg(c) = deg(e) = deg(d) = 0, c < e < d; deg(a) = 1; deg(b) = 2

Axiom: ababab=baaba.

Referenced by [5].

Axiom: ab=c.

Defines rule #31.

Referenced by [6], [8], [9], [12], [13].

Axiom: baacc=d.

Referenced by [7].

Axiom: baa=e.

Defines rule #21.

Referenced by [5], [7], [8], [9], [14].

Simplify [1] ababab=baaba.

Reduce RHS:

Referenced by [6].

Overlap of [5] ababab=eba with [2] ab=c:

Critical pair: cabab=eba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [3] baacc=d with [4] baa=e:

Critical pair: ecc=d.

Defines rule #2.

Referenced by [10], [15], [16], [17], [19], [20], [23], [26], [28], [30], [32], [34].

Overlap of [2] ab=c with [4] baa=e:

Critical pair: ae=caa.

Flip LHS and RHS.

Defines rule #17.

Referenced by [10], [14], [21].

Overlap of [4] baa=e with [2] ab=c:

Critical pair: bac=eb.

Flip LHS and RHS.

Defines rule #23.

Referenced by [11], [15], [18].

Overlap of [7] ecc=d with [8] caa=ae:

Critical pair: ecae=daa.

Flip LHS and RHS.

Defines rule #19.

Simplify [6] eba=ccc.

Reduce LHS:

Defines rule #22.

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

Overlap of [2] ab=c with [11] baca=ccc:

Critical pair: accc=caca.

Flip LHS and RHS.

Defines rule #18.

Referenced by [28], [29].

Overlap of [11] baca=ccc with [2] ab=c:

Critical pair: bacc=cccb.

Flip LHS and RHS.

Defines rule #25.

Referenced by [30], [31].

Overlap of [11] baca=ccc with [8] caa=ae:

Critical pair: baae=ccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [15], [19], [20], [21], [23], [25], [29].

Overlap of [9] eb=bac with [11] baca=ccc:

Critical pair: eccc=bacaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [16], [17], [18], [20], [22], [24], [26], [34].

Overlap of [7] ecc=d with [15] cee=dc:

Critical pair: ecdc=dee.

Defines rule #3.

Referenced by [22], [23], [24], [27], [33], [35].

Overlap of [15] cee=dc with [7] ecc=d:

Critical pair: ced=dccc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [31].

Overlap of [15] cee=dc with [9] eb=bac:

Critical pair: cebac=dcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [7] ecc=d with [14] ccca=ee:

Critical pair: eee=dca.

Flip LHS and RHS.

Defines rule #8.

Overlap of [7] ecc=d with [14] ccca=ee:

Critical pair: ecee=dcca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [14] ccca=ee with [8] caa=ae:

Critical pair: ccae=eea.

Flip LHS and RHS.

Defines rule #7.

Referenced by [26].

Overlap of [15] cee=dc with [16] ecdc=dee:

Critical pair: cedee=dccdc.

Flip LHS and RHS.

Defines rule #5.

Overlap of [16] ecdc=dee with [14] ccca=ee:

Critical pair: ecdee=deecca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [16] ecdc=dee with [15] cee=dc:

Critical pair: ecddc=deeee.

Flip LHS and RHS.

Defines rule #6.

Overlap of [17] dccc=ced with [14] ccca=ee:

Critical pair: dee=ceda.

Flip LHS and RHS.

Defines rule #10.

Referenced by [27].

Overlap of [15] cee=dc with [21] eea=ccae:

Critical pair: ceccae=dcea.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [16] ecdc=dee with [25] ceda=dee:

Critical pair: ecddee=deeeda.

Flip LHS and RHS.

Defines rule #16.

Overlap of [7] ecc=d with [12] caca=accc:

Critical pair: ecaccc=daca.

Flip LHS and RHS.

Defines rule #20.

Overlap of [14] ccca=ee with [12] caca=accc:

Critical pair: ccaccc=eeca.

Flip LHS and RHS.

Defines rule #11.

Referenced by [34].

Overlap of [7] ecc=d with [13] cccb=bacc:

Critical pair: ecbacc=dccb.

Flip LHS and RHS.

Defines rule #27.

Referenced by [35].

Overlap of [17] dccc=ced with [13] cccb=bacc:

Critical pair: dbacc=cedb.

Flip LHS and RHS.

Defines rule #26.

Referenced by [32], [33].

Overlap of [7] ecc=d with [31] cedb=dbacc:

Critical pair: ecdbacc=dedb.

Flip LHS and RHS.

Defines rule #28.

Overlap of [16] ecdc=dee with [31] cedb=dbacc:

Critical pair: ecddbacc=deeedb.

Flip LHS and RHS.

Defines rule #30.

Overlap of [15] cee=dc with [29] eeca=ccaccc:

Critical pair: ceccaccc=dceca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [16] ecdc=dee with [30] dccb=ecbacc:

Critical pair: ececbacc=deecb.

Flip LHS and RHS.

Defines rule #29.