Certificate for #6750 ⟨a, b | aba=a, abbb=ba⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

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

[2] abbb=ba

Axiom: abbb=ba.

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

[3] abba=ba

Overlap of [1] aba=a with [2] abbb=ba:

ab a abbb

Critical pair: abba=abbb.

Reduce RHS:

[2]	(abbb)
	⇒ ba

Referenced by [4].

[4] bba=baa

Overlap of [3] abba=ba with [2] abbb=ba:

abb a abbb

Critical pair: abbba=babbb.

Reduce LHS:

[2]	(abbb)a
	⇒ baa

Reduce RHS:

[2]	b(abbb)
	⇒ bba

Flip LHS and RHS.

Referenced by [5].

[5] baaa=ba

Overlap of [2] abbb=ba with [4] bba=baa:

abb b bba

Critical pair: abbbaa=baba.

Reduce LHS:

[2]	(abbb)aa
	⇒ baaa

Reduce RHS:

[1]	b(aba)
	⇒ ba

Referenced by [6].

[6] aaa=a

Overlap of [1] aba=a with [5] baaa=ba:

a ba baaa

Critical pair: aba=aaa.

Reduce LHS:

[1]	(aba)
	⇒ a

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] ba=aa

Overlap of [6] aaa=a with [2] abbb=ba:

aa a abbb

Critical pair: aaba=abbb.

Reduce LHS:

[1]	a(aba)
	⇒ aa

Reduce RHS:

[2]	(abbb)
	⇒ ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] abbb=aa

Simplify [2] abbb=ba.

Reduce RHS:

[7]	(ba)
	⇒ aa

Defines rule #3.