Certificate for #2065 ⟨a, b | ababbaba=ab⟩

Completion settings:

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

[1] ababbaba=ab

Axiom: ababbaba=ab.

Referenced by [3], [4], [5], [6], [7], [8], [9], [12].

[2] bbbabaa=c

Axiom: bbbabaa=c.

Referenced by [4], [5], [7], [9], [10], [11], [12], [13].

[3] ababbab=abbbaba

Overlap of [1] ababbaba=ab with [1] ababbaba=ab:

ababb aba ababbaba

Critical pair: ababbab=abbbaba.

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

[4] abbabbaba=acb

Overlap of [1] ababbaba=ab with [1] ababbaba=ab:

ababbab a ababbaba

Critical pair: ababbabab=abbabbaba.

Reduce LHS:

[3]	(ababbab)ab
[2]	⇒ a(bbbabaa)b
	⇒ acb

Flip LHS and RHS.

Referenced by [10].

[5] cbabbaba=cb

Overlap of [2] bbbabaa=c with [1] ababbaba=ab:

bbbaba a ababbaba

Critical pair: bbbabaab=cbabbaba.

Reduce LHS:

[2]	(bbbabaa)b
	⇒ cb

Flip LHS and RHS.

Referenced by [6], [7], [11], [16].

[6] cbabbab=cbbbaba

Overlap of [5] cbabbaba=cb with [1] ababbaba=ab:

cbabb aba ababbaba

Critical pair: cbabbab=cbbbaba.

Referenced by [7], [11], [18].

[7] cbbabbaba=ccb

Overlap of [5] cbabbaba=cb with [1] ababbaba=ab:

cbabbab a ababbaba

Critical pair: cbabbabab=cbbabbaba.

Reduce LHS:

[6]	(cbabbab)ab
[2]	⇒ c(bbbabaa)b
	⇒ ccb

Flip LHS and RHS.

Referenced by [8], [9].

[8] cbbabbab=ccbbbaba

Overlap of [7] cbbabbaba=ccb with [1] ababbaba=ab:

cbbabb aba ababbaba

Critical pair: cbbabbab=ccbbbaba.

Referenced by [9], [10].

[9] cccb=cccc

Overlap of [7] cbbabbaba=ccb with [1] ababbaba=ab:

cbbabbab a ababbaba

Critical pair: cbbabbabab=ccbbabbaba.

Reduce LHS:

[8]	(cbbabbab)ab
[2]	⇒ cc(bbbabaa)b
	⇒ cccb

Reduce RHS:

[8]	c(cbbabbab)a
[2]	⇒ ccc(bbbabaa)
	⇒ cccc

Referenced by [18].

[10] ccb=ccc

Overlap of [2] bbbabaa=c with [4] abbabbaba=acb:

bbbaba a abbabbaba

Critical pair: bbbabaacb=cbbabbaba.

Reduce LHS:

[2]	(bbbabaa)cb
	⇒ ccb

Reduce RHS:

[8]	(cbbabbab)a
[2]	⇒ cc(bbbabaa)
	⇒ ccc

Referenced by [14], [18].

[11] cb=cc

Overlap of [5] cbabbaba=cb with [6] cbabbab=cbbbaba:

cbabbaba cbabbab

Critical pair: cbbbabaa=cb.

Reduce LHS:

[2]	c(bbbabaa)
	⇒ cc

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [15], [16], [17], [18], [19], [20].

[12] ab=ac

Overlap of [1] ababbaba=ab with [3] ababbab=abbbaba:

ababbaba ababbab

Critical pair: abbbabaa=ab.

Reduce LHS:

[2]	a(bbbabaa)
	⇒ ac

Flip LHS and RHS.

Defines rule #2.

Referenced by [13], [14], [15], [17], [18], [19], [20].

[13] bbbacaa=c

Overlap of [2] bbbabaa=c with [12] ab=ac:

bbb abaa ab

Critical pair: bbbacaa=c.

Defines rule #7.

Referenced by [20].

[14] ababbab=acccaca

Simplify [3] ababbab=abbbaba.

Reduce RHS:

[12]	(ab)bbaba
[11]	⇒ a(cb)baba
[10]	⇒ a(ccb)aba
[12]	⇒ accc(ab)a
	⇒ acccaca

Referenced by [15].

[15] acccaca=acaccac

Overlap of [14] ababbab=acccaca with [12] ab=ac:

ababbab ab

Critical pair: acabbab=acccaca.

Reduce LHS:

[12]	ac(ab)bab
[11]	⇒ aca(cb)ab
[12]	⇒ acacc(ab)
	⇒ acaccac

Flip LHS and RHS.

Defines rule #4.

Referenced by [20].

[16] cbabbaba=cc

Simplify [5] cbabbaba=cb.

Reduce RHS:

[11]	(cb)
	⇒ cc

Referenced by [17].

[17] ccaccaca=cc

Overlap of [16] cbabbaba=cc with [11] cb=cc:

cbabbaba cb

Critical pair: ccabbaba=cc.

Reduce LHS:

[12]	cc(ab)baba
[11]	⇒ cca(cb)aba
[12]	⇒ ccacc(ab)a
	⇒ ccaccaca

Defines rule #5.

[18] cbabbab=ccccaca

Simplify [6] cbabbab=cbbbaba.

Reduce RHS:

[11]	(cb)bbaba
[10]	⇒ (ccb)baba
[9]	⇒ (cccb)aba
[12]	⇒ cccc(ab)a
	⇒ ccccaca

Referenced by [19].

[19] ccccaca=ccaccac

Overlap of [18] cbabbab=ccccaca with [11] cb=cc:

cbabbab cb

Critical pair: ccabbab=ccccaca.

Reduce LHS:

[12]	cc(ab)bab
[11]	⇒ cca(cb)ab
[12]	⇒ ccacc(ab)
	⇒ ccaccac

Flip LHS and RHS.

Defines rule #3.

[20] acaccaca=ac

Overlap of [12] ab=ac with [13] bbbacaa=c:

a b bbbacaa

Critical pair: ac=acbbacaa.

Reduce RHS:

[11]	a(cb)bacaa
[11]	⇒ ac(cb)acaa
[15]	⇒ (acccaca)a
	⇒ acaccaca

Flip LHS and RHS.

Defines rule #6.