Certificate for #24667 ⟨a, b | aa=a, ababbb=ba⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [8].

[2] ababbb=ba

Axiom: ababbb=ba.

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

[3] aba=ba

Overlap of [1] aa=a with [2] ababbb=ba:

a a ababbb

Critical pair: aba=ababbb.

Reduce RHS:

[2]	(ababbb)
	⇒ ba

Defines rule #2.

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

[4] babbb=ba

Overlap of [2] ababbb=ba with [3] aba=ba:

ababbb aba

Critical pair: babbb=ba.

Defines rule #5.

[5] abba=bba

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

ab a aba

Critical pair: abba=baba.

Reduce RHS:

[3]	b(aba)
	⇒ bba

Defines rule #3.

Referenced by [6], [7].

[6] abbba=bbba

Overlap of [3] aba=ba with [5] abba=bba:

ab a abba

Critical pair: abbba=babba.

Reduce RHS:

[5]	b(abba)
	⇒ bbba

Defines rule #4.

Referenced by [8].

[7] abbbba=bbbba

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

abb a abba

Critical pair: abbbba=bbabba.

Reduce RHS:

[5]	bb(abba)
	⇒ bbbba

Referenced by [8].

[8] bbbba=ba

Overlap of [2] ababbb=ba with [6] abbba=bbba:

ab abbb abbba

Critical pair: abbbba=baa.

Reduce LHS:

[7]	(abbbba)
	⇒ bbbba

Reduce RHS:

[1]	b(aa)
	⇒ ba

Defines rule #6.