Certificate for #4192 ⟨a, b | aabbbaaab=ba⟩

Completion settings:

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

Axiom: aabbbaaab=ba.

Referenced by [4].

Axiom: aab=c.

Defines rule #18.

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

Axiom: bbbac=d.

Referenced by [5], [11].

Overlap of [1] aabbbaaab=ba with [2] aab=c:

Critical pair: cbbaaab=ba.

Reduce LHS:

Referenced by [5], [8].

Overlap of [2] aab=c with [3] bbbac=d:

Critical pair: aad=cbbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [6], [7], [8], [11], [12].

Overlap of [2] aab=c with [5] ba=aad:

Critical pair: aaaad=ca.

Defines rule #2.

Referenced by [10], [24].

Overlap of [5] ba=aad with [2] aab=c:

Critical pair: bc=aadab.

Defines rule #20.

Simplify [4] cbbac=ba.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [9], [14], [20].

Overlap of [8] caadadc=aad with [8] caadadc=aad:

Critical pair: caadadaad=aadaadadc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [10].

Overlap of [6] aaaad=ca with [9] aadaadadc=caadadaad:

Critical pair: aacaadadaad=caaadadc.

Defines rule #8.

Referenced by [13], [15], [18].

Overlap of [3] bbbac=d with [5] ba=aad:

Critical pair: bbaadc=d.

Reduce LHS:

Defines rule #3.

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

Overlap of [5] ba=aad with [11] aadadadc=d:

Critical pair: bd=aadadadadc.

Defines rule #19.

Overlap of [10] aacaadadaad=caaadadc with [11] aadadadc=d:

Critical pair: aacaadadd=caaadadcadadc.

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [11] aadadadc=d with [8] caadadc=aad:

Critical pair: aadadadaad=daadadc.

Defines rule #6.

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

Overlap of [10] aacaadadaad=caaadadc with [14] aadadadaad=daadadc:

Critical pair: aacaadaddaadadc=caaadadcadadaad.

Defines rule #11.

Overlap of [14] aadadadaad=daadadc with [11] aadadadc=d:

Critical pair: aadadadd=daadadcadadc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [18], [19], [23].

Overlap of [14] aadadadaad=daadadc with [14] aadadadaad=daadadc:

Critical pair: aadadaddaadadc=daadadcadadaad.

Defines rule #9.

Overlap of [10] aacaadadaad=caaadadc with [16] daadadcadadc=aadadadd:

Critical pair: aacaadaaadadadd=caaadadcadcadadc.

Defines rule #14.

Overlap of [14] aadadadaad=daadadc with [16] daadadcadadc=aadadadd:

Critical pair: aadadaaadadadd=daadadcadcadadc.

Defines rule #10.

Overlap of [8] caadadc=aad with [13] caaadadcadadc=aacaadadd:

Critical pair: caadadaacaadadd=aadaaadadcadadc.

Flip LHS and RHS.

Defines rule #12.

Referenced by [24].

Overlap of [11] aadadadc=d with [13] caaadadcadadc=aacaadadd:

Critical pair: aadadadaacaadadd=daaadadcadadc.

Defines rule #13.

Overlap of [13] caaadadcadadc=aacaadadd with [13] caaadadcadadc=aacaadadd:

Critical pair: caaadadcadadaacaadadd=aacaadaddaaadadcadadc.

Flip LHS and RHS.

Defines rule #17.

Overlap of [16] daadadcadadc=aadadadd with [13] caaadadcadadc=aacaadadd:

Critical pair: daadadcadadaacaadadd=aadadaddaaadadcadadc.

Flip LHS and RHS.

Defines rule #16.

Overlap of [6] aaaad=ca with [20] aadaaadadcadadc=caadadaacaadadd:

Critical pair: aacaadadaacaadadd=caaaadadcadadc.

Reduce RHS:

Defines rule #15.