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

Completion settings:

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

[1] aabb=aa

Axiom: aabb=aa.

Referenced by [4].

[2] baba=a

Axiom: baba=a.

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

[3] baa=aba

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

ba ba baba

Critical pair: baa=aba.

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

[4] ababb=aba

Overlap of [3] baa=aba with [1] aabb=aa:

b aa aabb

Critical pair: baa=ababb.

Reduce LHS:

[3]	(baa)
	⇒ aba

Flip LHS and RHS.

Referenced by [5].

[5] abb=a

Overlap of [2] baba=a with [4] ababb=aba:

b aba ababb

Critical pair: baba=abb.

Reduce LHS:

[2]	(baba)
	⇒ a

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] aaba=aba

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

ab b baba

Critical pair: aba=aaba.

Flip LHS and RHS.

Referenced by [7].

[7] aa=a

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

b aa aaba

Critical pair: baba=ababa.

Reduce LHS:

[2]	(baba)
	⇒ a

Reduce RHS:

[2]	a(baba)
	⇒ aa

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] aba=ba

Overlap of [3] baa=aba with [7] aa=a:

b aa aa

Critical pair: ba=aba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] bba=a

Overlap of [2] baba=a with [8] aba=ba:

b aba aba

Critical pair: bba=a.

Defines rule #4.