Certificate for #3749 ⟨a, b, c | aab=1, bbcac=1⟩

Completion settings:

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

Axiom: aab=1.

Defines rule #2.

Referenced by [3], [4], [7], [9], [10], [11].

Axiom: bbcac=1.

Referenced by [3], [6].

Overlap of [1] aab=1 with [2] bbcac=1:

Critical pair: aa=bcac.

Flip LHS and RHS.

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

Overlap of [1] aab=1 with [3] bcac=aa:

Critical pair: aaaa=cac.

Flip LHS and RHS.

Defines rule #5.

Referenced by [5].

Overlap of [3] bcac=aa with [4] cac=aaaa:

Critical pair: bcaaaaa=aaac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

Overlap of [2] bbcac=1 with [3] bcac=aa:

Critical pair: baa=1.

Referenced by [7], [8].

Overlap of [6] baa=1 with [1] aab=1:

Critical pair: ba=ab.

Defines rule #1.

Referenced by [11].

Overlap of [6] baa=1 with [5] aaac=bcaaaaa:

Critical pair: bbcaaaaa=ac.

Referenced by [9].

Overlap of [8] bbcaaaaa=ac with [1] aab=1:

Critical pair: bbcaaa=acb.

Referenced by [10].

Overlap of [9] bbcaaa=acb with [1] aab=1:

Critical pair: bbca=acbb.

Referenced by [11].

Overlap of [10] bbca=acbb with [1] aab=1:

Critical pair: bbc=acbbab.

Reduce RHS:

Defines rule #3.