Certificate for #1763 ⟨a, b | abaabaaab=a⟩

Completion settings:

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

Axiom: abaabaaab=a.

Referenced by [5].

Axiom: abaab=c.

Referenced by [5], [8], [9], [10], [21].

Axiom: aaa=d.

Referenced by [5], [6], [7], [10], [15].

Axiom: cca=e.

Defines rule #3.

Referenced by [7], [9], [11], [12], [16], [25], [27], [28], [30], [38], [40], [46].

Overlap of [1] abaabaaab=a with [2] abaab=c:

Critical pair: caaab=a.

Reduce LHS:

Referenced by [10], [33].

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

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #10.

Referenced by [25], [27], [38], [40], [46].

Overlap of [4] cca=e with [3] aaa=d:

Critical pair: ccd=eaa.

Flip LHS and RHS.

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

Overlap of [2] abaab=c with [2] abaab=c:

Critical pair: abac=caab.

Flip LHS and RHS.

Referenced by [23].

Overlap of [4] cca=e with [2] abaab=c:

Critical pair: ccc=ebaab.

Flip LHS and RHS.

Referenced by [24].

Overlap of [7] eaa=ccd with [2] abaab=c:

Critical pair: eac=ccdbaab.

Reduce RHS:

Defines rule #4.

Referenced by [11], [13], [20], [26], [35], [37], [47].

Overlap of [10] eac=a with [4] cca=e:

Critical pair: eae=aca.

Flip LHS and RHS.

Defines rule #12.

Referenced by [12], [13], [14], [17], [18], [29], [31], [32], [34], [49], [50].

Overlap of [4] cca=e with [11] aca=eae:

Critical pair: cceae=eca.

Defines rule #5.

Referenced by [26], [27], [42].

Overlap of [10] eac=a with [11] aca=eae:

Critical pair: eeae=aa.

Flip LHS and RHS.

Defines rule #11.

Referenced by [15], [16], [17], [18], [19], [21], [22], [23], [24], [26], [27], [33], [35], [36], [37], [38].

Overlap of [11] aca=eae with [11] aca=eae:

Critical pair: aceae=eaeca.

Defines rule #15.

Overlap of [3] aaa=d with [13] aa=eeae:

Critical pair: eeaea=d.

Defines rule #13.

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

Overlap of [4] cca=e with [13] aa=eeae:

Critical pair: cceeae=ea.

Defines rule #6.

Referenced by [28], [29], [39], [41], [43], [47], [48].

Overlap of [11] aca=eae with [13] aa=eeae:

Critical pair: aceeae=eaea.

Defines rule #17.

Overlap of [13] aa=eeae with [11] aca=eae:

Critical pair: aeae=eeaeca.

Defines rule #14.

Referenced by [27], [36], [38], [47].

Overlap of [13] aa=eeae with [13] aa=eeae:

Critical pair: aeeae=eeaea.

Reduce RHS:

Defines rule #16.

Overlap of [15] eeaea=d with [10] eac=a:

Critical pair: eeaa=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [25], [27], [38], [40].

Overlap of [2] abaab=c with [13] aa=eeae:

Critical pair: abeeaeb=c.

Defines rule #37.

Overlap of [7] eaa=ccd with [13] aa=eeae:

Critical pair: eeeae=ccd.

Defines rule #7.

Referenced by [26], [27], [33], [37], [38], [47].

Overlap of [8] caab=abac with [13] aa=eeae:

Critical pair: ceeaeb=abac.

Flip LHS and RHS.

Defines rule #21.

Referenced by [28], [29], [30], [31], [32], [34], [49], [50].

Overlap of [9] ebaab=ccc with [13] aa=eeae:

Critical pair: ebeeaeb=ccc.

Defines rule #33.

Overlap of [20] dc=eccd with [4] cca=e:

Critical pair: de=eccdca.

Reduce RHS:

Defines rule #2.

Overlap of [12] cceae=eca with [10] eac=a:

Critical pair: cceaa=ecaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [12] cceae=eca with [18] aeae=eeaeca:

Critical pair: cceeeaeca=ecaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [4] cca=e with [23] abac=ceeaeb:

Critical pair: ccceeaeb=ebac.

Reduce LHS:

Defines rule #19.

Referenced by [32], [44].

Overlap of [11] aca=eae with [23] abac=ceeaeb:

Critical pair: acceeaeb=eaebac.

Reduce LHS:

Defines rule #31.

Referenced by [33], [34].

Overlap of [23] abac=ceeaeb with [4] cca=e:

Critical pair: abae=ceeaebca.

Defines rule #22.

Referenced by [35], [36].

Overlap of [23] abac=ceeaeb with [11] aca=eae:

Critical pair: abeae=ceeaeba.

Defines rule #23.

Referenced by [37], [38].

Overlap of [28] ceab=ebac with [23] abac=ceeaeb:

Critical pair: ceceeaeb=ebacac.

Reduce RHS:

Defines rule #20.

Referenced by [45].

Overlap of [15] eeaea=d with [29] aeab=eaebac:

Critical pair: eeeaebac=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [47].

Overlap of [29] aeab=eaebac with [23] abac=ceeaeb:

Critical pair: aeceeaeb=eaebacac.

Reduce RHS:

Defines rule #32.

Referenced by [47].

Overlap of [30] abae=ceeaebca with [10] eac=a:

Critical pair: abaa=ceeaebcaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [41], [42], [43], [44], [45].

Overlap of [30] abae=ceeaebca with [18] aeae=eeaeca:

Critical pair: abeeaeca=ceeaebcaae.

Reduce RHS:

Defines rule #34.

Referenced by [46].

Overlap of [31] abeae=ceeaeba with [10] eac=a:

Critical pair: abeaa=ceeaebaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [39].

Overlap of [31] abeae=ceeaeba with [18] aeae=eeaeca:

Critical pair: abeeeaeca=ceeaebaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [16] cceeae=ea with [37] ceeaebeeaec=abccd:

Critical pair: cabccd=eabeeaec.

Flip LHS and RHS.

Defines rule #24.

Referenced by [40], [46].

Overlap of [39] eabeeaec=cabccd with [4] cca=e:

Critical pair: eabeeaee=cabccdca.

Reduce RHS:

Defines rule #28.

Overlap of [16] cceeae=ea with [35] ceeaebceeaec=abeeae:

Critical pair: cabeeae=eabceeaec.

Flip LHS and RHS.

Defines rule #26.

Overlap of [35] ceeaebceeaec=abeeae with [12] cceae=eca:

Critical pair: ceeaebceeaeeca=abeeaeceae.

Flip LHS and RHS.

Defines rule #35.

Overlap of [35] ceeaebceeaec=abeeae with [16] cceeae=ea:

Critical pair: ceeaebceeaeea=abeeaeceeae.

Flip LHS and RHS.

Defines rule #36.

Referenced by [47].

Overlap of [35] ceeaebceeaec=abeeae with [28] ceab=ebac:

Critical pair: ceeaebceeaeebac=abeeaeeab.

Flip LHS and RHS.

Defines rule #38.

Overlap of [35] ceeaebceeaec=abeeae with [32] ceceeaeb=ebeaec:

Critical pair: ceeaebceeaeebeaec=abeeaeeceeaeb.

Flip LHS and RHS.

Defines rule #41.

Overlap of [39] eabeeaec=cabccd with [36] abeeaeca=ceeaebceeaee:

Critical pair: eceeaebceeaee=cabccda.

Reduce RHS:

Defines rule #30.

Overlap of [43] abeeaeceeae=ceeaebceeaeea with [34] aeceeaeb=eaebeaec:

Critical pair: abeeeaebeaec=ceeaebceeaeeab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #40.

Referenced by [48], [49].

Overlap of [16] cceeae=ea with [47] ceeaebceeaeeab=abceeaecac:

Critical pair: cabceeaecac=eabceeaeeab.

Flip LHS and RHS.

Defines rule #39.

Referenced by [50].

Overlap of [47] ceeaebceeaeeab=abceeaecac with [23] abac=ceeaeb:

Critical pair: ceeaebceeaeeceeaeb=abceeaecacac.

Reduce RHS:

Defines rule #43.

Overlap of [48] eabceeaeeab=cabceeaecac with [23] abac=ceeaeb:

Critical pair: eabceeaeeceeaeb=cabceeaecacac.

Reduce RHS:

Defines rule #42.