Certificate for #4269 ⟨a, b | abaababba=ba⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1
Auxiliary generators:
1. bbbba=c

[1] abaababba=ba

Axiom: abaababba=ba.

Defines rule #6.

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

[2] bbbba=c

Axiom: bbbba=c.

Referenced by [4], [6], [7], [8], [10], [14].

[3] abaababbba=bba

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

abaababb a abaababba

Critical pair: abaababbba=babaababba.

Reduce RHS:

[1]	b(abaababba)
	⇒ bba

Referenced by [6], [7], [8], [11], [15].

[4] cbaababba=bc

Overlap of [2] bbbba=c with [1] abaababba=ba:

bbbb a abaababba

Critical pair: bbbbba=cbaababba.

Reduce LHS:

[2]	b(bbbba)
	⇒ bc

Flip LHS and RHS.

Defines rule #10.

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

[5] cbaababbba=bbc

Overlap of [4] cbaababba=bc with [1] abaababba=ba:

cbaababb a abaababba

Critical pair: cbaababbba=bcbaababba.

Reduce RHS:

[4]	b(cbaababba)
	⇒ bbc

Referenced by [8], [13].

[6] bbba=abaabac

Overlap of [1] abaababba=ba with [3] abaababbba=bba:

abaababb a abaababbba

Critical pair: abaababbbba=babaababbba.

Reduce LHS:

[2]	abaaba(bbbba)
	⇒ abaabac

Reduce RHS:

[3]	b(abaababbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [14], [15].

[7] abaababc=c

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

abaababbb a abaababbba

Critical pair: abaababbbbba=bbabaababbba.

Reduce LHS:

[2]	abaabab(bbbba)
	⇒ abaababc

Reduce RHS:

[3]	bb(abaababbba)
[2]	⇒ (bbbba)
	⇒ c

Defines rule #4.

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

[8] bbbc=cbaabac

Overlap of [4] cbaababba=bc with [3] abaababbba=bba:

cbaababb a abaababbba

Critical pair: cbaababbbba=bcbaababbba.

Reduce LHS:

[2]	cbaaba(bbbba)
	⇒ cbaabac

Reduce RHS:

[5]	b(cbaababbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] abaababbc=bc

Overlap of [1] abaababba=ba with [7] abaababc=c:

abaababb a abaababc

Critical pair: abaababbc=babaababc.

Reduce RHS:

[7]	b(abaababc)
	⇒ bc

Defines rule #7.

[10] cbaababc=bcbaabac

Overlap of [2] bbbba=c with [7] abaababc=c:

bbbb a abaababc

Critical pair: bbbbc=cbaababc.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcbaabac

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[11] abaabacbaabac=bbc

Overlap of [3] abaababbba=bba with [7] abaababc=c:

abaababbb a abaababc

Critical pair: abaababbbc=bbabaababc.

Reduce LHS:

[8]	abaaba(bbbc)
	⇒ abaabacbaabac

Reduce RHS:

[7]	bb(abaababc)
	⇒ bbc

Defines rule #9.

[12] cbaababbc=bbcbaabac

Overlap of [4] cbaababba=bc with [7] abaababc=c:

cbaababb a abaababc

Critical pair: cbaababbc=bcbaababc.

Reduce RHS:

[10]	b(cbaababc)
	⇒ bbcbaabac

Defines rule #11.

[13] cbaabaabaabac=bbc

Simplify [5] cbaababbba=bbc.

Reduce LHS:

[6]	cbaaba(bbba)
	⇒ cbaabaabaabac

Defines rule #12.

[14] babaabac=c

Overlap of [2] bbbba=c with [6] bbba=abaabac:

b bbba bbba

Critical pair: babaabac=c.

Defines rule #3.

[15] abaabaabaabac=bba

Overlap of [3] abaababbba=bba with [6] bbba=abaabac:

abaaba bbba bbba

Critical pair: abaabaabaabac=bba.

Defines rule #8.