نظریه مک‌ناتون
ساختن ماشین مولر

هر دو مفهموم "خدمت کردن" و "هم‌ارزی" در لم 2 مورد استفاده قرار گرفته‌است. اکنون از این لم برای ساختن یک ماشین مولر برای زبان αβω استفاده می‌کنیم. ماشین پیشنهادی یک کلمه را قبول می‌کند اگر و فقط اگر زمان i وجود داشته باشد که سمت راست لم 2 را ارضا گرداند. ماشین مذکور در ادامه توصیف شده‌است. توجه شود که این ماشین، یک ماشین قطعی مولر خواهد بود.

این ماشین شامل p+2 ماشین متناهی 
قطعی و یک کنترل‌کننده مستر (به انگلیسی: master controller) باشد که p سایز Aβ* می‌باشد. یکی از p+2 ماشین قادر است تا *αβ را تشخیص دهد و این ماشین در هر چرخه ورودی می‌گیرد. در هر زمان i یا کنترل‌کننده مستر ارتباط برقرار می‌کند، خواه *w(0,i) ∈ αβ برقرار باشد و یا خیر. باقی این p+1 ماشین کپی‌هایی از Aβ* هستند. مستر می‌تواند یک ماشین Aβ* را فعال یا غیر فعال گرداند. اگر مستر آن را غیرفعال گرداند، آنگاه  آن در حالت ابتدایی خود باقی مانده و نسبت به ورودی‌ها بی‌توجه خواهد شد. اگر مستر آن را فعال گرداند، سپس آن ماشین داده را خوانده و حرکت می‌کند تا زمانی که مستر آن را غیرفعال گردانیده و وادار به بازگشت به حالت ابتدایی کند. مستر قادر است تا یک ماشین Aβ* را به تعداد دفعاتی که مایل است فعال و غیرفعال گرداند. مستر در هر لحظه اطلاعات زیر را دربارهٔ ماشین‌های Aβ* ذخیره می‌کند.
حالت‌های جاری ماشین‌های Aβ*
لیستی از ماشین‌های Aβ* فعال به ترتیب زمان فعال‌سازیشان
برای هر ماشین Aβ* که فعال است، M، مجموعه ماشین‌های فعال دیگر که در زمان فعالسازی M، حالت پذیرش دارند. به عبارت دیگر، اگر یک ماشینی در زمان i فعال شده باشد و ماشین‌های دیگری در زمان j<i آخرین بار فعال شده باشند، و تا زمان i هم فعال بمانند، آنگاه مستر ثبت می‌کند که آیا i به j خدمت می‌کند یا خیر. این ثبتِ اطلاعات زمانی متوقف می‌شود که ماشین دیگری پیش از M غیر فعال گردد.
در ابتدا، مستر ممکن است با توجه به α به دو شکل متفاوت عمل کند. اگر α محتوی کلمات خالی باشد آنگاه تنها یکی از Aβ*  فعال خواهد بود، در غیر آن صورت، هیچ‌کدام از آن‌ها در شروع فعال نخواهند بود. بعدها در زمانی چون i، اگر *w(0,i) ∈ αβ و هیچکدام از ماشین‌های Aβ* در حالت اولیه نباشند، آنگاه مستر یکی از ماشین‌های غیرفعال را فعال کرده و ماشینی که به تازگی فعال شده شروع به دریافت ورودی از زمان i+1 می‌کند. در زمانی دیگر، اگر دو ماشین Aβ* به حالت یکسانی برسند، سپس مستر ماشینی را که دیرتر از دیگری فعال شده را غیرفعال می‌کند. توجه شود که مستر تصمیمات بالا را با توجه به اطلاعات ذخیره کرده اتخاذ می‌کند.

برای خروجی، مستر یک جفت چراغ سبز و قرمز را برای هر ماشین Aβ* داراست.اگر یک ماشین به حالت غیرفعال برود، چراغ قرمز روشن می‌شود. چراغ سبز ماشین M که در زمان j فعال شده‌است در دو حالت زیر در زمان i روشن خواهد بود:
M در حالت اولیه قرار دارد، در نتیجه (E(j,i,i و i به j خدمت می‌کند (حالت اولیه باید که حالت پذیرش باشد).
برای ماشین دیگری چون M' که فعال است و در زمان k فعال شده‌است، که در آن j<k<i، داریم که k به j خدمت می‌کند (مستر اطلاعات ثبت شده را دارد) و i زودترین زمانی است که در آن (E(j,k,i (ماشین 'M در زمان i غیر فعال خواهد شد).
توجه داشته باشید که چراغ سبز برای ماشین M، هر سری که یک ماشین به سبب M غیرفعال می‌شود، روشن نمی‌شود.

لم 3

اگر یک زمان هم‌ارز برای تعداد نامتناهی از زمان‌ها وجود داشته باشد که به آن خدمت کنند و i زودهنگام‌ترین آن‌ها باشد، آنگاه یک ماشین Aβ* مثل M در زمان i فعال می‌شود و برای همیشه فعال باقی می‌ماند (هیچ چراغ قرمزی روشن نمی‌شود پس ار آن) و چراغ سبز بینهایت بار میزند.

لم 4

برعکس، اگر ماشین Aβ* مانند M وجود داشته باشد که چراغ سبزش بینهایت بار روشن شده بوده باشد و چراغ قرمزش تنها دفعات متناهی زده باشد، آنگاه زمان‌های نامتناهی وجود خواهد داشت که هم‌ارز بوده و به آخرین زمانی که ماشین M فعال شده‌است، خدمت می‌کند.

لم 5

w ∈ αβω اگر و فقط اگر برای برخی ماشین‌های Aβ* چراغ سبز تعداد دفعات نامتناهی فلاش زده و چراغ قرمز تنها دفعات متناهی فلاش می‌زند.

توصیف بالا از یک ماشین کامل می‌تواند به عنوان یک ماشین قطعی گسترده در نظر گرفته شود. اکنون باید شرط پذیرش مولر تعریف گردد. در این ماشین گسترده، μn را مجموعه حالت‌های مرتبط با ماشین nام از نوع Aβ* تعریف می‌کنیم که در آن چراغ سبز فلاش زده و چراغ قرمز فلاش نمی‌زند. فرض کنید νn مجموعه حالت‌هایی باشد که در آن چراغ قرمز مربوط ماشین  nام فلاش نمی‌زند. در نتیجه، شرط پذیرش مولر خواهد بود: 
{F = { S | ∃n μn ⊆ S ⊆ νn 
این شرط، ساخت ماشین مولر مورد نظر را به اتمام می‌رساند.