Certificate for #3440 ⟨a, b, c | ba=ac, aac=a⟩

Completion settings:

Auxiliary generators:
1. d = cac
Reduction order:
- Left-to-right shortlex with a < b < d < c

[1] ba=ac

Axiom: ba=ac.

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

[2] aac=a

Axiom: aac=a.

Referenced by [4], [11].

[3] cac=d

Axiom: cac=d.

Referenced by [4], [6].

[4] ac=ad

Overlap of [1] ba=ac with [2] aac=a:

b a aac

Critical pair: ba=acac.

Reduce LHS:

[1]	(ba)
	⇒ ac

Reduce RHS:

[3]	a(cac)
	⇒ ad

Defines rule #1.

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

[5] adc=add

Overlap of [1] ba=ac with [4] ac=ad:

b a ac

Critical pair: bad=acc.

Reduce LHS:

[1]	(ba)d
[4]	⇒ (ac)d
	⇒ add

Reduce RHS:

[4]	(ac)c
	⇒ adc

Flip LHS and RHS.

Referenced by [8].

[6] cad=d

Simplify [3] cac=d.

Reduce LHS:

[4]	c(ac)
	⇒ cad

Defines rule #6.

Referenced by [7], [8], [9].

[7] adad=ad

Overlap of [4] ac=ad with [6] cad=d:

a c cad

Critical pair: ad=adad.

Flip LHS and RHS.

Referenced by [9].

[8] dc=dd

Overlap of [6] cad=d with [5] adc=add:

c ad adc

Critical pair: cadd=dc.

Reduce LHS:

[6]	(cad)d
	⇒ dd

Flip LHS and RHS.

Defines rule #3.

[9] dad=d

Overlap of [6] cad=d with [7] adad=ad:

c ad adad

Critical pair: cad=dad.

Reduce LHS:

[6]	(cad)
	⇒ d

Flip LHS and RHS.

Defines rule #5.

[10] ba=ad

Simplify [1] ba=ac.

Reduce RHS:

[4]	(ac)
	⇒ ad

Defines rule #2.

[11] aad=a

Overlap of [2] aac=a with [4] ac=ad:

a ac ac

Critical pair: aad=a.

Defines rule #4.