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

Axiom: aababbbba=ba.

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

[2] bbbbba=c

Axiom: bbbbba=c.

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

[3] bba=aabac

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

aababbbb a aababbbba

Critical pair: aababbbbba=baababbbba.

Reduce LHS:

[2]	aaba(bbbbba)
	⇒ aabac

Reduce RHS:

[1]	b(aababbbba)
	⇒ bba

Flip LHS and RHS.

Defines rule #1.

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

[4] cabaaabacabac=bc

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

bbbbb a aababbbba

Critical pair: bbbbbba=cababbbba.

Reduce LHS:

[2]	b(bbbbba)
	⇒ bc

Reduce RHS:

[3]	cababb(bba)
[3]	⇒ caba(bba)abac
	⇒ cabaaabacabac

Flip LHS and RHS.

Defines rule #8.

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

[5] aababc=baabac

Overlap of [3] bba=aabac with [1] aababbbba=ba:

bb a aababbbba

Critical pair: bbba=aabacababbbba.

Reduce LHS:

[3]	b(bba)
	⇒ baabac

Reduce RHS:

[3]	aabacababb(bba)
[3]	⇒ aabacaba(bba)abac
[4]	⇒ aaba(cabaaabacabac)
	⇒ aababc

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] aabacababc=baabacabac

Overlap of [3] bba=aabac with [5] aababc=baabac:

bb a aababc

Critical pair: bbbaabac=aabacababc.

Reduce LHS:

[3]	b(bba)abac
	⇒ baabacabac

Flip LHS and RHS.

Referenced by [7].

[7] cababaabacabac=bbc

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

cabaaabacaba c cabaaabacabac

Critical pair: cabaaabacababc=bcabaaabacabac.

Reduce LHS:

[6]	caba(aabacababc)
	⇒ cababaabacabac

Reduce RHS:

[4]	b(cabaaabacabac)
	⇒ bbc

Referenced by [10].

[8] aabaaabacabac=ba

Overlap of [1] aababbbba=ba with [3] bba=aabac:

aababb bba bba

Critical pair: aababbaabac=ba.

Reduce LHS:

[3]	aaba(bba)abac
	⇒ aabaaabacabac

Defines rule #6.

[9] baabacabac=c

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

bbb bba bba

Critical pair: bbbaabac=c.

Reduce LHS:

[3]	b(bba)abac
	⇒ baabacabac

Defines rule #5.

Referenced by [10], [12].

[10] bbc=cabac

Overlap of [7] cababaabacabac=bbc with [9] baabacabac=c:

caba baabacabac baabacabac

Critical pair: cabac=bbc.

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

[11] cababc=bcabac

Overlap of [10] bbc=cabac with [4] cabaaabacabac=bc:

bb c cabaaabacabac

Critical pair: bbbc=cabacabaaabacabac.

Reduce LHS:

[10]	b(bbc)
	⇒ bcabac

Reduce RHS:

[4]	caba(cabaaabacabac)
	⇒ cababc

Flip LHS and RHS.

Defines rule #4.

[12] aabacabacabac=bc

Overlap of [3] bba=aabac with [9] baabacabac=c:

b ba baabacabac

Critical pair: bc=aabacabacabac.

Flip LHS and RHS.

Defines rule #7.