Certificate for #16549 ⟨a, b | aba=bb, bab=aaa⟩

Completion settings:

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

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #6.

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

Axiom: bab=aaa.

Defines rule #7.

Referenced by [3], [4], [5], [13], [14].

Overlap of [1] bb=aba with [2] bab=aaa:

Critical pair: baaa=abaab.

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [2] bab=aaa with [1] bb=aba:

Critical pair: baaba=aaab.

Defines rule #8.

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

Overlap of [2] bab=aaa with [2] bab=aaa:

Critical pair: baaaa=aaaab.

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [1] bb=aba with [4] baaba=aaab:

Critical pair: baaab=abaaaba.

Flip LHS and RHS.

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

Overlap of [4] baaba=aaab with [5] aaaab=baaaa:

Critical pair: baabbaaaa=aaabaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9].

Overlap of [6] abaaaba=baaab with [7] aaabaaab=baaabaaaaa:

Critical pair: abbaaabaaaaa=baaabaab.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Overlap of [7] aaabaaab=baaabaaaaa with [6] abaaaba=baaab:

Critical pair: aabaaab=baaabaaaaaa.

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

Overlap of [4] baaba=aaab with [9] aabaaab=baaabaaaaaa:

Critical pair: bbaaabaaaaaa=aaabaab.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [14].

Overlap of [9] aabaaab=baaabaaaaaa with [6] abaaaba=baaab:

Critical pair: abaaab=baaabaaaaaaa.

Defines rule #11.

Referenced by [12], [13].

Overlap of [6] abaaaba=baaab with [11] abaaab=baaabaaaaaaa:

Critical pair: baaabaaaaaaaa=baaab.

Defines rule #9.

Referenced by [13].

Overlap of [9] aabaaab=baaabaaaaaa with [11] abaaab=baaabaaaaaaa:

Critical pair: aabaabaaabaaaaaaa=baaabaaaaaaaaab.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Overlap of [10] aabaaaaaaaaaaa=aabaaa with [5] aaaab=baaaa:

Critical pair: aabaaaaaaaaabaaaa=aabaaaaab.

Reduce LHS:

Reduce RHS:

Defines rule #1.