Certificate for #18011 ⟨a, b | abab=1, aaaaa=bb⟩

Completion settings:

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

Axiom: abab=1.

Referenced by [3], [8], [14].

Axiom: aaaaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4], [11], [12], [13], [14].

Overlap of [1] abab=1 with [2] bb=aaaaa:

Critical pair: abaaaaaa=b.

Referenced by [5], [6], [7], [8], [9], [10].

Overlap of [2] bb=aaaaa with [2] bb=aaaaa:

Critical pair: baaaaa=aaaaab.

Flip LHS and RHS.

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

Overlap of [3] abaaaaaa=b with [4] aaaaab=baaaaa:

Critical pair: abaabaaaaa=bab.

Referenced by [8].

Overlap of [3] abaaaaaa=b with [4] aaaaab=baaaaa:

Critical pair: abaaabaaaaa=baab.

Referenced by [9].

Overlap of [4] aaaaab=baaaaa with [3] abaaaaaa=b:

Critical pair: aaaab=baaaaaaaaaaa.

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

Overlap of [5] abaabaaaaa=bab with [3] abaaaaaa=b:

Critical pair: abab=baba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [6] abaaabaaaaa=baab with [3] abaaaaaa=b:

Critical pair: abaab=baaba.

Referenced by [13].

Overlap of [7] aaaab=baaaaaaaaaaa with [3] abaaaaaa=b:

Critical pair: aaab=baaaaaaaaaaaaaaaaa.

Referenced by [11].

Overlap of [8] baba=1 with [10] aaab=baaaaaaaaaaaaaaaaa:

Critical pair: babbaaaaaaaaaaaaaaaaa=aab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [8] baba=1 with [11] aab=baaaaaaaaaaaaaaaaaaaaaaa:

Critical pair: babbaaaaaaaaaaaaaaaaaaaaaaa=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [14].

Overlap of [11] aab=baaaaaaaaaaaaaaaaaaaaaaa with [9] abaab=baaba:

Critical pair: abaaba=baaaaaaaaaaaaaaaaaaaaaaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [1] abab=1 with [12] ab=baaaaaaaaaaaaaaaaaaaaaaaaaaaaa:

Critical pair: baaaaaaaaaaaaaaaaaaaaaaaaaaaaaab=1.

Reduce LHS:

Defines rule #1.