Certificate for #2936 ⟨a, b | aaababababa=1⟩

Completion settings:

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

Axiom: aaababababa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #2.

Referenced by [5], [6], [7], [9], [11], [19], [24], [25].

Axiom: bababab=d.

Referenced by [4], [21], [24].

Overlap of [1] aaababababa=1 with [3] bababab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12], [14], [16].

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [12], [15], [24], [25].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10], [11], [13], [14].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

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

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

Overlap of [6] cda=a with [4] aaada=1:

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [7] cada=aa with [4] aaada=1:

Critical pair: cad=aaaada.

Reduce RHS:

Referenced by [12], [15], [20], [22].

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Referenced by [15], [16].

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaada=1 with [8] aaad=aada:

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #4.

Referenced by [17], [18], [23], [32].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [15] cddaa=ada with [16] cd=1:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [19].

Simplify [17] adaaa=1.

Reduce LHS:

Defines rule #3.

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

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #5.

Referenced by [21], [24], [25].

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

Critical pair: bad=dab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [11] cad=a with [21] dab=bda:

Critical pair: cabda=aab.

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [16] cd=1 with [21] dab=bda:

Critical pair: cbda=ab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [24], [25].

Overlap of [21] dab=bda with [3] bababab=d:

Critical pair: dad=bdaababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [2] aaaa=c with [23] ab=cbda:

Critical pair: aaacbda=cb.

Reduce LHS:

Referenced by [26].

Overlap of [19] dc=1 with [25] ccccbddd=cb:

Critical pair: dcb=cccbddd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27], [28].

Overlap of [19] dc=1 with [26] cccbddd=b:

Critical pair: db=ccbddd.

Defines rule #8.

Referenced by [31].

Overlap of [26] cccbddd=b with [19] dc=1:

Critical pair: cccbdd=bc.

Referenced by [29].

Overlap of [28] cccbdd=bc with [19] dc=1:

Critical pair: cccbd=bcc.

Referenced by [30].

Overlap of [29] cccbd=bcc with [19] dc=1:

Critical pair: cccb=bccc.

Defines rule #7.

Referenced by [32].

Overlap of [24] bcbcbddb=dda with [27] db=ccbddd:

Critical pair: bcbcbdccbddd=dda.

Reduce LHS:

Referenced by [32].

Overlap of [30] cccb=bccc with [31] bcbcbcbddd=dda:

Critical pair: cccdda=bccccbcbcbddd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.