Certificate for #14664 ⟨a, b | aaba=b, bbbbb=b⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = 0; deg(b) = 1

Axiom: aaba=b.

Referenced by [3], [4], [8], [9], [10], [11], [12], [13], [15], [16], [17], [18], [19], [20], [21], [22], [24], [25], [26], [27], [28], [29], [30], [31].

Axiom: bbbbb=b.

Defines rule #3.

Referenced by [5], [6], [23], [32].

Overlap of [1] aaba=b with [1] aaba=b:

Critical pair: aabb=baba.

Flip LHS and RHS.

Referenced by [4], [9], [25].

Overlap of [1] aaba=b with [3] baba=aabb:

Critical pair: aaaabb=bba.

Flip LHS and RHS.

Referenced by [5], [7], [10], [11], [12], [13], [15], [16], [17], [18], [19], [20], [21], [22], [25].

Overlap of [2] bbbbb=b with [4] bba=aaaabb:

Critical pair: bbbaaaabb=ba.

Reduce LHS:

Referenced by [6], [7].

Overlap of [5] baaaaaaaaaaaaaaaabbbb=ba with [2] bbbbb=b:

Critical pair: baaaaaaaaaaaaaaaab=bab.

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

Overlap of [5] baaaaaaaaaaaaaaaabbbb=ba with [4] bba=aaaabb:

Critical pair: baaaaaaaaaaaaaaaabbaaaabb=baa.

Reduce LHS:

Referenced by [14].

Overlap of [1] aaba=b with [6] baaaaaaaaaaaaaaaab=bab:

Critical pair: aabab=baaaaaaaaaaaaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [6] baaaaaaaaaaaaaaaab=bab with [1] aaba=b:

Critical pair: baaaaaaaaaaaaaab=baba.

Reduce RHS:

Referenced by [11], [15], [19].

Overlap of [8] baaaaaaaaaaaaaaab=bb with [1] aaba=b:

Critical pair: baaaaaaaaaaaaab=bba.

Reduce RHS:

Referenced by [12], [13], [18].

Overlap of [9] baaaaaaaaaaaaaab=aabb with [1] aaba=b:

Critical pair: baaaaaaaaaaaab=aabba.

Reduce RHS:

Referenced by [17], [21].

Overlap of [10] baaaaaaaaaaaaab=aaaabb with [1] aaba=b:

Critical pair: baaaaaaaaaaab=aaaabba.

Reduce RHS:

Referenced by [16], [20].

Overlap of [10] baaaaaaaaaaaaab=aaaabb with [4] bba=aaaabb:

Critical pair: baaaaaaaaaaaaaaaaabb=aaaabbba.

Reduce RHS:

Referenced by [14].

Overlap of [7] baaaaaaaaaaaaaaaaabbbb=baa with [13] baaaaaaaaaaaaaaaaabb=baabb:

Critical pair: baabbbb=baa.

Referenced by [15].

Overlap of [14] baabbbb=baa with [4] bba=aaaabb:

Critical pair: baabbaaaabb=baaa.

Reduce LHS:

Referenced by [16].

Overlap of [15] baaabbbb=baaa with [4] bba=aaaabb:

Critical pair: baaabbaaaabb=baaaa.

Reduce LHS:

Referenced by [17].

Overlap of [16] baaaabbbb=baaaa with [4] bba=aaaabb:

Critical pair: baaaabbaaaabb=baaaaa.

Reduce LHS:

Referenced by [18].

Overlap of [17] baaaaabbbb=baaaaa with [4] bba=aaaabb:

Critical pair: baaaaabbaaaabb=baaaaaa.

Reduce LHS:

Referenced by [19].

Overlap of [18] baaaaaabbbb=baaaaaa with [4] bba=aaaabb:

Critical pair: baaaaaabbaaaabb=baaaaaaa.

Reduce LHS:

Referenced by [20].

Overlap of [19] baaaaaaabbbb=baaaaaaa with [4] bba=aaaabb:

Critical pair: baaaaaaabbaaaabb=baaaaaaaa.

Reduce LHS:

Referenced by [23].

Overlap of [11] baaaaaaaaaaaab=aaaaaabb with [1] aaba=b:

Critical pair: baaaaaaaaaab=aaaaaabba.

Reduce RHS:

Referenced by [22].

Overlap of [21] baaaaaaaaaab=aaaaaaaaaabb with [1] aaba=b:

Critical pair: baaaaaaaab=aaaaaaaaaabba.

Reduce RHS:

Referenced by [23].

Overlap of [20] baaaaaaaabbbb=baaaaaaaa with [22] baaaaaaaab=aaaaaaaaaaaaaabb:

Critical pair: aaaaaaaaaaaaaabbbbb=baaaaaaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [25].

Overlap of [1] aaba=b with [23] baaaaaaaa=aaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaab=baaaaaaa.

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [3] baba=aabb with [23] baaaaaaaa=aaaaaaaaaaaaaab:

Critical pair: baaaaaaaaaaaaaaab=aabbaaaaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [1] aaba=b with [24] baaaaaaa=aaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaab=baaaaaa.

Flip LHS and RHS.

Referenced by [27].

Overlap of [1] aaba=b with [26] baaaaaa=aaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaab=baaaaa.

Flip LHS and RHS.

Referenced by [28].

Overlap of [1] aaba=b with [27] baaaaa=aaaaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaab=baaaa.

Flip LHS and RHS.

Referenced by [29].

Overlap of [1] aaba=b with [28] baaaa=aaaaaaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaab=baaa.

Flip LHS and RHS.

Referenced by [30].

Overlap of [1] aaba=b with [29] baaa=aaaaaaaaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaab=baa.

Flip LHS and RHS.

Referenced by [31].

Overlap of [1] aaba=b with [30] baa=aaaaaaaaaaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaab=ba.

Flip LHS and RHS.

Defines rule #2.

Overlap of [25] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb=bb with [2] bbbbb=b:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaab=bbbbb.

Reduce RHS:

Defines rule #1.