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

Axiom: abababbba=ba.

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

[2] bbbbba=c

Axiom: bbbbba=c.

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

[3] abababbbba=bba

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

abababbb a abababbba

Critical pair: abababbbba=babababbba.

Reduce RHS:

[1]	b(abababbba)
	⇒ bba

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

[4] cbababbba=bc

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

bbbbb a abababbba

Critical pair: bbbbbba=cbababbba.

Reduce LHS:

[2]	b(bbbbba)
	⇒ bc

Flip LHS and RHS.

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

[5] cbababbbba=bbc

Overlap of [4] cbababbba=bc with [1] abababbba=ba:

cbababbb a abababbba

Critical pair: cbababbbba=bcbababbba.

Reduce RHS:

[4]	b(cbababbba)
	⇒ bbc

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

[6] bbba=ababac

Overlap of [1] abababbba=ba with [3] abababbbba=bba:

abababbb a abababbbba

Critical pair: abababbbbba=babababbbba.

Reduce LHS:

[2]	ababa(bbbbba)
	⇒ ababac

Reduce RHS:

[3]	b(abababbbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

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

[7] abababc=bababac

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

abababbbb a abababbbba

Critical pair: abababbbbbba=bbabababbbba.

Reduce LHS:

[2]	ababab(bbbbba)
	⇒ abababc

Reduce RHS:

[3]	bb(abababbbba)
[6]	⇒ b(bbba)
	⇒ bababac

Defines rule #3.

Referenced by [14].

[8] bbbc=cbabac

Overlap of [4] cbababbba=bc with [3] abababbbba=bba:

cbababbb a abababbbba

Critical pair: cbababbbbba=bcbababbbba.

Reduce LHS:

[2]	cbaba(bbbbba)
	⇒ cbabac

Reduce RHS:

[5]	b(cbababbbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] abababbc=c

Overlap of [6] bbba=ababac with [3] abababbbba=bba:

bbb a abababbbba

Critical pair: bbbbba=ababacbababbbba.

Reduce LHS:

[2]	(bbbbba)
	⇒ c

Reduce RHS:

[5]	ababa(cbababbbba)
	⇒ abababbc

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [14].

[10] ababacbabac=bc

Overlap of [9] abababbc=c with [4] cbababbba=bc:

abababb c cbababbba

Critical pair: abababbbc=cbababbba.

Reduce LHS:

[8]	ababa(bbbc)
	⇒ ababacbabac

Reduce RHS:

[4]	(cbababbba)
	⇒ bc

Defines rule #8.

Referenced by [13].

[11] cbababc=bcbabac

Overlap of [8] bbbc=cbabac with [4] cbababbba=bc:

bbb c cbababbba

Critical pair: bbbbc=cbabacbababbba.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcbabac

Reduce RHS:

[4]	cbaba(cbababbba)
	⇒ cbababc

Flip LHS and RHS.

Defines rule #4.

[12] cbababababac=bbc

Simplify [5] cbababbbba=bbc.

Reduce LHS:

[6]	cbabab(bbba)
	⇒ cbababababac

Defines rule #12.

Referenced by [13].

[13] cbababbc=bbcbabac

Overlap of [12] cbababababac=bbc with [10] ababacbabac=bc:

cbabab ababac ababacbabac

Critical pair: cbababbc=bbcbabac.

Defines rule #9.

[14] bbababac=c

Overlap of [7] abababc=bababac with [4] cbababbba=bc:

ababab c cbababbba

Critical pair: abababbc=bababacbababbba.

Reduce LHS:

[9]	(abababbc)
	⇒ c

Reduce RHS:

[4]	bababa(cbababbba)
[7]	⇒ b(abababc)
	⇒ bbababac

Flip LHS and RHS.

Defines rule #5.

[15] ababaababac=ba

Overlap of [1] abababbba=ba with [6] bbba=ababac:

ababa bbba bbba

Critical pair: ababaababac=ba.

Defines rule #7.

[16] abababababac=bba

Overlap of [3] abababbbba=bba with [6] bbba=ababac:

ababab bbba bbba

Critical pair: abababababac=bba.

Defines rule #11.

[17] cbabaababac=bc

Overlap of [4] cbababbba=bc with [6] bbba=ababac:

cbaba bbba bbba

Critical pair: cbabaababac=bc.

Defines rule #10.