Certificate for #4281 ⟨a, b | abaabbbba=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] abaabbbba=ba

Axiom: abaabbbba=ba.

Referenced by [3], [4], [5], [8].

[2] bbbbba=c

Axiom: bbbbba=c.

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

[3] bba=abaac

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

abaabbbb a abaabbbba

Critical pair: abaabbbbba=babaabbbba.

Reduce LHS:

[2]	abaa(bbbbba)
	⇒ abaac

Reduce RHS:

[1]	b(abaabbbba)
	⇒ bba

Flip LHS and RHS.

Defines rule #1.

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

[4] cbaaabaacbaac=bc

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

bbbbb a abaabbbba

Critical pair: bbbbbba=cbaabbbba.

Reduce LHS:

[2]	b(bbbbba)
	⇒ bc

Reduce RHS:

[3]	cbaabb(bba)
[3]	⇒ cbaa(bba)baac
	⇒ cbaaabaacbaac

Flip LHS and RHS.

Defines rule #8.

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

[5] abaabc=babaac

Overlap of [3] bba=abaac with [1] abaabbbba=ba:

bb a abaabbbba

Critical pair: bbba=abaacbaabbbba.

Reduce LHS:

[3]	b(bba)
	⇒ babaac

Reduce RHS:

[3]	abaacbaabb(bba)
[3]	⇒ abaacbaa(bba)baac
[4]	⇒ abaa(cbaaabaacbaac)
	⇒ abaabc

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] abaacbaabc=babaacbaac

Overlap of [3] bba=abaac with [5] abaabc=babaac:

bb a abaabc

Critical pair: bbbabaac=abaacbaabc.

Reduce LHS:

[3]	b(bba)baac
	⇒ babaacbaac

Flip LHS and RHS.

Referenced by [7].

[7] cbaababaacbaac=bbc

Overlap of [4] cbaaabaacbaac=bc with [4] cbaaabaacbaac=bc:

cbaaabaacbaa c cbaaabaacbaac

Critical pair: cbaaabaacbaabc=bcbaaabaacbaac.

Reduce LHS:

[6]	cbaa(abaacbaabc)
	⇒ cbaababaacbaac

Reduce RHS:

[4]	b(cbaaabaacbaac)
	⇒ bbc

Referenced by [10].

[8] abaaabaacbaac=ba

Overlap of [1] abaabbbba=ba with [3] bba=abaac:

abaabb bba bba

Critical pair: abaabbabaac=ba.

Reduce LHS:

[3]	abaa(bba)baac
	⇒ abaaabaacbaac

Defines rule #6.

[9] babaacbaac=c

Overlap of [2] bbbbba=c with [3] bba=abaac:

bbb bba bba

Critical pair: bbbabaac=c.

Reduce LHS:

[3]	b(bba)baac
	⇒ babaacbaac

Defines rule #5.

Referenced by [10], [12].

[10] bbc=cbaac

Overlap of [7] cbaababaacbaac=bbc with [9] babaacbaac=c:

cbaa babaacbaac babaacbaac

Critical pair: cbaac=bbc.

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

[11] cbaabc=bcbaac

Overlap of [10] bbc=cbaac with [4] cbaaabaacbaac=bc:

bb c cbaaabaacbaac

Critical pair: bbbc=cbaacbaaabaacbaac.

Reduce LHS:

[10]	b(bbc)
	⇒ bcbaac

Reduce RHS:

[4]	cbaa(cbaaabaacbaac)
	⇒ cbaabc

Flip LHS and RHS.

Defines rule #4.

[12] abaacbaacbaac=bc

Overlap of [3] bba=abaac with [9] babaacbaac=c:

b ba babaacbaac

Critical pair: bc=abaacbaacbaac.

Flip LHS and RHS.

Defines rule #7.