Certificate for #4737 ⟨a, b | aabb=a, baba=a⟩

Completion settings:

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

[1] aabb=a

Axiom: aabb=a.

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

[2] baba=a

Axiom: baba=a.

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

[3] aba=baa

Overlap of [2] baba=a with [2] baba=a:

ba ba baba

Critical pair: baa=aba.

Flip LHS and RHS.

Defines rule #2.

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

[4] abbaa=aa

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

ab a aba

Critical pair: abbaa=baaba.

Reduce RHS:

[3]	ba(aba)
[2]	⇒ (baba)a
	⇒ aa

Referenced by [5].

[5] abba=a

Overlap of [4] abbaa=aa with [1] aabb=a:

abb aa aabb

Critical pair: abba=aabb.

Reduce RHS:

[1]	(aabb)
	⇒ a

Referenced by [6].

[6] abbbaa=baa

Overlap of [5] abba=a with [3] aba=baa:

abb a aba

Critical pair: abbbaa=aba.

Reduce RHS:

[3]	(aba)
	⇒ baa

Referenced by [7].

[7] abbba=ba

Overlap of [6] abbbaa=baa with [1] aabb=a:

abbb aa aabb

Critical pair: abbba=baabb.

Reduce RHS:

[1]	b(aabb)
	⇒ ba

Referenced by [8], [9].

[8] abbbbaa=a

Overlap of [7] abbba=ba with [3] aba=baa:

abbb a aba

Critical pair: abbbbaa=baba.

Reduce RHS:

[2]	(baba)
	⇒ a

Referenced by [10].

[9] abbbba=bba

Overlap of [7] abbba=ba with [7] abbba=ba:

abbb a abbba

Critical pair: abbbba=babbba.

Reduce RHS:

[7]	b(abbba)
	⇒ bba

Referenced by [10].

[10] bbaa=a

Simplify [8] abbbbaa=a.

Reduce LHS:

[9]	(abbbba)a
	⇒ bbaa

Defines rule #3.

Referenced by [11].

[11] abb=bba

Overlap of [10] bbaa=a with [1] aabb=a:

bb aa aabb

Critical pair: bba=abb.

Flip LHS and RHS.

Defines rule #1.