Certificate for #4141 ⟨a, b | aababbbaa=ba⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1
Auxiliary generators:
1. bbba=c

[1] aababbbaa=ba

Axiom: aababbbaa=ba.

Referenced by [3].

[2] bbba=c

Axiom: bbba=c.

Defines rule #10.

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

[3] aabaca=ba

Overlap of [1] aababbbaa=ba with [2] bbba=c:

aaba bbbaa bbba

Critical pair: aabaca=ba.

Defines rule #1.

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

[4] cabaca=bc

Overlap of [2] bbba=c with [3] aabaca=ba:

bbb a aabaca

Critical pair: bbbba=cabaca.

Reduce LHS:

[2]	b(bbba)
	⇒ bc

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7], [8], [10], [13], [14], [16].

[5] aabacba=bba

Overlap of [3] aabaca=ba with [3] aabaca=ba:

aabac a aabaca

Critical pair: aabacba=baabaca.

Reduce RHS:

[3]	b(aabaca)
	⇒ bba

Defines rule #4.

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

[6] babaca=aababc

Overlap of [3] aabaca=ba with [4] cabaca=bc:

aaba ca cabaca

Critical pair: aababc=babaca.

Flip LHS and RHS.

Defines rule #7.

Referenced by [15].

[7] bbc=cabacba

Overlap of [4] cabaca=bc with [3] aabaca=ba:

cabac a aabaca

Critical pair: cabacba=bcabaca.

Reduce RHS:

[4]	b(cabaca)
	⇒ bbc

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[8] bcbaca=cababc

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

caba ca cabaca

Critical pair: cababc=bcbaca.

Flip LHS and RHS.

Defines rule #8.

[9] aabacbba=c

Overlap of [3] aabaca=ba with [5] aabacba=bba:

aabac a aabacba

Critical pair: aabacbba=baabacba.

Reduce RHS:

[5]	b(aabacba)
[2]	⇒ (bbba)
	⇒ c

Defines rule #11.

Referenced by [14].

[10] bcabacba=cabacbba

Overlap of [4] cabaca=bc with [5] aabacba=bba:

cabac a aabacba

Critical pair: cabacbba=bcabacba.

Flip LHS and RHS.

Defines rule #12.

[11] aabacc=bc

Overlap of [5] aabacba=bba with [5] aabacba=bba:

aabacb a aabacba

Critical pair: aabacbbba=bbaabacba.

Reduce LHS:

[2]	aabac(bbba)
	⇒ aabacc

Reduce RHS:

[5]	bb(aabacba)
[2]	⇒ b(bbba)
	⇒ bc

Defines rule #3.

Referenced by [12], [13].

[12] aabacbc=cabacba

Overlap of [3] aabaca=ba with [11] aabacc=bc:

aabac a aabacc

Critical pair: aabacbc=baabacc.

Reduce RHS:

[11]	b(aabacc)
[7]	⇒ (bbc)
	⇒ cabacba

Defines rule #6.

Referenced by [16].

[13] bcabacc=cabacbc

Overlap of [4] cabaca=bc with [11] aabacc=bc:

cabac a aabacc

Critical pair: cabacbc=bcabacc.

Flip LHS and RHS.

Defines rule #9.

[14] bcabacbba=cabacc

Overlap of [4] cabaca=bc with [9] aabacbba=c:

cabac a aabacbba

Critical pair: cabacc=bcabacbba.

Flip LHS and RHS.

Defines rule #14.

[15] bbaababc=cbaca

Overlap of [2] bbba=c with [6] babaca=aababc:

bb ba babaca

Critical pair: bbaababc=cbaca.

Defines rule #15.

[16] bcabacbc=cabaccabacba

Overlap of [4] cabaca=bc with [12] aabacbc=cabacba:

cabac a aabacbc

Critical pair: cabaccabacba=bcabacbc.

Flip LHS and RHS.

Defines rule #13.