Certificate for #19013 ⟨a, b | aab=b, abbaba=b⟩

Completion settings:

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

Axiom: aab=b.

Defines rule #2.

Referenced by [3], [4], [6], [7], [12], [13].

Axiom: abbaba=b.

Referenced by [3], [5], [8], [9].

Overlap of [1] aab=b with [2] abbaba=b:

Critical pair: ab=bbaba.

Flip LHS and RHS.

Referenced by [4], [8], [10], [11].

Overlap of [3] bbaba=ab with [1] aab=b:

Critical pair: bbabb=abab.

Referenced by [5], [6], [12].

Overlap of [4] bbabb=abab with [2] abbaba=b:

Critical pair: bbb=abababa.

Flip LHS and RHS.

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

Overlap of [4] bbabb=abab with [4] bbabb=abab:

Critical pair: bbaabab=abababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [1] aab=b with [5] abababa=bbb:

Critical pair: abbb=bababa.

Defines rule #4.

Referenced by [14].

Overlap of [3] bbaba=ab with [5] abababa=bbb:

Critical pair: bbbbb=abbaba.

Reduce RHS:

Defines rule #7.

Referenced by [9], [10].

Overlap of [5] abababa=bbb with [2] abbaba=b:

Critical pair: abababb=bbbbbaba.

Reduce LHS:

Reduce RHS:

Referenced by [10].

Overlap of [8] bbbbb=b with [9] bbbab=baba:

Critical pair: bbbbaba=bbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [3] bbaba=ab with [10] bbab=aba:

Critical pair: abaa=ab.

Referenced by [13].

Overlap of [4] bbabb=abab with [10] bbab=aba:

Critical pair: bbaaba=ababab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [1] aab=b with [11] abaa=ab:

Critical pair: aab=baa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [14].

Overlap of [10] bbab=aba with [7] abbb=bababa:

Critical pair: bbbababa=ababb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.