Certificate for #3105 ⟨a, b | aabbaabaaab=1⟩

Completion settings:

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

Axiom: aabbaabaaab=1.

Referenced by [4].

Axiom: baab=c.

Referenced by [4], [5], [6], [8], [11].

Axiom: caaa=d.

Referenced by [4], [7], [9], [11], [15].

Overlap of [1] aabbaabaaab=1 with [2] baab=c:

Critical pair: aabcaaab=1.

Reduce LHS:

Referenced by [6], [7], [13].

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

Critical pair: baac=caab.

Flip LHS and RHS.

Referenced by [23].

Overlap of [2] baab=c with [4] aabdb=1:

Critical pair: b=cdb.

Flip LHS and RHS.

Referenced by [8], [10].

Overlap of [3] caaa=d with [4] aabdb=1:

Critical pair: ca=dbdb.

Flip LHS and RHS.

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

Overlap of [6] cdb=b with [2] baab=c:

Critical pair: cdc=baab.

Reduce RHS:

Referenced by [9].

Overlap of [8] cdc=c with [3] caaa=d:

Critical pair: cdd=caaa.

Reduce RHS:

Referenced by [14].

Overlap of [6] cdb=b with [7] dbdb=ca:

Critical pair: cca=bdb.

Flip LHS and RHS.

Defines rule #6.

Overlap of [7] dbdb=ca with [2] baab=c:

Critical pair: dbdc=caaab.

Reduce RHS:

Referenced by [13].

Overlap of [7] dbdb=ca with [7] dbdb=ca:

Critical pair: dbca=cadb.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] aabdb=1 with [11] dbdc=db:

Critical pair: aabdb=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [15], [17], [18], [23].

Overlap of [9] cdd=d with [13] dc=1:

Critical pair: cd=dc.

Reduce RHS:

Defines rule #2.

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

Overlap of [13] dc=1 with [3] caaa=d:

Critical pair: dd=aaa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [16].

Overlap of [15] aaa=dd with [15] aaa=dd:

Critical pair: add=dda.

Referenced by [17].

Overlap of [16] add=dda with [13] dc=1:

Critical pair: ad=ddac.

Defines rule #3.

Referenced by [18], [21].

Overlap of [17] ad=ddac with [13] dc=1:

Critical pair: a=ddacc.

Flip LHS and RHS.

Referenced by [19].

Overlap of [14] cd=1 with [18] ddacc=a:

Critical pair: ca=dacc.

Flip LHS and RHS.

Referenced by [20].

Overlap of [14] cd=1 with [19] dacc=ca:

Critical pair: cca=acc.

Flip LHS and RHS.

Defines rule #4.

Simplify [12] cadb=dbca.

Reduce LHS:

Referenced by [22].

Overlap of [14] cd=1 with [21] dacb=dbca:

Critical pair: cdbca=acb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [13] dc=1 with [5] caab=baac:

Critical pair: dbaac=aab.

Flip LHS and RHS.

Defines rule #8.