Certificate for #2831 ⟨a, b | aaaaabbabba=1⟩

Completion settings:

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

Axiom: aaaaabbabba=1.

Referenced by [4].

Axiom: bba=c.

Referenced by [4], [5].

Axiom: aaaaa=d.

Defines rule #5.

Referenced by [4], [5], [6], [9], [15], [18], [19], [20], [27], [28].

Overlap of [1] aaaaabbabba=1 with [3] aaaaa=d:

Critical pair: dbbabba=1.

Reduce LHS:

Defines rule #3.

Referenced by [7], [8], [9], [10], [19], [21], [22], [26], [30], [31].

Overlap of [2] bba=c with [3] aaaaa=d:

Critical pair: bbd=caaaa.

Referenced by [8], [9].

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

Critical pair: ad=da.

Defines rule #2.

Referenced by [7], [17], [29].

Overlap of [6] ad=da with [4] dcc=1:

Critical pair: a=dacc.

Flip LHS and RHS.

Referenced by [9], [23].

Overlap of [5] bbd=caaaa with [4] dcc=1:

Critical pair: bb=caaaacc.

Referenced by [9], [13].

Overlap of [5] bbd=caaaa with [7] dacc=a:

Critical pair: bba=caaaaacc.

Reduce LHS:

Reduce RHS:

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

Overlap of [4] dcc=1 with [9] caaaacca=c:

Critical pair: dcc=aaaacca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [14].

Overlap of [9] caaaacca=c with [9] caaaacca=c:

Critical pair: caaaacc=caaacca.

Referenced by [13].

Overlap of [10] aaaacca=1 with [9] caaaacca=c:

Critical pair: aaaacc=aaacca.

Referenced by [14].

Simplify [8] bb=caaaacc.

Reduce RHS:

Referenced by [24].

Overlap of [10] aaaacca=1 with [12] aaaacc=aaacca:

Critical pair: aaaccaa=1.

Referenced by [15], [16], [18], [19].

Overlap of [14] aaaccaa=1 with [3] aaaaa=d:

Critical pair: aaaccd=aaa.

Referenced by [17].

Overlap of [14] aaaccaa=1 with [14] aaaccaa=1:

Critical pair: aaacc=accaa.

Referenced by [17], [18], [24].

Simplify [15] aaaccd=aaa.

Reduce LHS:

Referenced by [18], [19].

Overlap of [14] aaaccaa=1 with [17] accdaa=aaa:

Critical pair: aaaccaaaa=ccdaa.

Reduce LHS:

Referenced by [19].

Overlap of [17] accdaa=aaa with [14] aaaccaa=1:

Critical pair: accda=aaaaaccaa.

Reduce LHS:

Reduce RHS:

Referenced by [20].

Overlap of [19] ccdaa=aa with [3] aaaaa=d:

Critical pair: ccdd=aaaaa.

Reduce RHS:

Referenced by [21].

Overlap of [20] ccdd=d with [4] dcc=1:

Critical pair: ccd=dcc.

Reduce RHS:

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

Overlap of [4] dcc=1 with [21] ccd=1:

Critical pair: dc=cd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [29], [31].

Overlap of [21] ccd=1 with [7] dacc=a:

Critical pair: cca=acc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [24], [27].

Simplify [13] bb=caaacca.

Reduce RHS:

Defines rule #8.

Referenced by [25].

Overlap of [24] bb=cccaaaa with [24] bb=cccaaaa:

Critical pair: bcccaaaa=cccaaaab.

Flip LHS and RHS.

Referenced by [26], [27].

Overlap of [4] dcc=1 with [25] cccaaaab=bcccaaaa:

Critical pair: dbcccaaaa=caaaab.

Flip LHS and RHS.

Referenced by [31].

Overlap of [23] acc=cca with [25] cccaaaab=bcccaaaa:

Critical pair: acbcccaaaa=ccaccaaaab.

Reduce RHS:

Referenced by [28].

Overlap of [27] acbcccaaaa=ccb with [3] aaaaa=d:

Critical pair: acbcccd=ccba.

Reduce LHS:

Referenced by [29].

Overlap of [28] acbc=ccba with [22] cd=dc:

Critical pair: acbdc=ccbad.

Reduce RHS:

Referenced by [30].

Overlap of [29] acbdc=ccbda with [4] dcc=1:

Critical pair: acb=ccbdac.

Defines rule #6.

Overlap of [4] dcc=1 with [26] caaaab=dbcccaaaa:

Critical pair: dcdbcccaaaa=aaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.