Certificate for #4137 ⟨a, b | aababbaba=ba⟩

Completion settings:

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

[1] aababbaba=ba

Axiom: aababbaba=ba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #2.

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

[3] aabacba=ba

Overlap of [1] aababbaba=ba with [2] bba=c:

aaba bbaba bba

Critical pair: aabacba=ba.

Defines rule #4.

Referenced by [4], [5], [7].

[4] cabacba=bc

Overlap of [2] bba=c with [3] aabacba=ba:

bb a aabacba

Critical pair: bbba=cabacba.

Reduce LHS:

[2]	b(bba)
	⇒ bc

Flip LHS and RHS.

Defines rule #6.

[5] aabacc=c

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

aabacb a aabacba

Critical pair: aabacbba=baabacba.

Reduce LHS:

[2]	aabac(bba)
	⇒ aabacc

Reduce RHS:

[3]	b(aabacba)
[2]	⇒ (bba)
	⇒ c

Defines rule #1.

Referenced by [6], [7].

[6] bbc=cabacc

Overlap of [2] bba=c with [5] aabacc=c:

bb a aabacc

Critical pair: bbc=cabacc.

Defines rule #3.

Referenced by [8].

[7] aabacbc=bc

Overlap of [3] aabacba=ba with [5] aabacc=c:

aabacb a aabacc

Critical pair: aabacbc=baabacc.

Reduce RHS:

[5]	b(aabacc)
	⇒ bc

Defines rule #5.

Referenced by [8].

[8] cabacbc=bcabacc

Overlap of [2] bba=c with [7] aabacbc=bc:

bb a aabacbc

Critical pair: bbbc=cabacbc.

Reduce LHS:

[6]	b(bbc)
	⇒ bcabacc

Flip LHS and RHS.

Defines rule #7.