Certificate for #5622 ⟨a, b, c | aa=a, abb=ca⟩

Completion settings:

Axiom: aa=a.

Defines rule #5.

Referenced by [4], [5].

Axiom: abb=ca.

Referenced by [5], [7].

Axiom: ac=d.

Defines rule #4.

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

Overlap of [1] aa=a with [3] ac=d:

a a ac

Critical pair: ad=ac.

Reduce RHS:

[3]	(ac)
	⇒ d

Defines rule #3.

a a abb

Critical pair: aca=abb.

Reduce LHS:

[3]	(ac)a
	⇒ da

Reduce RHS:

[2]	(abb)
	⇒ ca

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7].

Overlap of [5] ca=da with [3] ac=d:

c a ac

Critical pair: cd=dac.

Reduce RHS:

[3]	d(ac)
	⇒ dd

Defines rule #1.

Reduce RHS:

[5]	(ca)
	⇒ da

Defines rule #6.