Certificate for #14354 ⟨a, b | aaaa=a, abbba=b⟩

Completion settings:

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

Axiom: aaaa=a.

Defines rule #9.

Referenced by [3], [4].

Axiom: abbba=b.

Defines rule #6.

Referenced by [3], [4], [5], [6], [7], [8], [9], [17].

Overlap of [1] aaaa=a with [2] abbba=b:

Critical pair: aaab=abbba.

Reduce RHS:

Referenced by [6], [14].

Overlap of [2] abbba=b with [1] aaaa=a:

Critical pair: abbba=baaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7].

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

Critical pair: abbbb=bbbba.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [3] aaab=b with [2] abbba=b:

Critical pair: aab=bbba.

Defines rule #4.

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

Overlap of [2] abbba=b with [4] baaa=b:

Critical pair: abbb=baa.

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [6] aab=bbba with [2] abbba=b:

Critical pair: ab=bbbabba.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [2] abbba=b with [7] baa=abbb:

Critical pair: abbabbb=ba.

Referenced by [10], [11], [12], [15].

Overlap of [6] aab=bbba with [9] abbabbb=ba:

Critical pair: aba=bbbababbb.

Flip LHS and RHS.

Referenced by [13].

Overlap of [7] baa=abbb with [9] abbabbb=ba:

Critical pair: baba=abbbbbabbb.

Reduce RHS:

Defines rule #8.

Referenced by [12], [13].

Overlap of [9] abbabbb=ba with [5] bbbba=abbbb:

Critical pair: abbababbbb=babba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Simplify [10] bbbababbb=aba.

Reduce LHS:

Referenced by [14], [15].

Overlap of [3] aaab=b with [13] ababbbbbbbbbbbbbbbbbbbbbbbb=aba:

Critical pair: aaaba=babbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [8] bbbabba=ab with [13] ababbbbbbbbbbbbbbbbbbbbbbbb=aba:

Critical pair: bbbabbaba=abbabbbbbbbbbbbbbbbbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #5.

Overlap of [8] bbbabba=ab with [12] babba=bbabbbbbbbbbbbbbbbbbbbbb:

Critical pair: bbbbabbbbbbbbbbbbbbbbbbbbb=ab.

Reduce LHS:

Referenced by [17].

Overlap of [16] abbbbbbbbbbbbbbbbbbbbbbbbb=ab with [5] bbbba=abbbb:

Critical pair: abbbbbbbbbbbbbbbbbbbbbbbabbbb=abbba.

Reduce LHS:

Reduce RHS:

Defines rule #1.