Certificate for #19797 ⟨a, b | aaa=a, aaba=bbb⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(a) = 1

[1] aaa=a

Axiom: aaa=a.

Defines rule #7.

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

[2] aaba=bbb

Axiom: aaba=bbb.

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

[3] aba=abbb

Overlap of [1] aaa=a with [2] aaba=bbb:

a aa aaba

Critical pair: abbb=aba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [6], [7].

[4] aabbb=bbb

Overlap of [1] aaa=a with [2] aaba=bbb:

aa a aaba

Critical pair: aabbb=aaba.

Reduce RHS:

[2]	(aaba)
	⇒ bbb

Defines rule #4.

Referenced by [6].

[5] bbbaa=bbb

Overlap of [2] aaba=bbb with [1] aaa=a:

aab a aaa

Critical pair: aaba=bbbaa.

Reduce LHS:

[2]	(aaba)
	⇒ bbb

Flip LHS and RHS.

Defines rule #6.

Referenced by [8].

[6] bbbabbb=bbbb

Overlap of [2] aaba=bbb with [2] aaba=bbb:

aab a aaba

Critical pair: aabbbb=bbbaba.

Reduce LHS:

[4]	(aabbb)b
	⇒ bbbb

Reduce RHS:

[3]	bbb(aba)
	⇒ bbbabbb

Flip LHS and RHS.

Defines rule #2.

[7] bbbba=bbbbbb

Overlap of [2] aaba=bbb with [3] aba=abbb:

aab a aba

Critical pair: aababbb=bbbba.

Reduce LHS:

[2]	(aaba)bbb
	⇒ bbbbbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] bbbbbbbb=bbbb

Overlap of [7] bbbba=bbbbbb with [5] bbbaa=bbb:

b bbba bbbaa

Critical pair: bbbb=bbbbbba.

Reduce RHS:

[7]	bb(bbbba)
	⇒ bbbbbbbb

Flip LHS and RHS.

Defines rule #1.