Certificate for #5125 ⟨a, b, c | aa=a, abca=b⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b < c

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abca=b

Axiom: abca=b.

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

[3] ab=b

Overlap of [1] aa=a with [2] abca=b:

a a abca

Critical pair: ab=abca.

Reduce RHS:

[2]	(abca)
	⇒ b

Defines rule #2.

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

[4] bca=ba

Overlap of [2] abca=b with [1] aa=a:

abc a aa

Critical pair: abca=ba.

Reduce LHS:

[3]	(ab)ca
	⇒ bca

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

[5] bcb=bba

Overlap of [2] abca=b with [2] abca=b:

abc a abca

Critical pair: abcb=bbca.

Reduce LHS:

[3]	(ab)cb
	⇒ bcb

Reduce RHS:

[4]	b(bca)
	⇒ bba

Referenced by [8].

[6] ba=b

Overlap of [2] abca=b with [3] ab=b:

abca ab

Critical pair: bca=b.

Reduce LHS:

[4]	(bca)
	⇒ ba

Defines rule #3.

Referenced by [7], [8].

[7] bca=b

Simplify [4] bca=ba.

Reduce RHS:

[6]	(ba)
	⇒ b

Defines rule #4.

[8] bcb=bb

Simplify [5] bcb=bba.

Reduce RHS:

[6]	b(ba)
	⇒ bb

Defines rule #5.