Certificate for #4293 ⟨a, b | ababaabba=ba⟩

Completion settings:

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

[1] ababaabba=ba

Axiom: ababaabba=ba.

Defines rule #6.

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

[2] bbbba=c

Axiom: bbbba=c.

Referenced by [4], [6], [7], [8], [10], [14].

[3] ababaabbba=bba

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

ababaabb a ababaabba

Critical pair: ababaabbba=bababaabba.

Reduce RHS:

[1]	b(ababaabba)
	⇒ bba

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

[4] cbabaabba=bc

Overlap of [2] bbbba=c with [1] ababaabba=ba:

bbbb a ababaabba

Critical pair: bbbbba=cbabaabba.

Reduce LHS:

[2]	b(bbbba)
	⇒ bc

Flip LHS and RHS.

Defines rule #10.

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

[5] cbabaabbba=bbc

Overlap of [4] cbabaabba=bc with [1] ababaabba=ba:

cbabaabb a ababaabba

Critical pair: cbabaabbba=bcbabaabba.

Reduce RHS:

[4]	b(cbabaabba)
	⇒ bbc

Referenced by [8], [13].

[6] bbba=ababaac

Overlap of [1] ababaabba=ba with [3] ababaabbba=bba:

ababaabb a ababaabbba

Critical pair: ababaabbbba=bababaabbba.

Reduce LHS:

[2]	ababaa(bbbba)
	⇒ ababaac

Reduce RHS:

[3]	b(ababaabbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

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

[7] ababaabc=c

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

ababaabbb a ababaabbba

Critical pair: ababaabbbbba=bbababaabbba.

Reduce LHS:

[2]	ababaab(bbbba)
	⇒ ababaabc

Reduce RHS:

[3]	bb(ababaabbba)
[2]	⇒ (bbbba)
	⇒ c

Defines rule #4.

Referenced by [9], [10], [11], [12].

[8] bbbc=cbabaac

Overlap of [4] cbabaabba=bc with [3] ababaabbba=bba:

cbabaabb a ababaabbba

Critical pair: cbabaabbbba=bcbabaabbba.

Reduce LHS:

[2]	cbabaa(bbbba)
	⇒ cbabaac

Reduce RHS:

[5]	b(cbabaabbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] ababaabbc=bc

Overlap of [1] ababaabba=ba with [7] ababaabc=c:

ababaabb a ababaabc

Critical pair: ababaabbc=bababaabc.

Reduce RHS:

[7]	b(ababaabc)
	⇒ bc

Defines rule #7.

[10] cbabaabc=bcbabaac

Overlap of [2] bbbba=c with [7] ababaabc=c:

bbbb a ababaabc

Critical pair: bbbbc=cbabaabc.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcbabaac

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[11] ababaacbabaac=bbc

Overlap of [3] ababaabbba=bba with [7] ababaabc=c:

ababaabbb a ababaabc

Critical pair: ababaabbbc=bbababaabc.

Reduce LHS:

[8]	ababaa(bbbc)
	⇒ ababaacbabaac

Reduce RHS:

[7]	bb(ababaabc)
	⇒ bbc

Defines rule #9.

[12] cbabaabbc=bbcbabaac

Overlap of [4] cbabaabba=bc with [7] ababaabc=c:

cbabaabb a ababaabc

Critical pair: cbabaabbc=bcbabaabc.

Reduce RHS:

[10]	b(cbabaabc)
	⇒ bbcbabaac

Defines rule #11.

[13] cbabaaababaac=bbc

Simplify [5] cbabaabbba=bbc.

Reduce LHS:

[6]	cbabaa(bbba)
	⇒ cbabaaababaac

Defines rule #12.

[14] bababaac=c

Overlap of [2] bbbba=c with [6] bbba=ababaac:

b bbba bbba

Critical pair: bababaac=c.

Defines rule #3.

[15] ababaaababaac=bba

Overlap of [3] ababaabbba=bba with [6] bbba=ababaac:

ababaa bbba bbba

Critical pair: ababaaababaac=bba.

Defines rule #8.