Certificate for #3048 ⟨a, b | aabaabbbaba=1⟩

Completion settings:

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

Axiom: aabaabbbaba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #2.

Referenced by [4], [5], [21], [34], [35], [39], [41].

Axiom: abaaabaa=d.

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

Overlap of [1] aabaabbbaba=1 with [2] bbb=c:

Critical pair: aabaacaba=1.

Referenced by [7], [8], [9], [11], [13].

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [20], [27], [31].

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

Critical pair: abaad=dabaa.

Defines rule #9.

Referenced by [22], [26].

Overlap of [3] abaaabaa=d with [4] aabaacaba=1:

Critical pair: aba=dcaba.

Flip LHS and RHS.

Referenced by [10], [11], [16].

Overlap of [3] abaaabaa=d with [4] aabaacaba=1:

Critical pair: abaaab=dbaacaba.

Referenced by [10], [12], [18], [19], [22], [23], [33].

Overlap of [4] aabaacaba=1 with [4] aabaacaba=1:

Critical pair: aabaacab=abaacaba.

Referenced by [11], [13].

Overlap of [7] dcaba=aba with [3] abaaabaa=d:

Critical pair: dcd=abaaabaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [14].

Overlap of [7] dcaba=aba with [4] aabaacaba=1:

Critical pair: dcab=abaabaacaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [3] abaaabaa=d with [8] abaaab=dbaacaba:

Critical pair: dbaacabaaa=d.

Reduce LHS:

Referenced by [14].

Overlap of [4] aabaacaba=1 with [9] aabaacab=abaacaba:

Critical pair: abaacabaa=1.

Referenced by [15], [16], [17], [18], [19], [23].

Simplify [10] dbaacabaaa=dcd.

Reduce RHS:

Referenced by [22].

Overlap of [11] ababaacabaa=dcab with [13] abaacabaa=1:

Critical pair: ab=dcab.

Flip LHS and RHS.

Referenced by [19].

Overlap of [7] dcaba=aba with [13] abaacabaa=1:

Critical pair: dc=abaacabaa.

Reduce RHS:

Defines rule #4.

Referenced by [19], [20], [24], [28].

Overlap of [13] abaacabaa=1 with [13] abaacabaa=1:

Critical pair: abaac=cabaa.

Defines rule #6.

Referenced by [18], [19], [23], [27], [29].

Overlap of [13] abaacabaa=1 with [13] abaacabaa=1:

Critical pair: abaacaba=baacabaa.

Reduce LHS:

Referenced by [19], [23].

Overlap of [15] dcab=ab with [13] abaacabaa=1:

Critical pair: dc=abaacabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [16] dc=1 with [5] cb=bc:

Critical pair: dbc=b.

Referenced by [25].

Overlap of [2] bbb=c with [19] baacabaaa=1:

Critical pair: bb=caacabaaa.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [19] baacabaaa=1 with [6] abaad=dabaa:

Critical pair: baacabaadabaa=baad.

Reduce LHS:

Referenced by [23].

Overlap of [13] abaacabaa=1 with [22] baacdd=baad:

Critical pair: abaacabaad=cdd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [23] cdd=d with [16] dc=1:

Critical pair: cd=dc.

Reduce RHS:

Defines rule #3.

Referenced by [25], [35], [39], [41].

Overlap of [20] dbc=b with [24] cd=1:

Critical pair: db=bd.

Defines rule #5.

Referenced by [26], [28], [32], [33].

Overlap of [6] abaad=dabaa with [25] db=bd:

Critical pair: abaabd=dabaab.

Defines rule #10.

Referenced by [32].

Overlap of [17] abaac=cabaa with [5] cb=bc:

Critical pair: abaabc=cabaab.

Defines rule #7.

Referenced by [31].

Overlap of [16] dc=1 with [21] caacabaaa=bb:

Critical pair: dbb=aacabaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [29], [30].

Overlap of [17] abaac=cabaa with [21] caacabaaa=bb:

Critical pair: abaabb=cabaaaacabaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [28] aacabaaa=bbd with [28] aacabaaa=bbd:

Critical pair: aacabaabbd=bbdacabaaa.

Reduce LHS:

Defines rule #14.

Referenced by [36], [37].

Overlap of [27] abaabc=cabaab with [5] cb=bc:

Critical pair: abaabbc=cabaabb.

Defines rule #8.

Referenced by [36], [38], [40].

Overlap of [26] abaabd=dabaab with [25] db=bd:

Critical pair: abaabbd=dabaabb.

Defines rule #11.

Referenced by [37].

Simplify [8] abaaab=dbaacaba.

Reduce RHS:

Defines rule #12.

Referenced by [34].

Overlap of [33] abaaab=bdaacaba with [2] bbb=c:

Critical pair: abaaac=bdaacababb.

Flip LHS and RHS.

Referenced by [35].

Overlap of [2] bbb=c with [34] bdaacababb=abaaac:

Critical pair: bbabaaac=cdaacababb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [30] aaabaabb=bbdacabaaa with [31] abaabbc=cabaabb:

Critical pair: aacabaabb=bbdacabaaac.

Defines rule #15.

Referenced by [38].

Overlap of [30] aaabaabb=bbdacabaaa with [32] abaabbd=dabaabb:

Critical pair: aadabaabb=bbdacabaaad.

Flip LHS and RHS.

Referenced by [39].

Overlap of [36] aacabaabb=bbdacabaaac with [31] abaabbc=cabaabb:

Critical pair: aaccabaabb=bbdacabaaacc.

Defines rule #16.

Referenced by [40].

Overlap of [2] bbb=c with [37] bbdacabaaad=aadabaabb:

Critical pair: baadabaabb=cdacabaaad.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [38] aaccabaabb=bbdacabaaacc with [31] abaabbc=cabaabb:

Critical pair: aacccabaabb=bbdacabaaaccc.

Flip LHS and RHS.

Referenced by [41].

Overlap of [2] bbb=c with [40] bbdacabaaaccc=aacccabaabb:

Critical pair: baacccabaabb=cdacabaaaccc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.