Certificate for #5699 ⟨a, b | aababa=babba⟩

Completion settings:

Auxiliary generators:
1. c = babba
Reduction order:
- Right-to-left recursive path with deg(b) = deg(c) = 0, b < c; deg(a) = 1

[1] aababa=babba

Axiom: aababa=babba.

Referenced by [3].

[2] babba=c

Axiom: babba=c.

Defines rule #2.

Referenced by [3], [4], [6], [7], [11], [12], [14].

[3] aababa=c

Simplify [1] aababa=babba.

Reduce RHS:

[2]	(babba)
	⇒ c

Defines rule #15.

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

[4] babc=cbba

Overlap of [2] babba=c with [2] babba=c:

bab ba babba

Critical pair: babc=cbba.

Defines rule #1.

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

[5] aacbba=cababa

Overlap of [3] aababa=c with [3] aababa=c:

aabab a aababa

Critical pair: aababc=cababa.

Reduce LHS:

[4]	aa(babc)
	⇒ aacbba

Referenced by [8], [10].

[6] aabac=cbba

Overlap of [3] aababa=c with [2] babba=c:

aaba ba babba

Critical pair: aabac=cbba.

Defines rule #12.

Referenced by [8].

[7] cababa=babbc

Overlap of [2] babba=c with [3] aababa=c:

babb a aababa

Critical pair: babbc=cababa.

Flip LHS and RHS.

Defines rule #9.

Referenced by [8], [9], [10], [14].

[8] cabac=babbcbba

Overlap of [3] aababa=c with [6] aabac=cbba:

aabab a aabac

Critical pair: aababcbba=cabac.

Reduce LHS:

[4]	aa(babc)bba
[5]	⇒ (aacbba)bba
[7]	⇒ (cababa)bba
	⇒ babbcbba

Flip LHS and RHS.

Defines rule #3.

[9] babbbabbc=cacbba

Overlap of [7] cababa=babbc with [3] aababa=c:

cabab a aababa

Critical pair: cababc=babbcababa.

Reduce LHS:

[4]	ca(babc)
	⇒ cacbba

Reduce RHS:

[7]	babb(cababa)
	⇒ babbbabbc

Flip LHS and RHS.

Defines rule #4.

[10] aacbba=babbc

Simplify [5] aacbba=cababa.

Reduce RHS:

[7]	(cababa)
	⇒ babbc

Defines rule #10.

Referenced by [11], [12], [13], [14], [15], [16], [18].

[11] aacbbc=cacbba

Overlap of [3] aababa=c with [10] aacbba=babbc:

aabab a aacbba

Critical pair: aababbabbc=cacbba.

Reduce LHS:

[2]	aa(babba)bbc
	⇒ aacbbc

Defines rule #7.

Referenced by [15].

[12] aacbc=babbcbba

Overlap of [10] aacbba=babbc with [2] babba=c:

aacb ba babba

Critical pair: aacbc=babbcbba.

Defines rule #5.

Referenced by [16].

[13] aacbbbabbc=babbcacbba

Overlap of [10] aacbba=babbc with [10] aacbba=babbc:

aacbb a aacbba

Critical pair: aacbbbabbc=babbcacbba.

Referenced by [16], [17].

[14] babbcacbba=cacbbc

Overlap of [7] cababa=babbc with [10] aacbba=babbc:

cabab a aacbba

Critical pair: cababbabbc=babbcacbba.

Reduce LHS:

[2]	ca(babba)bbc
	⇒ cacbbc

Flip LHS and RHS.

Defines rule #11.

Referenced by [16], [17], [18].

[15] babbcacbbc=cacbbbabbc

Overlap of [10] aacbba=babbc with [11] aacbbc=cacbba:

aacbb a aacbbc

Critical pair: aacbbcacbba=babbcacbbc.

Reduce LHS:

[11]	(aacbbc)acbba
[10]	⇒ cacbb(aacbba)
	⇒ cacbbbabbc

Flip LHS and RHS.

Defines rule #8.

[16] babbcacbc=cacbbcbba

Overlap of [10] aacbba=babbc with [12] aacbc=babbcbba:

aacbb a aacbc

Critical pair: aacbbbabbcbba=babbcacbc.

Reduce LHS:

[13]	(aacbbbabbc)bba
[14]	⇒ (babbcacbba)bba
	⇒ cacbbcbba

Flip LHS and RHS.

Defines rule #6.

[17] aacbbbabbc=cacbbc

Simplify [13] aacbbbabbc=babbcacbba.

Reduce RHS:

[14]	(babbcacbba)
	⇒ cacbbc

Defines rule #13.

[18] babbcacbbbabbc=cacbbcacbba

Overlap of [14] babbcacbba=cacbbc with [10] aacbba=babbc:

babbcacbb a aacbba

Critical pair: babbcacbbbabbc=cacbbcacbba.

Defines rule #14.