Certificate for #3196 ⟨a, b, c | ba=ab, cacc=1⟩

Back:⟨a, b, c | ba=ab, cacc=1⟩

Completion settings:

[1] ba=ab

Axiom: ba=ab.

Defines rule #2.

Referenced by [6].

[2] cacc=1

Axiom: cacc=1.

Referenced by [3], [4], [10].

[3] cac=acc

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

cac c cacc

Critical pair: cac=acc.

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

[4] accc=1

Overlap of [2] cacc=1 with [3] cac=acc:

cacc cac

Critical pair: accc=1.

Defines rule #3.

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

[5] caacc=a

Overlap of [3] cac=acc with [3] cac=acc:

ca c cac

Critical pair: caacc=accac.

Reduce RHS:

[3]ac(cac)
[3]⇒ a(cac)c
[4]⇒ a(accc)
⇒ a

Referenced by [7].

[6] abccc=b

Overlap of [1] ba=ab with [4] accc=1:

b a accc

Critical pair: b=abccc.

Flip LHS and RHS.

Referenced by [8].

[7] ca=ac

Overlap of [5] caacc=a with [4] accc=1:

ca acc accc

Critical pair: ca=ac.

Defines rule #1.

Referenced by [8].

[8] acbccc=cb

Overlap of [7] ca=ac with [6] abccc=b:

c a abccc

Critical pair: cb=acbccc.

Flip LHS and RHS.

Referenced by [9].

[9] accbccc=ccb

Overlap of [3] cac=acc with [8] acbccc=cb:

c ac acbccc

Critical pair: ccb=accbccc.

Flip LHS and RHS.

Referenced by [10].

[10] bccc=cccb

Overlap of [2] cacc=1 with [9] accbccc=ccb:

c acc accbccc

Critical pair: cccb=bccc.

Flip LHS and RHS.

Defines rule #4.