Certificate for #2964 ⟨a, b | aaabbaabbaa=1⟩

Completion settings:

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

Axiom: aaabbaabbaa=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #7.

Referenced by [4], [5], [6], [19], [24].

Axiom: bbaa=d.

Referenced by [4], [6], [8], [12].

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

Critical pair: cbbaabbaa=1.

Reduce LHS:

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [3] bbaa=d with [2] aaa=c:

Critical pair: bbc=da.

Referenced by [7], [9].

Overlap of [6] bbc=da with [4] cdd=1:

Critical pair: bb=dadd.

Defines rule #6.

Referenced by [8], [9], [10], [12].

Overlap of [3] bbaa=d with [7] bb=dadd:

Critical pair: daddaa=d.

Referenced by [12].

Overlap of [6] bbc=da with [7] bb=dadd:

Critical pair: daddc=da.

Referenced by [11].

Overlap of [7] bb=dadd with [7] bb=dadd:

Critical pair: bdadd=daddb.

Referenced by [18].

Overlap of [4] cdd=1 with [9] daddc=da:

Critical pair: cdda=addc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [3] bbaa=d with [11] addc=a:

Critical pair: bbaa=dddc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [4] cdd=1 with [12] dddc=d:

Critical pair: cd=dc.

Defines rule #1.

Referenced by [14], [16], [17], [20], [21], [22], [24].

Overlap of [4] cdd=1 with [13] cd=dc:

Critical pair: dcd=1.

Reduce LHS:

Defines rule #2.

Referenced by [15], [17], [18], [20], [21], [22], [24].

Overlap of [14] ddc=1 with [5] ca=ac:

Critical pair: ddac=a.

Referenced by [16].

Overlap of [15] ddac=a with [13] cd=dc:

Critical pair: ddadc=ad.

Referenced by [17].

Overlap of [16] ddadc=ad with [13] cd=dc:

Critical pair: ddaddc=add.

Reduce LHS:

Defines rule #4.

Referenced by [23].

Overlap of [10] bdadd=daddb with [14] ddc=1:

Critical pair: bda=daddbc.

Defines rule #5.

Referenced by [19].

Overlap of [18] bda=daddbc with [2] aaa=c:

Critical pair: bdc=daddbcaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [13] cd=dc with [19] daddbaac=bdc:

Critical pair: cbdc=dcaddbaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [20] dabaac=cbdc with [13] cd=dc:

Critical pair: dabaadc=cbdcd.

Reduce RHS:

Referenced by [22].

Overlap of [21] dabaadc=cb with [13] cd=dc:

Critical pair: dabaaddc=cbd.

Reduce LHS:

Referenced by [23].

Overlap of [17] dda=add with [22] dabaa=cbd:

Critical pair: dcbd=addbaa.

Flip LHS and RHS.

Referenced by [24].

Overlap of [2] aaa=c with [23] addbaa=dcbd:

Critical pair: aadcbd=cddbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.