Certificate for #2883 ⟨a, b | aaaabbabbba=1⟩

Completion settings:

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

Axiom: aaaabbabbba=1.

Referenced by [4].

Axiom: aaaaa=c.

Defines rule #5.

Referenced by [5], [6], [14], [18], [19], [23], [26], [33].

Axiom: bbabbb=d.

Defines rule #22.

Referenced by [4], [9], [10], [19], [24].

Overlap of [1] aaaabbabbba=1 with [3] bbabbb=d:

Critical pair: aaaada=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aaaad=aaada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaaada.

Reduce RHS:

Defines rule #2.

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

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

Critical pair: bbabd=dabbb.

Referenced by [15].

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

Critical pair: bbabbd=dbabbb.

Defines rule #17.

Referenced by [22], [23].

Overlap of [4] aaaada=1 with [7] aaada=aaaad:

Critical pair: aaaadaaaad=aada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [7] aaada=aaaad with [7] aaada=aaaad:

Critical pair: aaadaaaad=aaaadaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [12] ada=aad with [4] aaaada=1:

Critical pair: ad=aadaaada.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [14], [15], [16], [21], [22], [28], [30], [32], [34].

Overlap of [13] da=ad with [2] aaaaa=c:

Critical pair: dc=adaaaa.

Reduce RHS:

Defines rule #1.

Referenced by [17], [19], [23], [24], [35].

Simplify [9] bbabd=dabbb.

Reduce RHS:

Defines rule #7.

Referenced by [16], [17].

Overlap of [15] bbabd=adbbb with [13] da=ad:

Critical pair: bbabad=adbbba.

Defines rule #10.

Referenced by [21].

Overlap of [15] bbabd=adbbb with [14] dc=1:

Critical pair: bbab=adbbbc.

Flip LHS and RHS.

Referenced by [18].

Overlap of [2] aaaaa=c with [17] adbbbc=bbab:

Critical pair: aaaabbab=cdbbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

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

Overlap of [3] bbabbb=d with [18] bbbc=aaaabbab:

Critical pair: bbaaaaabbab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [24].

Overlap of [18] bbbc=aaaabbab with [5] ca=ac:

Critical pair: bbbac=aaaabbaba.

Defines rule #9.

Referenced by [27].

Overlap of [16] bbabad=adbbba with [13] da=ad:

Critical pair: bbabaad=adbbbaa.

Defines rule #12.

Referenced by [28].

Overlap of [10] bbabbd=dbabbb with [13] da=ad:

Critical pair: bbabbad=dbabbba.

Defines rule #18.

Referenced by [30].

Overlap of [10] bbabbd=dbabbb with [14] dc=1:

Critical pair: bbabb=dbabbbc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [23] dbcbbab=bbabb with [19] bbcbbab=1:

Critical pair: dbcbba=bbabbbcbbab.

Reduce RHS:

Referenced by [25], [26].

Overlap of [8] cd=1 with [24] dbcbba=bbab:

Critical pair: cbbab=bcbba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [29].

Overlap of [24] dbcbba=bbab with [2] aaaaa=c:

Critical pair: dbcbbc=bbabaaaa.

Flip LHS and RHS.

Defines rule #16.

Referenced by [29], [32].

Overlap of [20] bbbac=aaaabbaba with [5] ca=ac:

Critical pair: bbbaac=aaaabbabaa.

Defines rule #11.

Referenced by [31].

Overlap of [21] bbabaad=adbbbaa with [13] da=ad:

Critical pair: bbabaaad=adbbbaaa.

Defines rule #14.

Referenced by [32].

Overlap of [25] bcbba=cbbab with [26] bbabaaaa=dbcbbc:

Critical pair: bcdbcbbc=cbbabbaaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [22] bbabbad=dbabbba with [13] da=ad:

Critical pair: bbabbaad=dbabbbaa.

Defines rule #19.

Referenced by [34].

Overlap of [27] bbbaac=aaaabbabaa with [5] ca=ac:

Critical pair: bbbaaac=aaaabbabaaa.

Defines rule #13.

Overlap of [28] bbabaaad=adbbbaaa with [13] da=ad:

Critical pair: bbabaaaad=adbbbaaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [2] aaaaa=c with [32] adbbbaaaa=dbcbb:

Critical pair: aaaadbcbb=cdbbbaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [30] bbabbaad=dbabbbaa with [13] da=ad:

Critical pair: bbabbaaad=dbabbbaaa.

Defines rule #20.

Overlap of [14] dc=1 with [29] cbbabbaaaa=bbcbbc:

Critical pair: dbbcbbc=bbabbaaaa.

Flip LHS and RHS.

Defines rule #21.