Certificate for #631 ⟨a, b | aaabaabba=1⟩

Completion settings:

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

Axiom: aaabaabba=1.

Referenced by [4].

Axiom: baa=c.

Defines rule #5.

Referenced by [4], [5], [6], [7], [8], [10], [23], [28].

Axiom: bcaa=d.

Referenced by [10], [20].

Overlap of [1] aaabaabba=1 with [2] baa=c:

Critical pair: aaacbba=1.

Referenced by [5], [6], [13], [16].

Overlap of [2] baa=c with [4] aaacbba=1:

Critical pair: b=cacbba.

Flip LHS and RHS.

Referenced by [8].

Overlap of [4] aaacbba=1 with [2] baa=c:

Critical pair: aaacbc=a.

Referenced by [7], [9], [11], [14], [17].

Overlap of [2] baa=c with [6] aaacbc=a:

Critical pair: ba=cacbc.

Flip LHS and RHS.

Referenced by [8].

Overlap of [7] cacbc=ba with [7] cacbc=ba:

Critical pair: cacbba=baacbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [6] aaacbc=a with [8] ccbc=b:

Critical pair: aaacbb=acbc.

Referenced by [13], [18].

Overlap of [8] ccbc=b with [3] bcaa=d:

Critical pair: ccd=baa.

Reduce RHS:

Referenced by [11], [12].

Overlap of [6] aaacbc=a with [10] ccd=c:

Critical pair: aaacbc=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [8] ccbc=b with [10] ccd=c:

Critical pair: ccbc=bcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14], [15].

Overlap of [4] aaacbba=1 with [11] acd=a:

Critical pair: aaacbba=cd.

Reduce LHS:

Referenced by [19].

Overlap of [6] aaacbc=a with [12] bcd=b:

Critical pair: aaacb=ad.

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

Overlap of [8] ccbc=b with [12] bcd=b:

Critical pair: ccb=bd.

Referenced by [23], [24], [25].

Overlap of [4] aaacbba=1 with [14] aaacb=ad:

Critical pair: adba=1.

Referenced by [19], [22].

Overlap of [6] aaacbc=a with [14] aaacb=ad:

Critical pair: adc=a.

Referenced by [20].

Overlap of [9] aaacbb=acbc with [14] aaacb=ad:

Critical pair: adb=acbc.

Flip LHS and RHS.

Referenced by [19].

Overlap of [13] acbca=cd with [18] acbc=adb:

Critical pair: adba=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [21], [29], [30], [31].

Overlap of [3] bcaa=d with [17] adc=a:

Critical pair: bcaa=ddc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [24].

Overlap of [19] cd=1 with [20] ddc=d:

Critical pair: cd=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [16] adba=1 with [16] adba=1:

Critical pair: adb=dba.

Defines rule #8.

Referenced by [27], [28].

Overlap of [15] ccb=bd with [2] baa=c:

Critical pair: ccc=bdaa.

Flip LHS and RHS.

Referenced by [27].

Overlap of [20] ddc=d with [15] ccb=bd:

Critical pair: ddbd=dcb.

Reduce RHS:

Referenced by [26].

Overlap of [21] dc=1 with [15] ccb=bd:

Critical pair: dbd=cb.

Flip LHS and RHS.

Defines rule #6.

Overlap of [24] ddbd=b with [21] dc=1:

Critical pair: ddb=bc.

Defines rule #7.

Overlap of [22] adb=dba with [23] bdaa=ccc:

Critical pair: adccc=dbadaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [22] adb=dba with [27] dbadaa=acc:

Critical pair: aacc=dbaadaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [29].

Overlap of [19] cd=1 with [28] daa=aacc:

Critical pair: caacc=aa.

Referenced by [30].

Overlap of [29] caacc=aa with [19] cd=1:

Critical pair: caac=aad.

Referenced by [31].

Overlap of [30] caac=aad with [19] cd=1:

Critical pair: caa=aadd.

Defines rule #4.