is automatic, a simple proof
is particularly nice to analyze due to the uniqueness of the Garside normal form.
The Garside normal form is unique in , and is in the form , such that , and .
For any word , the Garside normal form is unique up to elements in and does not have a factor of . Now we show that there is only one way to write .
Every must be in this form. If for some , , then , which is a contradiction because doesn't have a factor of .
Every word in that form is also in , and without factor.
It's impossible to rewrite any word in this form with the relations . Therefore this form is unique.
The Garside normal form of is regular.
Let , then generates . The Garside normal form is a regular language over because they exist an explicit regular expression that matches it.
where and is the same except the and are switched.
Let be a FSA generated by the regular expression .
exists, because the Garside normal form is unique, then accepts all language of the form . It have the complete same structure as , but replacing every edge with .
Instead of construct directly, we only need to prove the fellow traveler property is true. This can be done by checking it is true for every independently.
Note that every generator has a constant distance from another generator.
Consider case by case:
- : The words differ in 1 are and .Assume is non-negative. At time , one encounters and , which has a distance of . At time , and , which also has distance 2. By induction, the distance is 2 till the end, where one has and . With one more step, it decrease the distance to . When is negative, it's similar.
- : Similar to case.
- : There are two cases. If the word end with , or end with , where , then the two words are exactly the same until the end. Thus implies the fellow traveler property. If the word end with a single , then the words are and . The second word in normal form is . Note the first word is We can use the fact that adding the have fellow traveler property to prove this also have that property.
- : Similar to case.
The fellow traveler property is true for each generator.
We now have the theorem