Certificate for #4000 ⟨a, b | aaababbaa=ba⟩

Completion settings:

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

Axiom: aaababbaa=ba.

Referenced by [3].

Axiom: bba=c.

Defines rule #4.

Referenced by [3], [4], [5], [13].

Overlap of [1] aaababbaa=ba with [2] bba=c:

Critical pair: aaabaca=ba.

Defines rule #1.

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

Overlap of [2] bba=c with [3] aaabaca=ba:

Critical pair: bbba=caabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7], [8], [10], [12], [14].

Overlap of [3] aaabaca=ba with [3] aaabaca=ba:

Critical pair: aaabacba=baaabaca.

Reduce RHS:

Defines rule #5.

Referenced by [9], [10], [11].

Overlap of [3] aaabaca=ba with [4] caabaca=bc:

Critical pair: aaababc=baabaca.

Flip LHS and RHS.

Defines rule #8.

Referenced by [13].

Overlap of [4] caabaca=bc with [3] aaabaca=ba:

Critical pair: caabacba=bcaabaca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [4] caabaca=bc with [4] caabaca=bc:

Critical pair: caababc=bcabaca.

Flip LHS and RHS.

Defines rule #9.

Overlap of [3] aaabaca=ba with [5] aaabacba=c:

Critical pair: aaabacc=baaabacba.

Reduce RHS:

Defines rule #3.

Referenced by [12].

Overlap of [4] caabaca=bc with [5] aaabacba=c:

Critical pair: caabacc=bcaabacba.

Flip LHS and RHS.

Defines rule #11.

Overlap of [5] aaabacba=c with [5] aaabacba=c:

Critical pair: aaabacbc=caabacba.

Defines rule #7.

Referenced by [14].

Overlap of [4] caabaca=bc with [9] aaabacc=bc:

Critical pair: caabacbc=bcaabacc.

Flip LHS and RHS.

Defines rule #10.

Overlap of [2] bba=c with [6] baabaca=aaababc:

Critical pair: baaababc=cabaca.

Defines rule #12.

Overlap of [4] caabaca=bc with [11] aaabacbc=caabacba:

Critical pair: caabaccaabacba=bcaabacbc.

Flip LHS and RHS.

Defines rule #13.