Certificate for #3181 ⟨a, b, c | ba=ab, aaca=1⟩

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

Completion settings:

[1] ba=ab

Axiom: ba=ab.

Defines rule #2.

Referenced by [3], [5].

[2] aaca=1

Axiom: aaca=1.

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

[3] aabca=b

Overlap of [1] ba=ab with [2] aaca=1:

b a aaca

Critical pair: b=abaca.

Reduce RHS:

[1]a(ba)ca
⇒ aabca

Flip LHS and RHS.

Referenced by [7].

[4] aca=aac

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

aac a aaca

Critical pair: aac=aca.

Flip LHS and RHS.

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

[5] abca=aabc

Overlap of [1] ba=ab with [4] aca=aac:

b a aca

Critical pair: baac=abca.

Reduce LHS:

[1](ba)ac
[1]⇒ a(ba)c
⇒ aabc

Flip LHS and RHS.

Referenced by [7].

[6] ca=ac

Overlap of [2] aaca=1 with [4] aca=aac:

aac a aca

Critical pair: aacaac=ca.

Reduce LHS:

[2](aaca)ac
⇒ ac

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[7] aaabc=b

Simplify [3] aabca=b.

Reduce LHS:

[5]a(abca)
⇒ aaabc

Referenced by [8].

[8] bc=cb

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

c a aaabc

Critical pair: cb=acaabc.

Reduce RHS:

[4](aca)abc
[2]⇒ (aaca)bc
⇒ bc

Flip LHS and RHS.

Defines rule #3.

[9] aaac=1

Overlap of [2] aaca=1 with [4] aca=aac:

a aca aca

Critical pair: aaac=1.

Defines rule #4.