Certificate for #2787 ⟨a, b | aaaaaaababa=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. aaaaaaaa=c
  2. bab=d

Axiom: aaaaaaababa=1.

Referenced by [4].

Axiom: aaaaaaaa=c.

Defines rule #2.

Referenced by [6], [7], [8], [12], [17], [20], [22], [24], [29], [30].

Axiom: bab=d.

Referenced by [4], [5], [13].

Overlap of [1] aaaaaaababa=1 with [3] bab=d:

Critical pair: aaaaaaada=1.

Referenced by [7], [8], [9], [10], [12], [14].

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

Critical pair: bad=dab.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [24], [30].

Overlap of [2] aaaaaaaa=c with [4] aaaaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

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

Overlap of [2] aaaaaaaa=c with [4] aaaaaaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [12].

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

Critical pair: aaaaaaad=aaaaaada.

Referenced by [10], [14].

Overlap of [7] cda=a with [4] aaaaaaada=1:

Critical pair: cd=aaaaaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14], [15].

Overlap of [7] cda=a with [5] dab=bad:

Critical pair: cbad=ab.

Flip LHS and RHS.

Referenced by [13], [30], [32].

Overlap of [8] cada=aa with [4] aaaaaaada=1:

Critical pair: cad=aaaaaaaada.

Reduce RHS:

Referenced by [23], [25].

Overlap of [3] bab=d with [11] ab=cbad:

Critical pair: bcbad=d.

Referenced by [27].

Overlap of [4] aaaaaaada=1 with [9] aaaaaaad=aaaaaada:

Critical pair: aaaaaadaa=1.

Reduce LHS:

Defines rule #4.

Referenced by [15], [17], [24], [25], [26], [31].

Simplify [10] aaaaaadaa=cd.

Reduce RHS:

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

Overlap of [15] aaaaaadaa=1 with [15] aaaaaadaa=1:

Critical pair: aaaaaad=aaaadaa.

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

Overlap of [2] aaaaaaaa=c with [16] aaaaaad=aaaadaa:

Critical pair: aaaaaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [18].

Overlap of [15] aaaaaadaa=1 with [16] aaaaaad=aaaadaa:

Critical pair: aaaaaadaaaadaa=aaaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [24], [30].

Overlap of [15] aaaaaadaa=1 with [16] aaaaaad=aaaadaa:

Critical pair: aaaadaaaa=1.

Reduce LHS:

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

Overlap of [19] aadaaaaaa=1 with [2] aaaaaaaa=c:

Critical pair: aadc=aa.

Referenced by [22], [23].

Overlap of [19] aadaaaaaa=1 with [19] aadaaaaaa=1:

Critical pair: aadaaaa=daaaaaa.

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

Overlap of [19] aadaaaaaa=1 with [20] aadc=aa:

Critical pair: aadaaaaaaa=adc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [20] aadc=aa with [12] cad=a:

Critical pair: aada=aaad.

Flip LHS and RHS.

Referenced by [24], [30].

Overlap of [2] aaaaaaaa=c with [22] adc=dca:

Critical pair: aaaaaaadca=cdc.

Reduce LHS:

Reduce RHS:

Referenced by [26].

Overlap of [22] adc=dca with [14] cd=1:

Critical pair: ad=dcad.

Reduce RHS:

Defines rule #5.

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

Overlap of [24] dcc=c with [14] cd=1:

Critical pair: dc=cd.

Reduce RHS:

Defines rule #3.

Referenced by [27], [29], [30], [33], [34], [35], [36], [37], [38], [39].

Overlap of [13] bcbad=d with [26] dc=1:

Critical pair: bcba=dc.

Reduce RHS:

Referenced by [28].

Overlap of [27] bcba=1 with [25] ad=da:

Critical pair: bcbda=d.

Referenced by [29], [30].

Overlap of [28] bcbda=d with [2] aaaaaaaa=c:

Critical pair: bcbdc=daaaaaaa.

Reduce LHS:

Defines rule #9.

Referenced by [30].

Overlap of [28] bcbda=d with [11] ab=cbad:

Critical pair: bcbdcbad=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [31].

Overlap of [14] cd=1 with [30] db=ccccccbddddddd:

Critical pair: cccccccbddddddd=b.

Referenced by [33].

Simplify [11] ab=cbad.

Reduce RHS:

Defines rule #6.

Overlap of [31] cccccccbddddddd=b with [26] dc=1:

Critical pair: cccccccbdddddd=bc.

Referenced by [34].

Overlap of [33] cccccccbdddddd=bc with [26] dc=1:

Critical pair: cccccccbddddd=bcc.

Referenced by [35].

Overlap of [34] cccccccbddddd=bcc with [26] dc=1:

Critical pair: cccccccbdddd=bccc.

Referenced by [36].

Overlap of [35] cccccccbdddd=bccc with [26] dc=1:

Critical pair: cccccccbddd=bcccc.

Referenced by [37].

Overlap of [36] cccccccbddd=bcccc with [26] dc=1:

Critical pair: cccccccbdd=bccccc.

Referenced by [38].

Overlap of [37] cccccccbdd=bccccc with [26] dc=1:

Critical pair: cccccccbd=bcccccc.

Referenced by [39].

Overlap of [38] cccccccbd=bcccccc with [26] dc=1:

Critical pair: cccccccb=bccccccc.

Defines rule #7.