Certificate for #851 ⟨a, b | ababbaab=a⟩

Completion settings:

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

Axiom: ababbaab=a.

Referenced by [3].

Axiom: babbaa=c.

Defines rule #16.

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

Overlap of [1] ababbaab=a with [2] babbaa=c:

Critical pair: acb=a.

Defines rule #6.

Referenced by [4], [5], [8], [11], [13], [15], [17], [20], [22], [24], [26].

Overlap of [2] babbaa=c with [3] acb=a:

Critical pair: babbaa=ccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [8], [9], [10], [12], [15], [16], [18], [19], [23], [25], [27].

Overlap of [3] acb=a with [2] babbaa=c:

Critical pair: acc=aabbaa.

Flip LHS and RHS.

Defines rule #22.

Referenced by [7], [8], [9], [11], [15], [21].

Overlap of [4] ccb=c with [2] babbaa=c:

Critical pair: ccc=cabbaa.

Flip LHS and RHS.

Referenced by [9], [11], [13], [20].

Overlap of [2] babbaa=c with [5] aabbaa=acc:

Critical pair: babbacc=cbbaa.

Defines rule #12.

Referenced by [25].

Overlap of [5] aabbaa=acc with [5] aabbaa=acc:

Critical pair: aabbacc=accbbaa.

Reduce RHS:

Defines rule #19.

Referenced by [14], [15], [16], [21].

Overlap of [6] cabbaa=ccc with [5] aabbaa=acc:

Critical pair: cabbacc=cccbbaa.

Reduce RHS:

Referenced by [10].

Overlap of [9] cabbacc=caa with [4] ccb=c:

Critical pair: cabbac=caab.

Flip LHS and RHS.

Referenced by [11], [24].

Overlap of [10] caab=cabbac with [5] aabbaa=acc:

Critical pair: cacc=cabbacbaa.

Reduce RHS:

Defines rule #3.

Referenced by [12].

Overlap of [11] cacc=ccca with [4] ccb=c:

Critical pair: cac=cccab.

Flip LHS and RHS.

Referenced by [13].

Overlap of [12] cccab=cac with [6] cabbaa=ccc:

Critical pair: ccccc=cacbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [2] babbaa=c with [8] aabbacc=aaa:

Critical pair: babbaaa=cbbacc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [5] aabbaa=acc with [8] aabbacc=aaa:

Critical pair: aabbaaa=accbbacc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [21].

Overlap of [8] aabbacc=aaa with [4] ccb=c:

Critical pair: aabbac=aaab.

Flip LHS and RHS.

Defines rule #17.

Overlap of [3] acb=a with [14] cbbacc=ca:

Critical pair: aca=abacc.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] ccb=c with [14] cbbacc=ca:

Critical pair: cca=cbacc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [14] cbbacc=ca with [4] ccb=c:

Critical pair: cbbac=cab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [20], [24].

Overlap of [6] cabbaa=ccc with [19] cab=cbbac:

Critical pair: cbbacbaa=ccc.

Reduce LHS:

Defines rule #15.

Referenced by [22], [23].

Overlap of [5] aabbaa=acc with [15] aacc=acca:

Critical pair: aabbacca=acccc.

Reduce LHS:

Defines rule #20.

Overlap of [3] acb=a with [20] cbbaaa=ccc:

Critical pair: accc=abaaa.

Flip LHS and RHS.

Defines rule #21.

Overlap of [4] ccb=c with [20] cbbaaa=ccc:

Critical pair: cccc=cbaaa.

Flip LHS and RHS.

Defines rule #14.

Simplify [10] caab=cabbac.

Reduce RHS:

Defines rule #7.

Overlap of [7] babbacc=cbbaa with [4] ccb=c:

Critical pair: babbac=cbbaab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [26], [27].

Overlap of [3] acb=a with [25] cbbaab=babbac:

Critical pair: ababbac=abaab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [4] ccb=c with [25] cbbaab=babbac:

Critical pair: cbabbac=cbaab.

Flip LHS and RHS.

Defines rule #8.