Certificate for #4779 ⟨a, b | abaaabba=baa⟩

Completion settings:

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

Axiom: abaaabba=baa.

Referenced by [4].

Axiom: aabb=c.

Defines rule #12.

Referenced by [4], [6], [7], [8], [9], [10], [15], [22].

Axiom: abac=d.

Referenced by [4], [5], [17].

Overlap of [1] abaaabba=baa with [2] aabb=c:

Critical pair: abaca=baa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [4] baa=da with [3] abac=d:

Critical pair: bad=dabac.

Reduce RHS:

Defines rule #6.

Referenced by [7], [11], [13], [18].

Overlap of [2] aabb=c with [4] baa=da:

Critical pair: aabda=caa.

Referenced by [27].

Overlap of [2] aabb=c with [5] bad=dd:

Critical pair: aabdd=cad.

Referenced by [28].

Overlap of [4] baa=da with [2] aabb=c:

Critical pair: bc=dabb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [11], [12], [13], [14], [16], [19], [20], [25].

Overlap of [4] baa=da with [2] aabb=c:

Critical pair: bac=daabb.

Reduce RHS:

Defines rule #11.

Referenced by [10], [14], [17].

Overlap of [2] aabb=c with [9] bac=dc:

Critical pair: aabdc=cac.

Referenced by [29].

Overlap of [5] bad=dd with [8] dabb=bc:

Critical pair: babc=ddabb.

Reduce RHS:

Defines rule #18.

Referenced by [15], [16].

Overlap of [8] dabb=bc with [4] baa=da:

Critical pair: dabda=bcaa.

Flip LHS and RHS.

Referenced by [21].

Overlap of [8] dabb=bc with [5] bad=dd:

Critical pair: dabdd=bcad.

Flip LHS and RHS.

Referenced by [23].

Overlap of [8] dabb=bc with [9] bac=dc:

Critical pair: dabdc=bcac.

Flip LHS and RHS.

Referenced by [24].

Overlap of [2] aabb=c with [11] babc=dbc:

Critical pair: aabdbc=cabc.

Referenced by [26].

Overlap of [8] dabb=bc with [11] babc=dbc:

Critical pair: dabdbc=bcabc.

Flip LHS and RHS.

Referenced by [30].

Overlap of [3] abac=d with [9] bac=dc:

Critical pair: adc=d.

Defines rule #1.

Referenced by [18].

Overlap of [5] bad=dd with [17] adc=d:

Critical pair: bd=ddc.

Defines rule #4.

Referenced by [19], [20], [21], [23], [24], [25], [26], [27], [28], [29], [30].

Overlap of [8] dabb=bc with [18] bd=ddc:

Critical pair: dabddc=bcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [18] bd=ddc with [8] dabb=bc:

Critical pair: bbc=ddcabb.

Defines rule #17.

Referenced by [25].

Simplify [12] bcaa=dabda.

Reduce RHS:

Defines rule #9.

Referenced by [22].

Overlap of [21] bcaa=daddca with [2] aabb=c:

Critical pair: bcc=daddcabb.

Defines rule #15.

Simplify [13] bcad=dabdd.

Reduce RHS:

Defines rule #10.

Simplify [14] bcac=dabdc.

Reduce RHS:

Defines rule #16.

Overlap of [8] dabb=bc with [20] bbc=ddcabb:

Critical pair: dabddcabb=bcbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Simplify [15] aabdbc=cabc.

Reduce LHS:

Defines rule #14.

Overlap of [6] aabda=caa with [18] bd=ddc:

Critical pair: aaddca=caa.

Defines rule #2.

Overlap of [7] aabdd=cad with [18] bd=ddc:

Critical pair: aaddcd=cad.

Defines rule #3.

Overlap of [10] aabdc=cac with [18] bd=ddc:

Critical pair: aaddcc=cac.

Defines rule #7.

Simplify [16] bcabc=dabdbc.

Reduce RHS:

Defines rule #20.