Certificate for #7529 ⟨a, b | aaa=1, abbbba=b⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #10.

Referenced by [3], [4].

Axiom: abbbba=b.

Defines rule #6.

Referenced by [3], [4], [5], [6], [7], [13], [18].

Overlap of [1] aaa=1 with [2] abbbba=b:

Critical pair: aab=bbbba.

Defines rule #4.

Referenced by [6], [8], [14], [17].

Overlap of [2] abbbba=b with [1] aaa=1:

Critical pair: abbbb=baa.

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [2] abbbba=b with [2] abbbba=b:

Critical pair: abbbbb=bbbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [9], [11], [12], [14], [16], [17], [19].

Overlap of [3] aab=bbbba with [2] abbbba=b:

Critical pair: ab=bbbbabbba.

Flip LHS and RHS.

Referenced by [10], [18].

Overlap of [2] abbbba=b with [4] baa=abbbb:

Critical pair: abbbabbbb=ba.

Referenced by [8], [9], [10], [11], [12], [15], [20].

Overlap of [3] aab=bbbba with [7] abbbabbbb=ba:

Critical pair: aba=bbbbabbabbbb.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] baa=abbbb with [7] abbbabbbb=ba:

Critical pair: baba=abbbbbbbabbbb.

Reduce RHS:

Defines rule #8.

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

Overlap of [7] abbbabbbb=ba with [6] bbbbabbba=ab:

Critical pair: abbbabbab=babbabbba.

Flip LHS and RHS.

Referenced by [13], [14], [15].

Overlap of [7] abbbabbbb=ba with [5] bbbbba=abbbbb:

Critical pair: abbbababbbbb=babba.

Reduce LHS:

Referenced by [22].

Overlap of [7] abbbabbbb=ba with [5] bbbbba=abbbbb:

Critical pair: abbbabbabbbbb=babbba.

Referenced by [15], [16].

Overlap of [2] abbbba=b with [10] babbabbba=abbbabbab:

Critical pair: abbbabbbabbab=bbbabbba.

Referenced by [17].

Overlap of [10] babbabbba=abbbabbab with [4] baa=abbbb:

Critical pair: babbabbabbbb=abbbabbaba.

Reduce RHS:

Referenced by [15].

Overlap of [10] babbabbba=abbbabbab with [9] baba=abbabbbbbbbbb:

Critical pair: babbabbabbabbbbbbbbb=abbbabbabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [12] abbbabbabbbbb=babbba with [5] bbbbba=abbbbb:

Critical pair: abbbabbabbabbbbb=babbbabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Simplify [13] abbbabbbabbab=bbbabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [6] bbbbabbba=ab with [17] bbbabbba=bbbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

Critical pair: bbbbabbbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=abbbba.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [19].

Overlap of [18] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=b with [5] bbbbba=abbbbb:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbabbbbb=ba.

Reduce LHS:

Defines rule #2.

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

Overlap of [7] abbbabbbb=ba with [19] babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ba:

Critical pair: abbba=babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #5.

Overlap of [8] bbbbabbabbbb=aba with [19] babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ba:

Critical pair: bbbbabba=ababbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #9.

Overlap of [11] abbabbabbbbbbbbbbbbbb=babba with [19] babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ba:

Critical pair: abbabba=babbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #11.