Certificate for #2795 ⟨a, b | aaaaaabaaba=1⟩

Completion settings:

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

Axiom: aaaaaabaaba=1.

Referenced by [4].

Axiom: aaaaaaa=c.

Defines rule #5.

Referenced by [6], [7], [15], [16], [17], [21], [22], [32], [37], [38], [40], [44].

Axiom: baab=d.

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

Overlap of [1] aaaaaabaaba=1 with [3] baab=d:

Critical pair: aaaaaada=1.

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

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

Critical pair: baad=daab.

Flip LHS and RHS.

Referenced by [10].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #1.

Referenced by [11], [12], [13], [21], [23], [37], [38], [39], [44].

Overlap of [2] aaaaaaa=c with [4] aaaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: aaaaaad=aaaaada.

Flip LHS and RHS.

Referenced by [15], [16], [17].

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

Critical pair: cd=aaaaaada.

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [17], [22], [24], [30], [32], [38], [39], [40], [45].

Overlap of [7] cda=a with [5] daab=baad:

Critical pair: cbaad=aab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [11], [14], [18], [27], [31], [38], [40].

Overlap of [6] ca=ac with [10] aab=cbaad:

Critical pair: ccbaad=acab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [32], [38].

Overlap of [6] ca=ac with [11] aacb=ccbaad:

Critical pair: cccbaad=acacb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [38].

Overlap of [6] ca=ac with [12] aaccb=cccbaad:

Critical pair: ccccbaad=acaccb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [3] baab=d with [10] aab=cbaad:

Critical pair: bcbaad=d.

Referenced by [19].

Overlap of [8] aaaaada=aaaaaad with [8] aaaaada=aaaaaad:

Critical pair: aaaaadaaaaaad=aaaaaadaaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [15] aaada=aaaad with [8] aaaaada=aaaaaad:

Critical pair: aaadaaaaaad=aaaadaaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [16] ada=aad with [2] aaaaaaa=c:

Critical pair: adc=aadaaaaaa.

Reduce RHS:

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

Overlap of [16] ada=aad with [10] aab=cbaad:

Critical pair: adcbaad=aadab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [14] bcbaad=d with [17] adc=a:

Critical pair: bcbaa=dc.

Referenced by [21], [25].

Overlap of [16] ada=aad with [17] adc=a:

Critical pair: ada=aaddc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [19] bcbaa=dc with [2] aaaaaaa=c:

Critical pair: bcbc=dcaaaaa.

Reduce RHS:

Referenced by [26].

Overlap of [2] aaaaaaa=c with [20] aaddc=aad:

Critical pair: aaaaaaad=cddc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [23], [25], [26], [27], [33], [34], [35], [36], [38], [41], [42], [43].

Overlap of [22] dc=1 with [6] ca=ac:

Critical pair: dac=a.

Referenced by [24].

Overlap of [23] dac=a with [9] cd=1:

Critical pair: da=ad.

Defines rule #3.

Referenced by [26], [27], [29], [31], [32], [33], [38], [40].

Simplify [19] bcbaa=dc.

Reduce RHS:

Referenced by [28].

Simplify [21] bcbc=daaaaac.

Reduce RHS:

Referenced by [30].

Overlap of [24] da=ad with [10] aab=cbaad:

Critical pair: dcbaad=adab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [28], [29].

Overlap of [25] bcbaa=1 with [27] aadb=baad:

Critical pair: bcbbaad=db.

Referenced by [31].

Overlap of [24] da=ad with [27] aadb=baad:

Critical pair: dbaad=adadb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [40].

Overlap of [26] bcbc=aaaaa with [9] cd=1:

Critical pair: bcb=aaaaad.

Defines rule #11.

Referenced by [31], [38], [39].

Simplify [28] bcbbaad=db.

Reduce LHS:

Referenced by [32], [33].

Overlap of [11] aacb=ccbaad with [31] acbaaaaaaddd=db:

Critical pair: adb=ccbaadaaaaaaddd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [24] da=ad with [31] acbaaaaaaddd=db:

Critical pair: ddb=adcbaaaaaaddd.

Reduce RHS:

Defines rule #9.

Referenced by [40].

Overlap of [32] ccbaddd=adb with [22] dc=1:

Critical pair: ccbadd=adbc.

Referenced by [35].

Overlap of [34] ccbadd=adbc with [22] dc=1:

Critical pair: ccbad=adbcc.

Referenced by [36].

Overlap of [35] ccbad=adbcc with [22] dc=1:

Critical pair: ccba=adbccc.

Referenced by [37], [38].

Overlap of [36] ccba=adbccc with [2] aaaaaaa=c:

Critical pair: ccbc=adbcccaaaaaa.

Reduce RHS:

Referenced by [38].

Overlap of [36] ccba=adbccc with [10] aab=cbaad:

Critical pair: ccbcbaad=adbcccab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [38] adbacccb=c with [30] bcb=aaaaad:

Critical pair: adbacccaaaaad=ccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [29] aaddb=dbaad with [33] ddb=abaaaaaaddd:

Critical pair: aaabaaaaaaddd=dbaad.

Reduce LHS:

Referenced by [41].

Overlap of [40] acbaddd=dbaad with [22] dc=1:

Critical pair: acbadd=dbaadc.

Reduce RHS:

Referenced by [42].

Overlap of [41] acbadd=dbaa with [22] dc=1:

Critical pair: acbad=dbaac.

Referenced by [43].

Overlap of [42] acbad=dbaac with [22] dc=1:

Critical pair: acba=dbaacc.

Referenced by [44].

Overlap of [43] acba=dbaacc with [2] aaaaaaa=c:

Critical pair: acbc=dbaaccaaaaaa.

Reduce RHS:

Referenced by [45].

Overlap of [44] acbc=dbaccc with [9] cd=1:

Critical pair: acb=dbacccd.

Reduce RHS:

Defines rule #7.