Certificate for #4851 ⟨a, b, c | ab=a, bacbb=1⟩

Completion settings:

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

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [6].

[2] bacbb=1

Axiom: bacbb=1.

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

[3] aacbb=a

Overlap of [1] ab=a with [2] bacbb=1:

a b bacbb

Critical pair: a=aacbb.

Flip LHS and RHS.

Referenced by [5].

[4] bacb=acbb

Overlap of [2] bacbb=1 with [2] bacbb=1:

bacb b bacbb

Critical pair: bacb=acbb.

Referenced by [7], [8].

[5] aacb=a

Overlap of [3] aacbb=a with [2] bacbb=1:

aacb b bacbb

Critical pair: aacb=aacbb.

Reduce RHS:

[3]	(aacbb)
	⇒ a

Referenced by [6].

[6] aac=a

Overlap of [5] aacb=a with [2] bacbb=1:

aac b bacbb

Critical pair: aac=aacbb.

Reduce RHS:

[5]	(aacb)b
[1]	⇒ (ab)
	⇒ a

Defines rule #2.

[7] acbbb=1

Overlap of [2] bacbb=1 with [4] bacb=acbb:

bacbb bacb

Critical pair: acbbb=1.

Defines rule #4.

Referenced by [8], [9].

[8] bacacbb=ac

Overlap of [4] bacb=acbb with [4] bacb=acbb:

bac b bacb

Critical pair: bacacbb=acbbacb.

Reduce RHS:

[4]	acb(bacb)
[4]	⇒ ac(bacb)b
[7]	⇒ ac(acbbb)
	⇒ ac

Referenced by [9].

[9] bac=acb

Overlap of [8] bacacbb=ac with [7] acbbb=1:

bac acbb acbbb

Critical pair: bac=acb.

Defines rule #3.