Certificate for #16056 ⟨a, b | aaa=bb, aabb=aa⟩

Completion settings:

• Auxiliary generators:
  1. c = aa
• Reduction order:
  • Left-to-right recursive path with deg(c) = 0; deg(a) = 1; deg(b) = 2

Axiom: aaa=bb.

Flip LHS and RHS.

Referenced by [2], [4].

Axiom: aabb=aa.

Reduce LHS:

Referenced by [5].

Axiom: aa=c.

Defines rule #4.

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

Simplify [1] bb=aaa.

Reduce RHS:

Referenced by [10].

Simplify [2] aaaaa=aa.

Reduce RHS:

Referenced by [6].

Overlap of [5] aaaaa=c with [3] aa=c:

Critical pair: caaa=c.

Reduce LHS:

Referenced by [8].

Overlap of [3] aa=c with [3] aa=c:

Critical pair: ac=ca.

Flip LHS and RHS.

Referenced by [8], [10], [15], [17].

Simplify [6] cca=c.

Reduce LHS:

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

Overlap of [3] aa=c with [8] acc=c:

Critical pair: ac=ccc.

Defines rule #2.

Referenced by [10], [12], [15], [17].

Simplify [4] bb=ca.

Reduce RHS:

Defines rule #9.

Referenced by [11].

Overlap of [10] bb=ccc with [10] bb=ccc:

Critical pair: bccc=cccb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [13], [14].

Overlap of [8] acc=c with [9] ac=ccc:

Critical pair: cccc=c.

Defines rule #1.

Referenced by [14], [16].

Overlap of [8] acc=c with [11] cccb=bccc:

Critical pair: abccc=ccb.

Referenced by [16].

Overlap of [12] cccc=c with [11] cccb=bccc:

Critical pair: cbccc=cb.

Defines rule #5.

Referenced by [15].

Overlap of [14] cbccc=cb with [7] ca=ac:

Critical pair: cbccac=cba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [13] abccc=ccb with [12] cccc=c:

Critical pair: abc=ccbc.

Defines rule #8.

Simplify [7] ca=ac.

Reduce RHS:

Defines rule #3.