Certificate for #15372 ⟨a, b | aba=bb, aaabbb=1⟩

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 #3.

Referenced by [2], [3], [5], [7], [8], [9], [10], [13], [14].

Axiom: aaabbb=1.

Reduce LHS:

Referenced by [4].

Overlap of [1] bb=aba with [1] bb=aba:

Critical pair: baba=abab.

Flip LHS and RHS.

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

Simplify [2] aaaabab=1.

Reduce LHS:

Referenced by [5], [6], [8], [11], [12], [13], [16], [17], [18].

Overlap of [1] bb=aba with [4] babaaaa=1:

Critical pair: b=abaabaaaa.

Flip LHS and RHS.

Referenced by [6], [7].

Overlap of [4] babaaaa=1 with [5] abaabaaaa=b:

Critical pair: babaaab=baabaaaa.

Referenced by [8].

Overlap of [5] abaabaaaa=b with [5] abaabaaaa=b:

Critical pair: abaabaaab=bbaabaaaa.

Reduce RHS:

Referenced by [10].

Overlap of [6] babaaab=baabaaaa with [1] bb=aba:

Critical pair: babaaaaba=baabaaaab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [1] bb=aba with [8] baabaaaab=ba:

Critical pair: bba=abaaabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11], [12].

Overlap of [8] baabaaaab=ba with [3] abab=baba:

Critical pair: baabaaababa=baab.

Reduce LHS:

Referenced by [14].

Overlap of [3] abab=baba with [9] abaaabaaaab=abaa:

Critical pair: ababaa=babaaaabaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [8] baabaaaab=ba with [9] abaaabaaaab=abaa:

Critical pair: baabaaaabaa=baaaabaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [4] babaaaa=1 with [12] aaab=baaa:

Critical pair: babaaabaaa=aab.

Reduce LHS:

Referenced by [15].

Overlap of [10] abaaabaaaaaaa=baab with [12] aaab=baaa:

Critical pair: abbaaaaaaaaaa=baab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [15].

Overlap of [13] baabaaaaaaa=aab with [14] baab=aabaaaaaaaaaaa:

Critical pair: aabaaaaaaaaaaaaaaaaaa=aab.

Referenced by [16].

Overlap of [15] aabaaaaaaaaaaaaaaaaaa=aab with [12] aaab=baaa:

Critical pair: aabaaaaaaaaaaaaaaaabaaa=aabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [4] babaaaa=1 with [16] babaa=aaaaaaaaaaaaaaaa:

Critical pair: aaaaaaaaaaaaaaaaaa=1.

Defines rule #1.

Referenced by [18].

Overlap of [4] babaaaa=1 with [17] aaaaaaaaaaaaaaaaaa=1:

Critical pair: bab=aaaaaaaaaaaaaa.

Defines rule #4.