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

Completion settings:

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

Axiom: aababa=aab.

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

Axiom: aabbbb=c.

Referenced by [4], [6], [11], [12], [13], [17].

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

Critical pair: aababaab=aabababa.

Reduce LHS:

Reduce RHS:

Referenced by [4], [5], [7], [8], [23].

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

Critical pair: aababc=aababbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [10].

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

Critical pair: aabbaa=aab.

Referenced by [6], [7], [8], [9], [11], [14], [18], [24].

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

Critical pair: aabbc=aabbbbb.

Reduce RHS:

Referenced by [9], [15], [18], [22], [25].

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

Critical pair: aabbaabba=aabbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [10], [13].

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

Critical pair: aabbaaabba=aababab.

Reduce LHS:

Reduce RHS:

Referenced by [11], [12], [13], [14], [15], [19], [20].

Overlap of [5] aabbaa=aab with [6] aabbc=cb:

Critical pair: aabbcb=aabbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26], [27].

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

Critical pair: aabbbabb=aabbac.

Referenced by [28].

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

Critical pair: aabbaabb=aabbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [12], [13], [14], [15], [17], [18], [19], [20].

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

Critical pair: aabbbc=aabbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [20], [26], [27].

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

Critical pair: aabbbac=aabbabbbb.

Reduce LHS:

Reduce RHS:

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

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

Critical pair: aabbbaab=aabbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [20], [26], [27], [29].

Overlap of [8] aabbbaa=aabb with [6] aabbc=cb:

Critical pair: aabbbcb=aabbbbc.

Reduce LHS:

Reduce RHS:

Referenced by [26], [27].

Overlap of [12] caac=ccaa with [12] caac=ccaa:

Critical pair: caaccaa=ccaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

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

Critical pair: caab=c.

Referenced by [18], [20], [23], [26], [27], [29].

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

Critical pair: aabbcaa=aabbbb.

Reduce LHS:

Reduce RHS:

Referenced by [21].

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

Critical pair: caaaa=aabb.

Flip LHS and RHS.

Referenced by [20], [22], [24].

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

Critical pair: aabbbcaa=aabbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [21], [22], [23], [25], [26], [27].

Simplify [18] cbaa=c.

Reduce LHS:

Defines rule #6.

Referenced by [22], [25], [26], [27], [28], [29].

Overlap of [6] aabbc=cb with [21] ccaaaaaa=c:

Critical pair: aabbc=cbcaaaaaa.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [25], [26], [27], [28], [29].

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

Critical pair: caabba=cab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [27].

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

Critical pair: caaaaaa=aab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [25], [26], [27], [28], [29].

Overlap of [6] aabbc=cb with [13] caaac=cacaa:

Critical pair: aabbcacaa=cbaaac.

Reduce LHS:

Reduce RHS:

Referenced by [30].

Overlap of [9] aabbbc=cbb with [13] caaac=cacaa:

Critical pair: aabbbcacaa=cbbaaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [9] aabbbc=cbb with [23] cab=ccaaaaa:

Critical pair: aabbbccaaaaa=cbbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Simplify [10] aabbbabb=aabbac.

Reduce RHS:

Referenced by [29].

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

Critical pair: caaaaaabbabb=caaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [25] ccaaaaacaa=cac with [26] ccaaaaac=ccacaaaa:

Critical pair: ccacaaaaaa=cac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [31], [32].

Simplify [29] caaaaac=cacaaaa.

Reduce RHS:

Defines rule #5.

Simplify [13] caaac=cacaa.

Reduce RHS:

Defines rule #3.