Certificate for #2333 ⟨a, b | abababa=bab⟩

Completion settings:

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

[1] abababa=bab

Axiom: abababa=bab.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #12.

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

[3] bcc=d

Axiom: bcc=d.

Defines rule #2.

Referenced by [7], [8], [9], [10], [11], [13], [14], [15], [16].

[4] abababa=cb

Simplify [1] abababa=bab.

Reduce RHS:

[2]	(ba)b
	⇒ cb

Referenced by [5].

[5] accc=cb

Overlap of [4] abababa=cb with [2] ba=c:

a bababa ba

Critical pair: acbaba=cb.

Reduce LHS:

[2]	ac(ba)ba
[2]	⇒ acc(ba)
	⇒ accc

Defines rule #4.

Referenced by [6], [12], [13], [14].

[6] bcb=cccc

Overlap of [2] ba=c with [5] accc=cb:

b a accc

Critical pair: bcb=cccc.

Defines rule #11.

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

[7] cccca=d

Overlap of [6] bcb=cccc with [2] ba=c:

bc b ba

Critical pair: bcc=cccca.

Reduce LHS:

[3]	(bcc)
	⇒ d

Flip LHS and RHS.

Defines rule #5.

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

[8] bcd=cccccc

Overlap of [6] bcb=cccc with [3] bcc=d:

bc b bcc

Critical pair: bcd=cccccc.

Defines rule #10.

Referenced by [11], [15], [16], [17].

[9] cccccb=dccc

Overlap of [6] bcb=cccc with [6] bcb=cccc:

bc b bcb

Critical pair: bccccc=cccccb.

Reduce LHS:

[3]	(bcc)ccc
	⇒ dccc

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [17].

[10] bd=dcca

Overlap of [3] bcc=d with [7] cccca=d:

b cc cccca

Critical pair: bd=dcca.

Defines rule #9.

[11] dccca=cccccc

Overlap of [3] bcc=d with [7] cccca=d:

bc c cccca

Critical pair: bcd=dccca.

Reduce LHS:

[8]	(bcd)
	⇒ cccccc

Flip LHS and RHS.

Defines rule #8.

[12] ad=cbca

Overlap of [5] accc=cb with [7] cccca=d:

a ccc cccca

Critical pair: ad=cbca.

Defines rule #13.

[13] acd=cda

Overlap of [5] accc=cb with [7] cccca=d:

ac cc cccca

Critical pair: acd=cbcca.

Reduce RHS:

[3]	c(bcc)a
	⇒ cda

Defines rule #14.

[14] accd=cdca

Overlap of [5] accc=cb with [7] cccca=d:

acc c cccca

Critical pair: accd=cbccca.

Reduce RHS:

[3]	c(bcc)ca
	⇒ cdca

Defines rule #15.

[15] cccccd=dccccc

Overlap of [6] bcb=cccc with [8] bcd=cccccc:

bc b bcd

Critical pair: bccccccc=cccccd.

Reduce LHS:

[3]	(bcc)ccccc
	⇒ dccccc

Flip LHS and RHS.

Defines rule #1.

[16] dccccb=ccccccccc

Overlap of [3] bcc=d with [9] cccccb=dccc:

bc c cccccb

Critical pair: bcdccc=dccccb.

Reduce LHS:

[8]	(bcd)ccc
	⇒ ccccccccc

Flip LHS and RHS.

Defines rule #7.

[17] dccccd=ccccccccccc

Overlap of [9] cccccb=dccc with [8] bcd=cccccc:

ccccc b bcd

Critical pair: ccccccccccc=dccccd.

Flip LHS and RHS.

Defines rule #6.