Certificate for #2044 ⟨a, b | abaabbab=ba⟩

Completion settings:

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

Axiom: abaabbab=ba.

Referenced by [3].

Axiom: baa=c.

Defines rule #5.

Referenced by [3], [4], [5], [6], [9], [10].

Overlap of [1] abaabbab=ba with [2] baa=c:

Critical pair: acbbab=ba.

Defines rule #2.

Referenced by [4], [5], [7], [9], [11], [18].

Overlap of [2] baa=c with [3] acbbab=ba:

Critical pair: baba=ccbbab.

Defines rule #6.

Referenced by [9], [10], [11], [12], [13], [14], [16].

Overlap of [3] acbbab=ba with [2] baa=c:

Critical pair: acbbac=baaa.

Reduce RHS:

Defines rule #3.

Referenced by [6], [7], [8], [13], [15], [17], [19].

Overlap of [2] baa=c with [5] acbbac=ca:

Critical pair: baca=ccbbac.

Defines rule #7.

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

Overlap of [5] acbbac=ca with [3] acbbab=ba:

Critical pair: acbbba=cabbab.

Flip LHS and RHS.

Defines rule #9.

Overlap of [5] acbbac=ca with [5] acbbac=ca:

Critical pair: acbbca=cabbac.

Flip LHS and RHS.

Defines rule #10.

Overlap of [3] acbbab=ba with [4] baba=ccbbab:

Critical pair: acbccbbab=baa.

Reduce RHS:

Defines rule #4.

Referenced by [14], [15].

Overlap of [4] baba=ccbbab with [2] baa=c:

Critical pair: bac=ccbbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [4] baba=ccbbab with [3] acbbab=ba:

Critical pair: babba=ccbbabcbbab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [4] baba=ccbbab with [4] baba=ccbbab:

Critical pair: baccbbab=ccbbabba.

Flip LHS and RHS.

Defines rule #12.

Overlap of [4] baba=ccbbab with [5] acbbac=ca:

Critical pair: babca=ccbbabcbbac.

Flip LHS and RHS.

Defines rule #15.

Overlap of [4] baba=ccbbab with [9] acbccbbab=c:

Critical pair: babc=ccbbabcbccbbab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [5] acbbac=ca with [9] acbccbbab=c:

Critical pair: acbbc=cabccbbab.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] baba=ccbbab with [6] baca=ccbbac:

Critical pair: baccbbac=ccbbabca.

Flip LHS and RHS.

Defines rule #13.

Overlap of [5] acbbac=ca with [6] baca=ccbbac:

Critical pair: acbccbbac=caa.

Flip LHS and RHS.

Defines rule #8.

Overlap of [6] baca=ccbbac with [3] acbbab=ba:

Critical pair: bacba=ccbbaccbbab.

Flip LHS and RHS.

Defines rule #16.

Overlap of [6] baca=ccbbac with [5] acbbac=ca:

Critical pair: bacca=ccbbaccbbac.

Flip LHS and RHS.

Defines rule #17.