Certificate for #1577 ⟨a, b, c | aaa=bb, cac=1⟩

Completion settings:

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

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [4].

Axiom: cac=1.

Referenced by [3], [5].

Overlap of [2] cac=1 with [2] cac=1:

Critical pair: ca=ac.

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [7], [8], [9], [10], [11], [12].

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

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

Overlap of [2] cac=1 with [3] ac=ca:

Critical pair: cca=1.

Defines rule #2.

Referenced by [6], [8], [10], [12].

Overlap of [5] cca=1 with [4] aaab=baaa:

Critical pair: ccbaaa=aab.

Referenced by [7].

Overlap of [6] ccbaaa=aab with [3] ac=ca:

Critical pair: ccbaaca=aabc.

Reduce LHS:

Referenced by [8].

Overlap of [7] ccbcaaa=aabc with [3] ac=ca:

Critical pair: ccbcaaca=aabcc.

Reduce LHS:

Referenced by [9].

Overlap of [8] ccbaa=aabcc with [3] ac=ca:

Critical pair: ccbaca=aabccc.

Reduce LHS:

Referenced by [10].

Overlap of [9] ccbcaa=aabccc with [3] ac=ca:

Critical pair: ccbcaca=aabcccc.

Reduce LHS:

Referenced by [11].

Overlap of [10] ccba=aabcccc with [3] ac=ca:

Critical pair: ccbca=aabccccc.

Referenced by [12].

Overlap of [11] ccbca=aabccccc with [3] ac=ca:

Critical pair: ccbcca=aabcccccc.

Reduce LHS:

Defines rule #4.