Certificate for #2415 ⟨a, b, c | aab=b, aaca=1⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3], [6].

[2] aaca=1

Axiom: aaca=1.

Referenced by [3], [4], [5], [7].

[3] aacb=ab

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

aac a aab

Critical pair: aacb=ab.

Referenced by [6].

[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], [7].

[5] 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 [6].

[6] cb=ab

Overlap of [5] ca=ac with [1] aab=b:

c a aab

Critical pair: cb=acab.

Reduce RHS:

[4](aca)b
[3]⇒ (aacb)
⇒ ab

Defines rule #2.

[7] aaac=1

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

a aca aca

Critical pair: aaac=1.

Defines rule #4.