Certificate for #71 ⟨a, b | ababba=1⟩

Completion settings:

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

Axiom: ababba=1.

Referenced by [4].

Axiom: ba=c.

Defines rule #5.

Referenced by [4], [5], [7], [10].

Axiom: bca=d.

Referenced by [6], [15].

Overlap of [1] ababba=1 with [2] ba=c:

Critical pair: acbba=1.

Reduce LHS:

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

Overlap of [2] ba=c with [4] acbc=1:

Critical pair: b=ccbc.

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] acbc=1 with [3] bca=d:

Critical pair: acd=a.

Referenced by [7].

Overlap of [2] ba=c with [6] acd=a:

Critical pair: ba=ccd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8].

Overlap of [4] acbc=1 with [7] ccd=c:

Critical pair: acbc=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

Overlap of [4] acbc=1 with [8] cd=1:

Critical pair: acb=d.

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

Overlap of [2] ba=c with [9] acb=d:

Critical pair: bd=ccb.

Defines rule #3.

Overlap of [4] acbc=1 with [9] acb=d:

Critical pair: dc=1.

Defines rule #2.

Referenced by [12], [13], [14], [16], [17].

Overlap of [11] dc=1 with [5] ccbc=b:

Critical pair: db=cbc.

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [9] acb=d with [12] cbc=db:

Critical pair: adb=dc.

Reduce RHS:

Defines rule #8.

Referenced by [15].

Overlap of [11] dc=1 with [12] cbc=db:

Critical pair: ddb=bc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [13] adb=1 with [3] bca=d:

Critical pair: add=ca.

Defines rule #7.

Referenced by [16].

Overlap of [15] add=ca with [11] dc=1:

Critical pair: ad=cac.

Flip LHS and RHS.

Referenced by [17].

Overlap of [11] dc=1 with [16] cac=ad:

Critical pair: dad=ac.

Flip LHS and RHS.

Defines rule #6.