Certificate for #16130 ⟨a, b | aab=aa, bbaa=ab⟩

Completion settings:

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

[1] aab=aa

Axiom: aab=aa.

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

[2] bbaa=ab

Axiom: bbaa=ab.

Referenced by [3], [4], [5], [6], [8], [9].

[3] abb=ab

Overlap of [2] bbaa=ab with [1] aab=aa:

bb aa aab

Critical pair: bbaa=abb.

Reduce LHS:

[2]	(bbaa)
	⇒ ab

Flip LHS and RHS.

Referenced by [5], [6].

[4] abab=aba

Overlap of [2] bbaa=ab with [1] aab=aa:

bba a aab

Critical pair: bbaaa=abab.

Reduce LHS:

[2]	(bbaa)a
	⇒ aba

Flip LHS and RHS.

Referenced by [6].

[5] abaa=aa

Overlap of [3] abb=ab with [2] bbaa=ab:

a bb bbaa

Critical pair: aab=abaa.

Reduce LHS:

[1]	(aab)
	⇒ aa

Flip LHS and RHS.

Referenced by [6], [7].

[6] aba=aa

Overlap of [3] abb=ab with [2] bbaa=ab:

ab b bbaa

Critical pair: abab=abbaa.

Reduce LHS:

[4]	(abab)
	⇒ aba

Reduce RHS:

[3]	(abb)aa
[5]	⇒ (abaa)
	⇒ aa

Referenced by [7], [8].

[7] aaa=aa

Simplify [5] abaa=aa.

Reduce LHS:

[6]	(aba)a
	⇒ aaa

Defines rule #2.

Referenced by [8].

[8] ab=aa

Overlap of [2] bbaa=ab with [7] aaa=aa:

bb aa aaa

Critical pair: bbaa=aba.

Reduce LHS:

[2]	(bbaa)
	⇒ ab

Reduce RHS:

[6]	(aba)
	⇒ aa

Defines rule #1.

Referenced by [9].

[9] bbaa=aa

Simplify [2] bbaa=ab.

Reduce RHS:

[8]	(ab)
	⇒ aa

Defines rule #3.