Certificate for #16350 ⟨a, b | aba=aa, aabb=ba⟩

Completion settings:

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

[1] aba=aa

Axiom: aba=aa.

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

[2] aabb=ba

Axiom: aabb=ba.

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

[3] abba=aa

Overlap of [1] aba=aa with [2] aabb=ba:

ab a aabb

Critical pair: abba=aaabb.

Reduce RHS:

[2]	a(aabb)
[1]	⇒ (aba)
	⇒ aa

Referenced by [4].

[4] baa=aaa

Overlap of [1] aba=aa with [3] abba=aa:

ab a abba

Critical pair: abaa=aabba.

Reduce LHS:

[1]	(aba)a
	⇒ aaa

Reduce RHS:

[2]	(aabb)a
	⇒ baa

Flip LHS and RHS.

Referenced by [5], [6].

[5] aaaa=aaa

Overlap of [1] aba=aa with [4] baa=aaa:

a ba baa

Critical pair: aaaa=aaa.

Referenced by [6].

[6] aaa=aa

Overlap of [4] baa=aaa with [2] aabb=ba:

ba a aabb

Critical pair: baba=aaaabb.

Reduce LHS:

[1]	b(aba)
[4]	⇒ (baa)
	⇒ aaa

Reduce RHS:

[5]	(aaaa)bb
[2]	⇒ a(aabb)
[1]	⇒ (aba)
	⇒ aa

Defines rule #2.

Referenced by [7].

[7] ba=aa

Overlap of [6] aaa=aa with [2] aabb=ba:

a aa aabb

Critical pair: aba=aabb.

Reduce LHS:

[1]	(aba)
	⇒ aa

Reduce RHS:

[2]	(aabb)
	⇒ ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] aabb=aa

Simplify [2] aabb=ba.

Reduce RHS:

[7]	(ba)
	⇒ aa

Defines rule #3.