Certificate for #14342 ⟨a, b | aaaa=a, aabba=b⟩

Completion settings:

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

Axiom: aaaa=a.

Defines rule #4.

Referenced by [3], [4].

Axiom: aabba=b.

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

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

Critical pair: aab=abba.

Referenced by [4], [5], [6], [8].

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

Critical pair: aabba=baaa.

Reduce LHS:

Referenced by [5].

Overlap of [2] aabba=b with [3] aab=abba:

Critical pair: abbaba=b.

Reduce LHS:

Defines rule #3.

Referenced by [6], [9], [10], [12].

Overlap of [2] aabba=b with [5] baaa=b:

Critical pair: aabb=baa.

Reduce LHS:

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

Overlap of [2] aabba=b with [6] abbab=baa:

Critical pair: abaa=bb.

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

Overlap of [2] aabba=b with [6] abbab=baa:

Critical pair: aabbbaa=bbbab.

Reduce LHS:

Referenced by [11].

Overlap of [6] abbab=baa with [7] abaa=bb:

Critical pair: abbbb=baaaa.

Reduce RHS:

Referenced by [11].

Overlap of [7] abaa=bb with [5] baaa=b:

Critical pair: ab=bba.

Defines rule #2.

Referenced by [11].

Simplify [9] abbbb=ba.

Reduce LHS:

Referenced by [12].

Overlap of [11] bbbbbbbba=ba with [5] baaa=b:

Critical pair: bbbbbbbb=baaa.

Reduce RHS:

Defines rule #1.