Certificate for #3259 ⟨a, b | ababbabbbba=1⟩

Completion settings:

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

Axiom: ababbabbbba=1.

Referenced by [4].

Axiom: babbbb=c.

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

Axiom: bcaa=d.

Referenced by [5], [17].

Overlap of [1] ababbabbbba=1 with [2] babbbb=c:

Critical pair: ababca=1.

Referenced by [5], [6], [9], [10], [11].

Overlap of [4] ababca=1 with [3] bcaa=d:

Critical pair: abad=a.

Referenced by [6].

Overlap of [4] ababca=1 with [5] abad=a:

Critical pair: ababca=bad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7], [13], [20], [21].

Overlap of [2] babbbb=c with [6] bad=1:

Critical pair: babbb=cad.

Referenced by [8], [12].

Overlap of [2] babbbb=c with [7] babbb=cad:

Critical pair: cadb=c.

Referenced by [9], [14].

Overlap of [4] ababca=1 with [8] cadb=c:

Critical pair: ababc=db.

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

Overlap of [4] ababca=1 with [9] ababc=db:

Critical pair: dba=1.

Referenced by [12], [16], [24].

Overlap of [4] ababca=1 with [9] ababc=db:

Critical pair: ababcdb=babc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [10] dba=1 with [7] babbb=cad:

Critical pair: dcad=bbb.

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [12] bbb=dcad with [6] bad=1:

Critical pair: bb=dcadad.

Referenced by [19].

Overlap of [12] bbb=dcad with [12] bbb=dcad:

Critical pair: bdcad=dcadb.

Reduce RHS:

Referenced by [18].

Overlap of [9] ababc=db with [11] babc=dbdb:

Critical pair: adbdb=db.

Referenced by [16].

Overlap of [15] adbdb=db with [10] dba=1:

Critical pair: adb=dba.

Reduce RHS:

Referenced by [17], [18].

Overlap of [16] adb=1 with [3] bcaa=d:

Critical pair: add=caa.

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [16] adb=1 with [14] bdcad=dc:

Critical pair: addc=dcad.

Flip LHS and RHS.

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

Simplify [13] bb=dcadad.

Reduce RHS:

Referenced by [20].

Overlap of [19] bb=adaddc with [6] bad=1:

Critical pair: b=adaddcad.

Reduce RHS:

Defines rule #6.

Referenced by [21].

Overlap of [6] bad=1 with [20] b=adadaddc:

Critical pair: adadaddcad=1.

Reduce LHS:

Defines rule #3.

Referenced by [22], [23], [26], [28].

Overlap of [17] caa=add with [21] adadadaddc=1:

Critical pair: ca=adddadadaddc.

Defines rule #4.

Referenced by [26].

Overlap of [21] adadadaddc=1 with [17] caa=add:

Critical pair: adadadaddadd=aa.

Referenced by [24].

Overlap of [10] dba=1 with [23] adadadaddadd=aa:

Critical pair: dbaa=dadadaddadd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [25], [26], [27].

Overlap of [24] dadadaddadd=a with [24] dadadaddadd=a:

Critical pair: dadadaddada=aadadaddadd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [26].

Overlap of [22] ca=adddadadaddc with [25] aadadaddadd=dadadaddada:

Critical pair: cdadadaddada=adddadadaddcadadaddadd.

Reduce RHS:

Referenced by [27].

Overlap of [26] cdadadaddada=adddadaddadd with [24] dadadaddadd=a:

Critical pair: cdadadada=adddadaddadddaddadd.

Referenced by [28].

Overlap of [27] cdadadada=adddadaddadddaddadd with [21] adadadaddc=1:

Critical pair: cd=adddadaddadddaddaddddc.

Defines rule #5.