Certificate for #5852 ⟨a, b | abaaba=abbab⟩

Completion settings:

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

Axiom: abaaba=abbab.

Referenced by [3].

Axiom: aba=c.

Defines rule #12.

Referenced by [3], [4], [5], [6], [8], [12], [17].

Overlap of [1] abaaba=abbab with [2] aba=c:

Critical pair: caba=abbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

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

Overlap of [2] aba=c with [2] aba=c:

Critical pair: abc=cba.

Defines rule #1.

Referenced by [5], [8], [10], [13], [15], [18].

Overlap of [2] aba=c with [3] abbab=cc:

Critical pair: abcc=cbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [3] abbab=cc with [2] aba=c:

Critical pair: abbc=cca.

Defines rule #10.

Referenced by [7], [8], [9], [11], [14], [16], [19], [20], [21].

Overlap of [3] abbab=cc with [3] abbab=cc:

Critical pair: abbcc=ccbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [15], [16], [22], [23].

Overlap of [2] aba=c with [6] abbc=cca:

Critical pair: abcca=cbbc.

Reduce LHS:

Defines rule #9.

Referenced by [10], [15], [17], [18], [19].

Overlap of [3] abbab=cc with [6] abbc=cca:

Critical pair: abbcca=ccbc.

Reduce LHS:

Defines rule #3.

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

Overlap of [4] abc=cba with [9] ccaca=ccbc:

Critical pair: abccbc=cbacaca.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Overlap of [6] abbc=cca with [9] ccaca=ccbc:

Critical pair: abbccbc=ccacaca.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Overlap of [9] ccaca=ccbc with [2] aba=c:

Critical pair: ccacc=ccbcba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [20].

Overlap of [9] ccaca=ccbc with [4] abc=cba:

Critical pair: ccaccba=ccbcbc.

Defines rule #13.

Referenced by [22].

Overlap of [9] ccaca=ccbc with [6] abbc=cca:

Critical pair: ccaccca=ccbcbbc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [4] abc=cba with [7] ccbab=ccac:

Critical pair: abccac=cbacbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [6] abbc=cca with [7] ccbab=ccac:

Critical pair: abbccac=ccacbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [8] cbaca=cbbc with [2] aba=c:

Critical pair: cbacc=cbbcba.

Flip LHS and RHS.

Defines rule #16.

Referenced by [21].

Overlap of [8] cbaca=cbbc with [4] abc=cba:

Critical pair: cbaccba=cbbcbc.

Defines rule #19.

Referenced by [23].

Overlap of [8] cbaca=cbbc with [6] abbc=cca:

Critical pair: cbaccca=cbbcbbc.

Flip LHS and RHS.

Defines rule #14.

Overlap of [12] ccbcba=ccacc with [6] abbc=cca:

Critical pair: ccbcbcca=ccaccbbc.

Flip LHS and RHS.

Defines rule #11.

Overlap of [17] cbbcba=cbacc with [6] abbc=cca:

Critical pair: cbbcbcca=cbaccbbc.

Flip LHS and RHS.

Defines rule #18.

Overlap of [13] ccaccba=ccbcbc with [7] ccbab=ccac:

Critical pair: ccaccac=ccbcbcb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [18] cbaccba=cbbcbc with [7] ccbab=ccac:

Critical pair: cbaccac=cbbcbcb.

Flip LHS and RHS.

Defines rule #15.