Certificate for #2287 ⟨a, b | aabbbba=baa⟩

Completion settings:

• Auxiliary generators:
  1. c = bbbba
  2. d = cccc
  3. e = da
• Reduction order:
  • Right-to-left recursive path with deg(a) = 0; deg(e) = 1; deg(d) = deg(c) = deg(b) = 2, d < c < b

Axiom: aabbbba=baa.

Referenced by [5].

Axiom: bbbba=c.

Defines rule #35.

Referenced by [5], [7].

Axiom: cccc=d.

Defines rule #34.

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

Axiom: da=e.

Defines rule #3.

Referenced by [8], [9], [10], [13], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38].

Overlap of [1] aabbbba=baa with [2] bbbba=c:

Critical pair: aac=baa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [11], [12], [15], [16], [17], [18], [20], [21], [23], [24], [26], [27], [32], [33].

Overlap of [3] cccc=d with [3] cccc=d:

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #15.

Referenced by [9], [14], [17], [18], [19], [20], [21], [22], [23], [24].

Overlap of [2] bbbba=c with [5] baa=aac:

Critical pair: bbbaac=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [8], [9], [12], [16], [18], [21], [24], [27], [28], [32], [33], [34].

Overlap of [3] cccc=d with [7] ca=aad:

Critical pair: cccaad=da.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

Overlap of [6] dc=cd with [7] ca=aad:

Critical pair: daad=cda.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [11], [15], [17], [20], [23], [26].

Overlap of [3] cccc=d with [9] ce=ead:

Critical pair: cccead=de.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12], [15], [16], [17], [18], [20], [21], [23], [24], [27], [29], [30], [35], [36], [38].

Overlap of [5] baa=aac with [8] aaeeed=e:

Critical pair: be=aaceeed.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [25], [26], [27], [28], [29], [30].

Overlap of [5] baa=aac with [8] aaeeed=e:

Critical pair: bae=aacaeeed.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [31], [32], [33], [34], [35], [36], [37], [38].

Overlap of [8] aaeeed=e with [4] da=e:

Critical pair: aaeeee=ea.

Defines rule #1.

Referenced by [15], [16].

Overlap of [8] aaeeed=e with [6] dc=cd:

Critical pair: aaeeecd=ec.

Defines rule #14.

Referenced by [17], [18], [19].

Overlap of [5] baa=aac with [13] aaeeee=ea:

Critical pair: bea=aaceeee.

Reduce RHS:

Defines rule #8.

Referenced by [37].

Overlap of [5] baa=aac with [13] aaeeee=ea:

Critical pair: baea=aacaeeee.

Reduce RHS:

Defines rule #9.

Overlap of [5] baa=aac with [14] aaeeecd=ec:

Critical pair: bec=aaceeecd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [5] baa=aac with [14] aaeeecd=ec:

Critical pair: baec=aacaeeecd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [14] aaeeecd=ec with [6] dc=cd:

Critical pair: aaeeeccd=ecc.

Defines rule #30.

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

Overlap of [5] baa=aac with [19] aaeeeccd=ecc:

Critical pair: becc=aaceeeccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [5] baa=aac with [19] aaeeeccd=ecc:

Critical pair: baecc=aacaeeeccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [19] aaeeeccd=ecc with [6] dc=cd:

Critical pair: aaeeecccd=eccc.

Defines rule #33.

Referenced by [23], [24].

Overlap of [5] baa=aac with [22] aaeeecccd=eccc:

Critical pair: beccc=aaceeecccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #36.

Overlap of [5] baa=aac with [22] aaeeecccd=eccc:

Critical pair: baeccc=aacaeeecccd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #37.

Overlap of [4] da=e with [11] aaeaeaeeeeaeeedd=be:

Critical pair: dbe=eaeaeaeeeeaeeedd.

Defines rule #16.

Referenced by [30], [36].

Overlap of [5] baa=aac with [11] aaeaeaeeeeaeeedd=be:

Critical pair: bbe=aaceaeaeeeeaeeedd.

Reduce RHS:

Defines rule #20.

Overlap of [5] baa=aac with [11] aaeaeaeeeeaeeedd=be:

Critical pair: babe=aacaeaeaeeeeaeeedd.

Reduce RHS:

Defines rule #21.

Overlap of [7] ca=aad with [11] aaeaeaeeeeaeeedd=be:

Critical pair: cbe=aadaeaeaeeeeaeeedd.

Reduce RHS:

Defines rule #18.

Overlap of [11] aaeaeaeeeeaeeedd=be with [10] de=eaeeed:

Critical pair: aaeaeaeeeeaeeedeaeeed=bee.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [11] aaeaeaeeeeaeeedd=be with [25] dbe=eaeaeaeeeeaeeedd:

Critical pair: aaeaeaeeeeaeeedeaeaeaeeeeaeeedd=bebe.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [4] da=e with [12] aaaaeaeeeeaeeeeaeeedd=bae:

Critical pair: dbae=eaaaeaeeeeaeeeeaeeedd.

Defines rule #17.

Referenced by [38].

Overlap of [5] baa=aac with [12] aaaaeaeeeeaeeeeaeeedd=bae:

Critical pair: bbae=aacaaeaeeeeaeeeeaeeedd.

Reduce RHS:

Defines rule #24.

Overlap of [5] baa=aac with [12] aaaaeaeeeeaeeeeaeeedd=bae:

Critical pair: babae=aacaaaeaeeeeaeeeeaeeedd.

Reduce RHS:

Defines rule #25.

Overlap of [7] ca=aad with [12] aaaaeaeeeeaeeeeaeeedd=bae:

Critical pair: cbae=aadaaaeaeeeeaeeeeaeeedd.

Reduce RHS:

Defines rule #19.

Overlap of [12] aaaaeaeeeeaeeeeaeeedd=bae with [10] de=eaeeed:

Critical pair: aaaaeaeeeeaeeeeaeeedeaeeed=baee.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [12] aaaaeaeeeeaeeeeaeeedd=bae with [25] dbe=eaeaeaeeeeaeeedd:

Critical pair: aaaaeaeeeeaeeeeaeeedeaeaeaeeeeaeeedd=baebe.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [15] bea=aaeaeaeeeeaeeeeaeeed with [12] aaaaeaeeeeaeeeeaeeedd=bae:

Critical pair: bebae=aaeaeaeeeeaeeeeaeeedaaaeaeeeeaeeeeaeeedd.

Reduce RHS:

Defines rule #26.

Overlap of [12] aaaaeaeeeeaeeeeaeeedd=bae with [31] dbae=eaaaeaeeeeaeeeeaeeedd:

Critical pair: aaaaeaeeeeaeeeeaeeedeaaaeaeeeeaeeeeaeeedd=baebae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.