Certificate for #16163 ⟨a, b | aab=ab, abaa=ba⟩

Back:⟨a, b | aab=ab, abaa=ba⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #5.

Referenced by [6].

[2] abaa=ba

Axiom: abaa=ba.

Referenced by [4].

[3] ba=c

Axiom: ba=c.

Defines rule #3.

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

[4] abaa=c

Simplify [2] abaa=ba.

Reduce RHS:

[3](ba)
⇒ c

Referenced by [5].

[5] aca=c

Overlap of [4] abaa=c with [3] ba=c:

a baa ba

Critical pair: aca=c.

Referenced by [7], [9].

[6] aac=ac

Overlap of [1] aab=ab with [3] ba=c:

aa b ba

Critical pair: aac=aba.

Reduce RHS:

[3]a(ba)
⇒ ac

Referenced by [7].

[7] ac=c

Overlap of [6] aac=ac with [5] aca=c:

a ac aca

Critical pair: ac=aca.

Reduce RHS:

[5](aca)
⇒ c

Defines rule #1.

Referenced by [8], [9].

[8] bc=cc

Overlap of [3] ba=c with [7] ac=c:

b a ac

Critical pair: bc=cc.

Defines rule #4.

[9] ca=c

Overlap of [5] aca=c with [7] ac=c:

aca ac

Critical pair: ca=c.

Defines rule #2.