Certificate for #7548 ⟨a, b | aaa=1, bbabbb=a⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #3.

Referenced by [5], [6], [8], [10], [13], [14], [18], [19], [20], [21], [25], [27].

Axiom: bbabbb=a.

Referenced by [3], [4], [7], [8], [9], [11], [15], [17], [22], [24], [25], [26].

Overlap of [2] bbabbb=a with [2] bbabbb=a:

Critical pair: bbaba=aabbb.

Referenced by [5], [10], [17], [22], [24], [25].

Overlap of [2] bbabbb=a with [2] bbabbb=a:

Critical pair: bbabba=ababbb.

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

Overlap of [3] bbaba=aabbb with [1] aaa=1:

Critical pair: bbab=aabbbaa.

Flip LHS and RHS.

Referenced by [6], [7].

Overlap of [1] aaa=1 with [5] aabbbaa=bbab:

Critical pair: abbab=bbbaa.

Flip LHS and RHS.

Referenced by [8].

Overlap of [5] aabbbaa=bbab with [5] aabbbaa=bbab:

Critical pair: aabbbbbab=bbabbbbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11], [16].

Overlap of [2] bbabbb=a with [6] bbbaa=abbab:

Critical pair: bbaabbab=aaa.

Reduce RHS:

Referenced by [12].

Overlap of [4] bbabba=ababbb with [2] bbabbb=a:

Critical pair: bbaa=ababbbbbb.

Referenced by [11], [12], [13], [22], [25].

Overlap of [4] bbabba=ababbb with [3] bbaba=aabbb:

Critical pair: bbaaabbb=ababbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [2] bbabbb=a with [9] bbaa=ababbbbbb:

Critical pair: bbabbababbbbbb=abaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [8] bbaabbab=1 with [9] bbaa=ababbbbbb:

Critical pair: ababbbbbbbbab=1.

Referenced by [25].

Overlap of [9] bbaa=ababbbbbb with [1] aaa=1:

Critical pair: bb=ababbbbbba.

Flip LHS and RHS.

Referenced by [14].

Overlap of [1] aaa=1 with [13] ababbbbbba=bb:

Critical pair: aabb=babbbbbba.

Flip LHS and RHS.

Referenced by [15].

Overlap of [2] bbabbb=a with [14] babbbbbba=aabb:

Critical pair: baabb=abbba.

Referenced by [17], [19].

Simplify [7] abaa=aabbbbbab.

Reduce RHS:

Referenced by [18].

Overlap of [15] baabb=abbba with [2] bbabbb=a:

Critical pair: baaba=abbbababbb.

Reduce RHS:

Referenced by [18], [19], [20].

Overlap of [17] baaba=aabab with [1] aaa=1:

Critical pair: baab=aababaa.

Reduce RHS:

Referenced by [25].

Overlap of [17] baaba=aabab with [15] baabb=abbba:

Critical pair: baaabbba=aabababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [17] baaba=aabab with [17] baaba=aabab:

Critical pair: baaaabab=aabababa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [1] aaa=1 with [19] aabababb=bbbba:

Critical pair: abbbba=bababb.

Flip LHS and RHS.

Referenced by [23].

Overlap of [19] aabababb=bbbba with [2] bbabbb=a:

Critical pair: aabababa=bbbbababbb.

Reduce LHS:

Reduce RHS:

Referenced by [23].

Simplify [21] bababb=abbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [2] bbabbb=a with [23] abbbba=ababbbbbbbbbbbbb:

Critical pair: bbababbbbbbbbbbbbb=aba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [18] baab=aabbbbbbbbbbbb with [12] ababbbbbbbbab=1:

Critical pair: ba=aabbbbbbbbbbbbabbbbbbbbab.

Reduce RHS:

Defines rule #2.

Referenced by [26].

Overlap of [2] bbabbb=a with [25] ba=abbbbbbbbbbbbbbbb:

Critical pair: bbabbabbbbbbbbbbbbbbbb=aa.

Reduce LHS:

Referenced by [27].

Overlap of [1] aaa=1 with [26] aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aa:

Critical pair: aaa=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.