Certificate for #2875 ⟨a, b | aaaabbaabba=1⟩

Completion settings:

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

Axiom: aaaabbaabba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [4], [5], [6], [7], [9], [16], [25].

Axiom: aabb=d.

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

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

Critical pair: cabbaabba=1.

Reduce LHS:

Referenced by [8].

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

Critical pair: ac=ca.

Defines rule #2.

Referenced by [14], [21], [22], [23].

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

Critical pair: ad=cbb.

Flip LHS and RHS.

Referenced by [18], [20].

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

Critical pair: aad=cabb.

Flip LHS and RHS.

Referenced by [8].

Simplify [4] cabbda=1.

Reduce LHS:

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

Overlap of [2] aaa=c with [8] aadda=1:

Critical pair: a=cdda.

Flip LHS and RHS.

Referenced by [11].

Overlap of [8] aadda=1 with [8] aadda=1:

Critical pair: aadd=adda.

Referenced by [11], [12].

Overlap of [9] cdda=a with [8] aadda=1:

Critical pair: cdd=aadda.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [8] aadda=1 with [10] aadd=adda:

Critical pair: addaa=1.

Reduce LHS:

Defines rule #3.

Referenced by [13], [14], [17], [22], [24], [26].

Simplify [11] addaa=cdd.

Reduce RHS:

Referenced by [15], [16], [21].

Overlap of [5] ac=ca with [12] cdd=1:

Critical pair: a=cadd.

Flip LHS and RHS.

Referenced by [19].

Overlap of [13] addaa=1 with [13] addaa=1:

Critical pair: adda=ddaa.

Referenced by [16].

Overlap of [13] addaa=1 with [15] adda=ddaa:

Critical pair: ddaaa=1.

Reduce LHS:

Referenced by [17], [18], [19], [21].

Overlap of [12] cdd=1 with [16] ddc=1:

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [23].

Overlap of [16] ddc=1 with [6] cbb=ad:

Critical pair: ddad=bb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [20].

Overlap of [16] ddc=1 with [14] cadd=a:

Critical pair: dda=add.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [24], [26].

Overlap of [6] cbb=ad with [18] bb=ddad:

Critical pair: cbddad=adb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [21].

Overlap of [13] addaa=1 with [20] adb=cbddad:

Critical pair: addacbddad=db.

Reduce LHS:

Referenced by [22].

Overlap of [21] aabddad=db with [17] dc=cd:

Critical pair: aabddacd=dbc.

Reduce LHS:

Referenced by [23].

Overlap of [22] aabad=dbc with [17] dc=cd:

Critical pair: aabacd=dbcc.

Reduce LHS:

Referenced by [24].

Overlap of [23] aabcad=dbcc with [19] add=dda:

Critical pair: aabcdda=dbccd.

Reduce LHS:

Referenced by [25].

Overlap of [24] aaba=dbccd with [2] aaa=c:

Critical pair: aabc=dbccdaa.

Referenced by [26].

Overlap of [25] aabc=dbccdaa with [12] cdd=1:

Critical pair: aab=dbccdaadd.

Reduce RHS:

Defines rule #7.