Certificate for #5867 ⟨a, b | ababab=aabba⟩

Completion settings:

Auxiliary generators:
1. c = ab
2. d = cccb
Reduction order:
- Left-to-right recursive path with deg(c) = deg(d) = 0, c < d; deg(a) = deg(b) = 1, a < b

[1] ababab=aabba

Axiom: ababab=aabba.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Defines rule #11.

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

[3] cccb=d

Axiom: cccb=d.

Defines rule #5.

Referenced by [6], [7], [8], [9], [11], [13].

[4] ababab=acba

Simplify [1] ababab=aabba.

Reduce RHS:

[2]	a(ab)ba
	⇒ acba

Referenced by [5].

[5] acba=ccc

Overlap of [4] ababab=acba with [2] ab=c:

ababab ab

Critical pair: cabab=acba.

Reduce LHS:

[2]	c(ab)ab
[2]	⇒ cc(ab)
	⇒ ccc

Flip LHS and RHS.

Defines rule #14.

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

[6] acbc=d

Overlap of [5] acba=ccc with [2] ab=c:

acb a ab

Critical pair: acbc=cccb.

Reduce RHS:

[3]	(cccb)
	⇒ d

Defines rule #12.

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

[7] cda=dcc

Overlap of [5] acba=ccc with [5] acba=ccc:

acb a acba

Critical pair: acbccc=ccccba.

Reduce LHS:

[6]	(acbc)cc
	⇒ dcc

Reduce RHS:

[3]	c(cccb)a
	⇒ cda

Flip LHS and RHS.

Defines rule #3.

Referenced by [10], [11], [13].

[8] acbd=cdc

Overlap of [5] acba=ccc with [6] acbc=d:

acb a acbc

Critical pair: acbd=ccccbc.

Reduce RHS:

[3]	c(cccb)c
	⇒ cdc

Defines rule #13.

Referenced by [9], [10], [13].

[9] dccb=cdc

Overlap of [6] acbc=d with [3] cccb=d:

acb c cccb

Critical pair: acbd=dccb.

Reduce LHS:

[8]	(acbd)
	⇒ cdc

Flip LHS and RHS.

Defines rule #6.

Referenced by [12], [14].

[10] dda=cdccc

Overlap of [6] acbc=d with [7] cda=dcc:

acb c cda

Critical pair: acbdcc=dda.

Reduce LHS:

[8]	(acbd)cc
	⇒ cdccc

Flip LHS and RHS.

Defines rule #4.

[11] ddc=cdd

Overlap of [7] cda=dcc with [6] acbc=d:

cd a acbc

Critical pair: cdd=dcccbc.

Reduce RHS:

[3]	d(cccb)c
	⇒ ddc

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [14], [15].

[12] ccddb=dcdc

Overlap of [11] ddc=cdd with [9] dccb=cdc:

d dc dccb

Critical pair: dcdc=cddcb.

Reduce RHS:

[11]	c(ddc)b
	⇒ ccddb

Flip LHS and RHS.

Defines rule #7.

[13] cdcdc=ddd

Overlap of [7] cda=dcc with [8] acbd=cdc:

cd a acbd

Critical pair: cdcdc=dcccbd.

Reduce RHS:

[3]	d(cccb)d
	⇒ ddd

Defines rule #2.

Referenced by [14], [16].

[14] dcddb=cdccdc

Overlap of [13] cdcdc=ddd with [9] dccb=cdc:

cdc dc dccb

Critical pair: cdccdc=dddcb.

Reduce RHS:

[11]	d(ddc)b
	⇒ dcddb

Flip LHS and RHS.

Defines rule #8.

Referenced by [15], [16].

[15] cddddb=dcdccdc

Overlap of [11] ddc=cdd with [14] dcddb=cdccdc:

d dc dcddb

Critical pair: dcdccdc=cddddb.

Flip LHS and RHS.

Defines rule #9.

[16] dddddb=cdccdccdc

Overlap of [13] cdcdc=ddd with [14] dcddb=cdccdc:

cdc dc dcddb

Critical pair: cdccdccdc=dddddb.

Flip LHS and RHS.

Defines rule #10.