Certificate for #3767 ⟨a, b | abababaaab=a⟩

Completion settings:

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

Axiom: abababaaab=a.

Referenced by [5].

Axiom: aaa=c.

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

Axiom: ab=d.

Defines rule #29.

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

Axiom: ddda=e.

Defines rule #3.

Referenced by [5], [8], [9], [10], [11], [14], [22], [29], [32], [33].

Overlap of [1] abababaaab=a with [3] ab=d:

Critical pair: dababaaab=a.

Reduce LHS:

Defines rule #4.

Referenced by [10], [12], [15], [28], [30], [31].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #14.

Referenced by [29], [32], [33].

Overlap of [2] aaa=c with [3] ab=d:

Critical pair: aad=cb.

Flip LHS and RHS.

Referenced by [20].

Overlap of [4] ddda=e with [2] aaa=c:

Critical pair: dddc=eaa.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] ddda=e with [3] ab=d:

Critical pair: dddd=eb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [5] ead=a with [4] ddda=e:

Critical pair: eae=adda.

Flip LHS and RHS.

Defines rule #18.

Referenced by [11], [12], [13], [16], [17], [23], [25].

Overlap of [4] ddda=e with [10] adda=eae:

Critical pair: dddeae=edda.

Defines rule #5.

Referenced by [30], [32].

Overlap of [5] ead=a with [10] adda=eae:

Critical pair: eeae=ada.

Flip LHS and RHS.

Defines rule #16.

Referenced by [14], [15], [16], [17], [18], [24], [26].

Overlap of [10] adda=eae with [10] adda=eae:

Critical pair: addeae=eaedda.

Defines rule #22.

Overlap of [4] ddda=e with [12] ada=eeae:

Critical pair: dddeeae=eda.

Defines rule #7.

Referenced by [31], [33].

Overlap of [5] ead=a with [12] ada=eeae:

Critical pair: eeeae=aa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [19], [20], [21], [22], [23], [24], [25], [26], [27], [28], [30], [31], [32], [33].

Overlap of [10] adda=eae with [12] ada=eeae:

Critical pair: addeeae=eaeda.

Defines rule #25.

Overlap of [12] ada=eeae with [10] adda=eae:

Critical pair: adeae=eeaedda.

Defines rule #20.

Overlap of [12] ada=eeae with [12] ada=eeae:

Critical pair: adeeae=eeaeda.

Defines rule #23.

Overlap of [2] aaa=c with [15] aa=eeeae:

Critical pair: eeeaea=c.

Defines rule #17.

Referenced by [27], [28].

Simplify [7] cb=aad.

Reduce RHS:

Defines rule #28.

Overlap of [8] eaa=dddc with [15] aa=eeeae:

Critical pair: eeeeae=dddc.

Defines rule #6.

Referenced by [28], [30], [31], [32], [33].

Overlap of [4] ddda=e with [15] aa=eeeae:

Critical pair: dddeeeae=ea.

Defines rule #8.

Overlap of [10] adda=eae with [15] aa=eeeae:

Critical pair: addeeeae=eaea.

Defines rule #27.

Overlap of [12] ada=eeae with [15] aa=eeeae:

Critical pair: adeeeae=eeaea.

Defines rule #26.

Overlap of [15] aa=eeeae with [10] adda=eae:

Critical pair: aeae=eeeaedda.

Defines rule #19.

Referenced by [32], [33].

Overlap of [15] aa=eeeae with [12] ada=eeae:

Critical pair: aeeae=eeeaeda.

Defines rule #21.

Overlap of [15] aa=eeeae with [15] aa=eeeae:

Critical pair: aeeeae=eeeaea.

Reduce RHS:

Defines rule #24.

Overlap of [19] eeeaea=c with [5] ead=a:

Critical pair: eeeaa=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [29], [32], [33].

Overlap of [28] cd=eedddc with [4] ddda=e:

Critical pair: ce=eedddcdda.

Reduce RHS:

Defines rule #2.

Overlap of [11] dddeae=edda with [5] ead=a:

Critical pair: dddeaa=eddaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [14] dddeeae=eda with [5] ead=a:

Critical pair: dddeeaa=edaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [11] dddeae=edda with [25] aeae=eeeaedda:

Critical pair: dddeeeeaedda=eddaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [14] dddeeae=eda with [25] aeae=eeeaedda:

Critical pair: dddeeeeeaedda=edaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.