Certificate for #4408 ⟨a, b, c | aba=1, acac=c⟩

Back:⟨a, b, c | aba=1, acac=c⟩

Completion settings:

[1] aba=1

Axiom: aba=1.

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

[2] acac=c

Axiom: acac=c.

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

[3] ba=ab

Overlap of [1] aba=1 with [1] aba=1:

ab a aba

Critical pair: ab=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [8].

[4] cac=abc

Overlap of [1] aba=1 with [2] acac=c:

ab a acac

Critical pair: abc=cac.

Flip LHS and RHS.

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

[5] abc=acc

Overlap of [2] acac=c with [2] acac=c:

ac ac acac

Critical pair: acc=cac.

Reduce RHS:

[4](cac)
⇒ abc

Flip LHS and RHS.

Referenced by [6].

[6] bc=cc

Overlap of [3] ba=ab with [2] acac=c:

b a acac

Critical pair: bc=abcac.

Reduce RHS:

[5](abc)ac
[4]⇒ ac(cac)
[5]⇒ ac(abc)
[2]⇒ (acac)c
⇒ cc

Defines rule #2.

Referenced by [7].

[7] cac=acc

Simplify [4] cac=abc.

Reduce RHS:

[6]a(bc)
⇒ acc

Defines rule #4.

Referenced by [9].

[8] aab=1

Overlap of [1] aba=1 with [3] ba=ab:

a ba ba

Critical pair: aab=1.

Defines rule #3.

[9] aacc=c

Overlap of [2] acac=c with [7] cac=acc:

a cac cac

Critical pair: aacc=c.

Defines rule #5.