Certificate for #4338 ⟨a, b | abbaabbba=ba⟩

Completion settings:

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

[1] abbaabbba=ba

Axiom: abbaabbba=ba.

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

[2] bbbbba=c

Axiom: bbbbba=c.

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

[3] abbaabbbba=bba

Overlap of [1] abbaabbba=ba with [1] abbaabbba=ba:

abbaabbb a abbaabbba

Critical pair: abbaabbbba=babbaabbba.

Reduce RHS:

[1]	b(abbaabbba)
	⇒ bba

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

[4] cbbaabbba=bc

Overlap of [2] bbbbba=c with [1] abbaabbba=ba:

bbbbb a abbaabbba

Critical pair: bbbbbba=cbbaabbba.

Reduce LHS:

[2]	b(bbbbba)
	⇒ bc

Flip LHS and RHS.

Referenced by [5], [8], [10], [11], [14], [17].

[5] cbbaabbbba=bbc

Overlap of [4] cbbaabbba=bc with [1] abbaabbba=ba:

cbbaabbb a abbaabbba

Critical pair: cbbaabbbba=bcbbaabbba.

Reduce RHS:

[4]	b(cbbaabbba)
	⇒ bbc

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

[6] bbba=abbaac

Overlap of [1] abbaabbba=ba with [3] abbaabbbba=bba:

abbaabbb a abbaabbbba

Critical pair: abbaabbbbba=babbaabbbba.

Reduce LHS:

[2]	abbaa(bbbbba)
	⇒ abbaac

Reduce RHS:

[3]	b(abbaabbbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [9], [12], [15], [16], [17].

[7] abbaabc=babbaac

Overlap of [3] abbaabbbba=bba with [3] abbaabbbba=bba:

abbaabbbb a abbaabbbba

Critical pair: abbaabbbbbba=bbabbaabbbba.

Reduce LHS:

[2]	abbaab(bbbbba)
	⇒ abbaabc

Reduce RHS:

[3]	bb(abbaabbbba)
[6]	⇒ b(bbba)
	⇒ babbaac

Defines rule #3.

Referenced by [14].

[8] bbbc=cbbaac

Overlap of [4] cbbaabbba=bc with [3] abbaabbbba=bba:

cbbaabbb a abbaabbbba

Critical pair: cbbaabbbbba=bcbbaabbbba.

Reduce LHS:

[2]	cbbaa(bbbbba)
	⇒ cbbaac

Reduce RHS:

[5]	b(cbbaabbbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] abbaabbc=c

Overlap of [6] bbba=abbaac with [3] abbaabbbba=bba:

bbb a abbaabbbba

Critical pair: bbbbba=abbaacbbaabbbba.

Reduce LHS:

[2]	(bbbbba)
	⇒ c

Reduce RHS:

[5]	abbaa(cbbaabbbba)
	⇒ abbaabbc

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [14].

[10] abbaacbbaac=bc

Overlap of [9] abbaabbc=c with [4] cbbaabbba=bc:

abbaabb c cbbaabbba

Critical pair: abbaabbbc=cbbaabbba.

Reduce LHS:

[8]	abbaa(bbbc)
	⇒ abbaacbbaac

Reduce RHS:

[4]	(cbbaabbba)
	⇒ bc

Defines rule #8.

Referenced by [13].

[11] cbbaabc=bcbbaac

Overlap of [8] bbbc=cbbaac with [4] cbbaabbba=bc:

bbb c cbbaabbba

Critical pair: bbbbc=cbbaacbbaabbba.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcbbaac

Reduce RHS:

[4]	cbbaa(cbbaabbba)
	⇒ cbbaabc

Flip LHS and RHS.

Defines rule #4.

[12] cbbaababbaac=bbc

Simplify [5] cbbaabbbba=bbc.

Reduce LHS:

[6]	cbbaab(bbba)
	⇒ cbbaababbaac

Defines rule #12.

Referenced by [13].

[13] cbbaabbc=bbcbbaac

Overlap of [12] cbbaababbaac=bbc with [10] abbaacbbaac=bc:

cbbaab abbaac abbaacbbaac

Critical pair: cbbaabbc=bbcbbaac.

Defines rule #9.

[14] bbabbaac=c

Overlap of [7] abbaabc=babbaac with [4] cbbaabbba=bc:

abbaab c cbbaabbba

Critical pair: abbaabbc=babbaacbbaabbba.

Reduce LHS:

[9]	(abbaabbc)
	⇒ c

Reduce RHS:

[4]	babbaa(cbbaabbba)
[7]	⇒ b(abbaabc)
	⇒ bbabbaac

Flip LHS and RHS.

Defines rule #5.

[15] abbaaabbaac=ba

Overlap of [1] abbaabbba=ba with [6] bbba=abbaac:

abbaa bbba bbba

Critical pair: abbaaabbaac=ba.

Defines rule #7.

[16] abbaababbaac=bba

Overlap of [3] abbaabbbba=bba with [6] bbba=abbaac:

abbaab bbba bbba

Critical pair: abbaababbaac=bba.

Defines rule #11.

[17] cbbaaabbaac=bc

Overlap of [4] cbbaabbba=bc with [6] bbba=abbaac:

cbbaa bbba bbba

Critical pair: cbbaaabbaac=bc.

Defines rule #10.