Certificate for #4509 ⟨a, b | aaba=b, bbbbb=1⟩

Completion settings:

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

Axiom: aaba=b.

Referenced by [3], [5], [9], [12], [13], [14], [15], [16], [17], [18].

Axiom: bbbbb=1.

Defines rule #3.

Referenced by [4], [6], [9], [10], [19], [20].

Overlap of [1] aaba=b with [1] aaba=b:

Critical pair: aabb=baba.

Referenced by [4], [7], [8], [9], [11], [18].

Overlap of [3] aabb=baba with [2] bbbbb=1:

Critical pair: aa=bababbb.

Flip LHS and RHS.

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

Overlap of [1] aaba=b with [4] bababbb=aa:

Critical pair: aaaa=bbabbb.

Flip LHS and RHS.

Referenced by [6], [7].

Overlap of [2] bbbbb=1 with [5] bbabbb=aaaa:

Critical pair: bbbaaaa=abbb.

Flip LHS and RHS.

Referenced by [8], [9].

Overlap of [4] bababbb=aa with [5] bbabbb=aaaa:

Critical pair: bababaaaa=aaabbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [3] aabb=baba with [6] abbb=bbbaaaa:

Critical pair: abbbaaaa=babab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [6] abbb=bbbaaaa with [4] bababbb=aa:

Critical pair: abbaa=bbbaaaaababbb.

Reduce RHS:

Referenced by [11].

Overlap of [2] bbbbb=1 with [8] babab=bbbaaaaaaaa:

Critical pair: bbbbbbbaaaaaaaa=abab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [3] aabb=baba with [9] abbaa=baaaaaaaaaaaab:

Critical pair: abaaaaaaaaaaaab=babaaa.

Referenced by [12].

Overlap of [11] abaaaaaaaaaaaab=babaaa with [1] aaba=b:

Critical pair: abaaaaaaaaaab=babaaaa.

Referenced by [13].

Overlap of [12] abaaaaaaaaaab=babaaaa with [1] aaba=b:

Critical pair: abaaaaaaaab=babaaaaa.

Referenced by [14].

Overlap of [13] abaaaaaaaab=babaaaaa with [1] aaba=b:

Critical pair: abaaaaaab=babaaaaaa.

Referenced by [15].

Overlap of [14] abaaaaaab=babaaaaaa with [1] aaba=b:

Critical pair: abaaaab=babaaaaaaa.

Referenced by [16].

Overlap of [15] abaaaab=babaaaaaaa with [1] aaba=b:

Critical pair: abaab=babaaaaaaaa.

Referenced by [17].

Overlap of [1] aaba=b with [16] abaab=babaaaaaaaa:

Critical pair: ababaaaaaaaa=bab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [1] aaba=b with [17] bab=bbaaaaaaaaaaaaaaaa:

Critical pair: aabbaaaaaaaaaaaaaaaa=bb.

Reduce LHS:

Referenced by [20].

Overlap of [2] bbbbb=1 with [17] bab=bbaaaaaaaaaaaaaaaa:

Critical pair: bbbbbbaaaaaaaaaaaaaaaa=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [2] bbbbb=1 with [18] bbaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=bb:

Critical pair: bbbbb=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.