Certificate for #3083 ⟨a, b | aababbabbba=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. aaa=c
  2. babbabbb=d

Axiom: aababbabbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [20], [27], [33].

Axiom: babbabbb=d.

Defines rule #18.

Referenced by [4], [11], [15], [16], [25].

Overlap of [1] aababbabbba=1 with [3] babbabbb=d:

Critical pair: aada=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [22], [24].

Overlap of [2] aaa=c with [4] aada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

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

Overlap of [4] aada=1 with [7] ada=aad:

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [12], [18], [21], [23], [30].

Overlap of [9] da=ad with [2] aaa=c:

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [15], [19], [21], [26], [28], [31].

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

Critical pair: babbabbd=dabbabbb.

Reduce RHS:

Defines rule #14.

Referenced by [12], [13].

Overlap of [11] babbabbd=adbbabbb with [9] da=ad:

Critical pair: babbabbad=adbbabbba.

Defines rule #15.

Referenced by [30].

Overlap of [11] babbabbd=adbbabbb with [10] dc=1:

Critical pair: babbabb=adbbabbbc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] adbbabbbc=babbabb:

Critical pair: aababbabb=cdbbabbbc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [3] babbabbb=d with [14] bbabbbc=aababbabb:

Critical pair: baaababbabb=dc.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17].

Overlap of [15] bcbabbabb=1 with [3] babbabbb=d:

Critical pair: bcbabd=abbb.

Defines rule #7.

Referenced by [18], [19].

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

Critical pair: bcbabbab=cbabbabb.

Referenced by [25], [29].

Overlap of [16] bcbabd=abbb with [9] da=ad:

Critical pair: bcbabad=abbba.

Defines rule #9.

Referenced by [23].

Overlap of [16] bcbabd=abbb with [10] dc=1:

Critical pair: bcbab=abbbc.

Flip LHS and RHS.

Referenced by [20].

Overlap of [2] aaa=c with [19] abbbc=bcbab:

Critical pair: aabcbab=cbbbc.

Flip LHS and RHS.

Referenced by [21].

Overlap of [10] dc=1 with [20] cbbbc=aabcbab:

Critical pair: daabcbab=bbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [22].

Overlap of [21] bbbc=aadbcbab with [5] ca=ac:

Critical pair: bbbac=aadbcbaba.

Defines rule #8.

Referenced by [24].

Overlap of [18] bcbabad=abbba with [9] da=ad:

Critical pair: bcbabaad=abbbaa.

Defines rule #11.

Overlap of [22] bbbac=aadbcbaba with [5] ca=ac:

Critical pair: bbbaac=aadbcbabaa.

Defines rule #10.

Overlap of [17] bcbabbab=cbabbabb with [3] babbabbb=d:

Critical pair: bcbabbad=cbabbabbabbabbb.

Reduce RHS:

Referenced by [26].

Overlap of [25] bcbabbad=cbabbabd with [10] dc=1:

Critical pair: bcbabba=cbabbabdc.

Reduce RHS:

Defines rule #12.

Referenced by [27].

Overlap of [26] bcbabba=cbabbab with [2] aaa=c:

Critical pair: bcbabbc=cbabbabaa.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [10] dc=1 with [27] cbabbabaa=bcbabbc:

Critical pair: dbcbabbc=babbabaa.

Flip LHS and RHS.

Defines rule #13.

Overlap of [17] bcbabbab=cbabbabb with [27] cbabbabaa=bcbabbc:

Critical pair: bbcbabbc=cbabbabbaa.

Flip LHS and RHS.

Referenced by [31].

Overlap of [12] babbabbad=adbbabbba with [9] da=ad:

Critical pair: babbabbaad=adbbabbbaa.

Referenced by [32].

Overlap of [10] dc=1 with [29] cbabbabbaa=bbcbabbc:

Critical pair: dbbcbabbc=babbabbaa.

Flip LHS and RHS.

Defines rule #17.

Referenced by [32].

Simplify [30] babbabbaad=adbbabbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [2] aaa=c with [32] adbbabbbaa=dbbcbabb:

Critical pair: aadbbcbabb=cdbbabbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.