Certificate for #5614 ⟨a, b, c | aa=a, aab=ca⟩

Completion settings:

Axiom: aa=a.

Defines rule #1.

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

Axiom: aab=ca.

Reduce LHS:

[1]	(aa)b
	⇒ ab

Flip LHS and RHS.

Referenced by [5], [7].

Axiom: ba=d.

Defines rule #5.

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

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

b a aa

Critical pair: ba=da.

Reduce LHS:

[3]	(ba)
	⇒ d

Flip LHS and RHS.

Defines rule #3.

Overlap of [2] ca=ab with [1] aa=a:

c a aa

Critical pair: ca=aba.

Reduce LHS:

[2]	(ca)
	⇒ ab

Reduce RHS:

[3]	a(ba)
	⇒ ad

Defines rule #2.

Referenced by [6], [7].

Overlap of [3] ba=d with [5] ab=ad:

b a ab

Critical pair: bad=db.

Reduce LHS:

[3]	(ba)d
	⇒ dd

Flip LHS and RHS.

Defines rule #4.

Simplify [2] ca=ab.

Reduce RHS:

[5]	(ab)
	⇒ ad

Defines rule #6.