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

Axiom: aabbabbba=ba.

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

[2] bbbbba=c

Axiom: bbbbba=c.

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

[3] aabbabbbba=bba

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

aabbabbb a aabbabbba

Critical pair: aabbabbbba=baabbabbba.

Reduce RHS:

[1]	b(aabbabbba)
	⇒ bba

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

[4] cabbabbba=bc

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

bbbbb a aabbabbba

Critical pair: bbbbbba=cabbabbba.

Reduce LHS:

[2]	b(bbbbba)
	⇒ bc

Flip LHS and RHS.

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

[5] cabbabbbba=bbc

Overlap of [4] cabbabbba=bc with [1] aabbabbba=ba:

cabbabbb a aabbabbba

Critical pair: cabbabbbba=bcabbabbba.

Reduce RHS:

[4]	b(cabbabbba)
	⇒ bbc

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

[6] bbba=aabbac

Overlap of [1] aabbabbba=ba with [3] aabbabbbba=bba:

aabbabbb a aabbabbbba

Critical pair: aabbabbbbba=baabbabbbba.

Reduce LHS:

[2]	aabba(bbbbba)
	⇒ aabbac

Reduce RHS:

[3]	b(aabbabbbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

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

[7] aabbabc=baabbac

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

aabbabbbb a aabbabbbba

Critical pair: aabbabbbbbba=bbaabbabbbba.

Reduce LHS:

[2]	aabbab(bbbbba)
	⇒ aabbabc

Reduce RHS:

[3]	bb(aabbabbbba)
[6]	⇒ b(bbba)
	⇒ baabbac

Defines rule #3.

Referenced by [14].

[8] bbbc=cabbac

Overlap of [4] cabbabbba=bc with [3] aabbabbbba=bba:

cabbabbb a aabbabbbba

Critical pair: cabbabbbbba=bcabbabbbba.

Reduce LHS:

[2]	cabba(bbbbba)
	⇒ cabbac

Reduce RHS:

[5]	b(cabbabbbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] aabbabbc=c

Overlap of [6] bbba=aabbac with [3] aabbabbbba=bba:

bbb a aabbabbbba

Critical pair: bbbbba=aabbacabbabbbba.

Reduce LHS:

[2]	(bbbbba)
	⇒ c

Reduce RHS:

[5]	aabba(cabbabbbba)
	⇒ aabbabbc

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [14].

[10] aabbacabbac=bc

Overlap of [9] aabbabbc=c with [4] cabbabbba=bc:

aabbabb c cabbabbba

Critical pair: aabbabbbc=cabbabbba.

Reduce LHS:

[8]	aabba(bbbc)
	⇒ aabbacabbac

Reduce RHS:

[4]	(cabbabbba)
	⇒ bc

Defines rule #8.

Referenced by [13].

[11] cabbabc=bcabbac

Overlap of [8] bbbc=cabbac with [4] cabbabbba=bc:

bbb c cabbabbba

Critical pair: bbbbc=cabbacabbabbba.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcabbac

Reduce RHS:

[4]	cabba(cabbabbba)
	⇒ cabbabc

Flip LHS and RHS.

Defines rule #4.

[12] cabbabaabbac=bbc

Simplify [5] cabbabbbba=bbc.

Reduce LHS:

[6]	cabbab(bbba)
	⇒ cabbabaabbac

Defines rule #12.

Referenced by [13].

[13] cabbabbc=bbcabbac

Overlap of [12] cabbabaabbac=bbc with [10] aabbacabbac=bc:

cabbab aabbac aabbacabbac

Critical pair: cabbabbc=bbcabbac.

Defines rule #9.

[14] bbaabbac=c

Overlap of [7] aabbabc=baabbac with [4] cabbabbba=bc:

aabbab c cabbabbba

Critical pair: aabbabbc=baabbacabbabbba.

Reduce LHS:

[9]	(aabbabbc)
	⇒ c

Reduce RHS:

[4]	baabba(cabbabbba)
[7]	⇒ b(aabbabc)
	⇒ bbaabbac

Flip LHS and RHS.

Defines rule #5.

[15] aabbaaabbac=ba

Overlap of [1] aabbabbba=ba with [6] bbba=aabbac:

aabba bbba bbba

Critical pair: aabbaaabbac=ba.

Defines rule #7.

[16] aabbabaabbac=bba

Overlap of [3] aabbabbbba=bba with [6] bbba=aabbac:

aabbab bbba bbba

Critical pair: aabbabaabbac=bba.

Defines rule #11.

[17] cabbaaabbac=bc

Overlap of [4] cabbabbba=bc with [6] bbba=aabbac:

cabba bbba bbba

Critical pair: cabbaaabbac=bc.

Defines rule #10.