Certificate for #1385 ⟨a, b | aaba=b, bbbb=1⟩

Completion settings:

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

Axiom: aaba=b.

Referenced by [3], [5], [6], [8], [11], [12], [13], [14].

Axiom: bbbb=1.

Defines rule #3.

Referenced by [4], [7], [10], [15].

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

Critical pair: aabb=baba.

Referenced by [4], [8].

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

Critical pair: aa=bababb.

Flip LHS and RHS.

Referenced by [5], [6].

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

Critical pair: aaaa=bbabb.

Flip LHS and RHS.

Referenced by [7], [8].

Overlap of [4] bababb=aa with [4] bababb=aa:

Critical pair: bababaa=aaababb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [2] bbbb=1 with [5] bbabb=aaaa:

Critical pair: bbaaaa=abb.

Flip LHS and RHS.

Referenced by [9].

Overlap of [5] bbabb=aaaa with [5] bbabb=aaaa:

Critical pair: bbabaaaa=aaaababb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Simplify [6] abbb=bababaa.

Reduce LHS:

Reduce RHS:

Referenced by [10].

Overlap of [2] bbbb=1 with [9] bbaaaab=bbabaaaaaa:

Critical pair: bbbbabaaaaaa=aaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [10] aaaab=abaaaaaa with [1] aaba=b:

Critical pair: aab=abaaaaaaa.

Referenced by [12], [14].

Overlap of [1] aaba=b with [11] aab=abaaaaaaa:

Critical pair: abaaaaaaaa=b.

Referenced by [13].

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

Critical pair: ab=baaaaaaa.

Defines rule #2.

Referenced by [14].

Overlap of [1] aaba=b with [11] aab=abaaaaaaa:

Critical pair: abaaaaaaaa=b.

Reduce LHS:

Referenced by [15].

Overlap of [2] bbbb=1 with [14] baaaaaaaaaaaaaaa=b:

Critical pair: bbbb=aaaaaaaaaaaaaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.