Certificate for #2823 ⟨a, b | aaaaababbba=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. aaaaaa=c
  2. babbb=d

Axiom: aaaaababbba=1.

Referenced by [4].

Axiom: aaaaaa=c.

Defines rule #5.

Referenced by [6], [7], [15], [18], [20], [23], [27], [30], [34], [37], [40].

Axiom: babbb=d.

Defines rule #20.

Referenced by [4], [5], [23], [25].

Overlap of [1] aaaaababbba=1 with [3] babbb=d:

Critical pair: aaaaada=1.

Referenced by [7], [8], [9], [10], [11], [12], [13], [15].

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

Critical pair: babbd=dabbb.

Referenced by [14], [16].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [19], [21], [31], [35], [38].

Overlap of [2] aaaaaa=c with [4] aaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9].

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

Critical pair: aaaaad=aaaada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaaaada.

Reduce RHS:

Defines rule #2.

Referenced by [18], [20], [30], [34], [37], [39], [40].

Overlap of [4] aaaaada=1 with [8] aaaada=aaaaad:

Critical pair: aaaaadaaaaad=aaada.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [8] aaaada=aaaaad with [8] aaaada=aaaaad:

Critical pair: aaaadaaaaad=aaaaadaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [11] aada=aaad with [4] aaaaada=1:

Critical pair: aad=aaadaaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [11] aada=aaad with [8] aaaada=aaaaad:

Critical pair: aadaaaaad=aaadaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [14], [15], [16], [22], [32], [36].

Overlap of [5] babbd=dabbb with [13] da=ad:

Critical pair: babbad=dabbba.

Reduce RHS:

Defines rule #11.

Referenced by [22].

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

Critical pair: dc=adaaaaa.

Reduce RHS:

Defines rule #1.

Referenced by [17], [23], [26], [28], [33].

Simplify [5] babbd=dabbb.

Reduce RHS:

Defines rule #9.

Referenced by [17].

Overlap of [16] babbd=adbbb with [15] dc=1:

Critical pair: babb=adbbbc.

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [2] aaaaaa=c with [17] adbbbc=babb:

Critical pair: aaaaababb=cdbbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [23].

Overlap of [17] adbbbc=babb with [6] ca=ac:

Critical pair: adbbbac=babba.

Referenced by [20], [21].

Overlap of [2] aaaaaa=c with [19] adbbbac=babba:

Critical pair: aaaaababba=cdbbbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [19] adbbbac=babba with [6] ca=ac:

Critical pair: adbbbaac=babbaa.

Referenced by [30], [31].

Overlap of [14] babbad=adbbba with [13] da=ad:

Critical pair: babbaad=adbbbaa.

Defines rule #13.

Referenced by [32].

Overlap of [3] babbb=d with [18] bbbc=aaaaababb:

Critical pair: baaaaaababb=dc.

Reduce LHS:

Reduce RHS:

Referenced by [24].

Overlap of [23] bcbabb=1 with [23] bcbabb=1:

Critical pair: bcbab=cbabb.

Referenced by [25], [29].

Overlap of [24] bcbab=cbabb with [3] babbb=d:

Critical pair: bcbad=cbabbabbb.

Reduce RHS:

Referenced by [26].

Overlap of [25] bcbad=cbabd with [15] dc=1:

Critical pair: bcba=cbabdc.

Reduce RHS:

Defines rule #6.

Referenced by [27].

Overlap of [26] bcba=cbab with [2] aaaaaa=c:

Critical pair: bcbc=cbabaaaaa.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [15] dc=1 with [27] cbabaaaaa=bcbc:

Critical pair: dbcbc=babaaaaa.

Flip LHS and RHS.

Defines rule #7.

Overlap of [24] bcbab=cbabb with [27] cbabaaaaa=bcbc:

Critical pair: bbcbc=cbabbaaaaa.

Flip LHS and RHS.

Referenced by [33].

Overlap of [2] aaaaaa=c with [21] adbbbaac=babbaa:

Critical pair: aaaaababbaa=cdbbbaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [21] adbbbaac=babbaa with [6] ca=ac:

Critical pair: adbbbaaac=babbaaa.

Referenced by [34], [35].

Overlap of [22] babbaad=adbbbaa with [13] da=ad:

Critical pair: babbaaad=adbbbaaa.

Defines rule #15.

Referenced by [36].

Overlap of [15] dc=1 with [29] cbabbaaaaa=bbcbc:

Critical pair: dbbcbc=babbaaaaa.

Flip LHS and RHS.

Defines rule #19.

Referenced by [38].

Overlap of [2] aaaaaa=c with [31] adbbbaaac=babbaaa:

Critical pair: aaaaababbaaa=cdbbbaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [31] adbbbaaac=babbaaa with [6] ca=ac:

Critical pair: adbbbaaaac=babbaaaa.

Referenced by [37], [38].

Overlap of [32] babbaaad=adbbbaaa with [13] da=ad:

Critical pair: babbaaaad=adbbbaaaa.

Defines rule #17.

Overlap of [2] aaaaaa=c with [35] adbbbaaaac=babbaaaa:

Critical pair: aaaaababbaaaa=cdbbbaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [35] adbbbaaaac=babbaaaa with [6] ca=ac:

Critical pair: adbbbaaaaac=babbaaaaa.

Reduce RHS:

Referenced by [39].

Overlap of [38] adbbbaaaaac=dbbcbc with [9] cd=1:

Critical pair: adbbbaaaaa=dbbcbcd.

Reduce RHS:

Referenced by [40].

Overlap of [2] aaaaaa=c with [39] adbbbaaaaa=dbbcb:

Critical pair: aaaaadbbcb=cdbbbaaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.