Certificate for #1070 ⟨a, b | aababa=aab⟩

Completion settings:

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

Axiom: aababa=aab.

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

Axiom: aabbbb=c.

Referenced by [4], [6], [10], [11], [12], [14].

Overlap of [1] aababa=aab with [1] aababa=aab:

Critical pair: aababaab=aabababa.

Reduce LHS:

Reduce RHS:

Referenced by [4], [5], [7], [8], [21], [22].

Overlap of [1] aababa=aab with [2] aabbbb=c:

Critical pair: aababc=aababbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [1] aababa=aab with [3] aabab=aabba:

Critical pair: aabbaa=aab.

Referenced by [6], [7], [8], [10], [13], [15], [23], [28].

Overlap of [5] aabbaa=aab with [2] aabbbb=c:

Critical pair: aabbc=aabbbbb.

Reduce RHS:

Referenced by [15], [19].

Overlap of [5] aabbaa=aab with [3] aabab=aabba:

Critical pair: aabbaabba=aabbab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [5] aabbaa=aab with [3] aabab=aabba:

Critical pair: aabbaaabba=aababab.

Reduce LHS:

Reduce RHS:

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

Overlap of [4] aabbabbb=aabbac with [7] aabbab=aabbba:

Critical pair: aabbbabb=aabbac.

Referenced by [29].

Overlap of [5] aabbaa=aab with [8] aabbbaa=aabb:

Critical pair: aabbaabb=aabbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [11], [12], [13], [14], [15], [16], [17], [25].

Overlap of [8] aabbbaa=aabb with [2] aabbbb=c:

Critical pair: aabbbc=aabbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19], [20], [21], [27].

Overlap of [8] aabbbaa=aabb with [2] aabbbb=c:

Critical pair: aabbbac=aabbabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25], [26], [31].

Overlap of [8] aabbbaa=aabb with [5] aabbaa=aab:

Critical pair: aabbbaab=aabbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [17], [30].

Overlap of [2] aabbbb=c with [10] aabbb=caa:

Critical pair: caab=c.

Referenced by [15], [17], [21], [22], [23], [30], [32].

Overlap of [5] aabbaa=aab with [10] aabbb=caa:

Critical pair: aabbcaa=aabbbb.

Reduce LHS:

Reduce RHS:

Referenced by [18].

Overlap of [8] aabbbaa=aabb with [10] aabbb=caa:

Critical pair: caaaa=aabb.

Flip LHS and RHS.

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

Overlap of [8] aabbbaa=aabb with [10] aabbb=caa:

Critical pair: aabbbcaa=aabbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18], [19], [21], [22], [23], [24].

Simplify [15] cbaa=c.

Reduce LHS:

Referenced by [19], [20], [21], [26].

Overlap of [6] aabbc=cb with [18] caacaaaa=c:

Critical pair: aabbc=cbaacaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20], [21], [22], [23], [24], [25], [30].

Overlap of [11] ccaa=caac with [18] caacaaaa=c:

Critical pair: cc=caaccaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [18] caacaaaa=c with [3] aabab=aabba:

Critical pair: caacaaaabba=cbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [14] caab=c with [3] aabab=aabba:

Critical pair: caabba=cab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25], [30], [33].

Overlap of [14] caab=c with [5] aabbaa=aab:

Critical pair: caab=cbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25], [26], [29], [30].

Simplify [17] cb=caacaa.

Reduce RHS:

Defines rule #7.

Overlap of [23] caaaacaa=c with [10] aabbb=caa:

Critical pair: caaaacacaa=cabbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [26], [27], [32].

Overlap of [23] caaaacaa=c with [18] caacaaaa=c:

Critical pair: caaaac=ccaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [32].

Overlap of [11] ccaa=caac with [25] cca=cac:

Critical pair: caca=caac.

Defines rule #2.

Referenced by [30], [31], [32].

Overlap of [5] aabbaa=aab with [16] aabb=caaaa:

Critical pair: caaaaaa=aab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [29], [30], [32].

Simplify [9] aabbbabb=aabbac.

Reduce RHS:

Referenced by [30].

Overlap of [29] aabbbabb=caaaaac with [28] aab=caaaaaa:

Critical pair: caaaaaabbabb=caaaaac.

Reduce LHS:

Defines rule #5.

Referenced by [32], [33].

Overlap of [12] cacaa=caaac with [27] caca=caac:

Critical pair: caaca=caaac.

Defines rule #3.

Referenced by [32].

Overlap of [14] caab=c with [28] aab=caaaaaa:

Critical pair: ccaaaaaa=c.

Reduce LHS:

Defines rule #6.

Simplify [22] cab=caaaaca.

Reduce RHS:

Defines rule #9.