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

Axiom: aabababba=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] aabababbba=bba

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

aabababb a aabababba

Critical pair: aabababbba=baabababba.

Reduce RHS:

[1]	b(aabababba)
	⇒ bba

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

[4] cabababba=bc

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

bbbb a aabababba

Critical pair: bbbbba=cabababba.

Reduce LHS:

[2]	b(bbbba)
	⇒ bc

Flip LHS and RHS.

Defines rule #10.

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

[5] cabababbba=bbc

Overlap of [4] cabababba=bc with [1] aabababba=ba:

cabababb a aabababba

Critical pair: cabababbba=bcabababba.

Reduce RHS:

[4]	b(cabababba)
	⇒ bbc

Referenced by [8], [13].

[6] bbba=aababac

Overlap of [1] aabababba=ba with [3] aabababbba=bba:

aabababb a aabababbba

Critical pair: aabababbbba=baabababbba.

Reduce LHS:

[2]	aababa(bbbba)
	⇒ aababac

Reduce RHS:

[3]	b(aabababbba)
	⇒ bbba

Flip LHS and RHS.

Defines rule #1.

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

[7] aabababc=c

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

aabababbb a aabababbba

Critical pair: aabababbbbba=bbaabababbba.

Reduce LHS:

[2]	aababab(bbbba)
	⇒ aabababc

Reduce RHS:

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

Defines rule #4.

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

[8] bbbc=cababac

Overlap of [4] cabababba=bc with [3] aabababbba=bba:

cabababb a aabababbba

Critical pair: cabababbbba=bcabababbba.

Reduce LHS:

[2]	cababa(bbbba)
	⇒ cababac

Reduce RHS:

[5]	b(cabababbba)
	⇒ bbbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[9] aabababbc=bc

Overlap of [1] aabababba=ba with [7] aabababc=c:

aabababb a aabababc

Critical pair: aabababbc=baabababc.

Reduce RHS:

[7]	b(aabababc)
	⇒ bc

Defines rule #7.

[10] cabababc=bcababac

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

bbbb a aabababc

Critical pair: bbbbc=cabababc.

Reduce LHS:

[8]	b(bbbc)
	⇒ bcababac

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[11] aababacababac=bbc

Overlap of [3] aabababbba=bba with [7] aabababc=c:

aabababbb a aabababc

Critical pair: aabababbbc=bbaabababc.

Reduce LHS:

[8]	aababa(bbbc)
	⇒ aababacababac

Reduce RHS:

[7]	bb(aabababc)
	⇒ bbc

Defines rule #9.

[12] cabababbc=bbcababac

Overlap of [4] cabababba=bc with [7] aabababc=c:

cabababb a aabababc

Critical pair: cabababbc=bcabababc.

Reduce RHS:

[10]	b(cabababc)
	⇒ bbcababac

Defines rule #11.

[13] cababaaababac=bbc

Simplify [5] cabababbba=bbc.

Reduce LHS:

[6]	cababa(bbba)
	⇒ cababaaababac

Defines rule #12.

[14] baababac=c

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

b bbba bbba

Critical pair: baababac=c.

Defines rule #3.

[15] aababaaababac=bba

Overlap of [3] aabababbba=bba with [6] bbba=aababac:

aababa bbba bbba

Critical pair: aababaaababac=bba.

Defines rule #8.