משפט אימרמן
הוכחה

בדומה למשפט סביץ', הוכחת המשפט הכללי מסתמכת על פתרון בעיה ספציפית - בעיית הישִיגוּת בגרפים (שנקראת באנגלית st-connectivity). בהינתן גרף מכוון  \ G בעל  \ n צמתים ושני צמתים  \ s,t, בעיית הישיגות היא השאלה האם קיים מסלול מ- \ s אל  \ t בגרף. מכיוון שניתן לייצג חישוב כלשהו של אלגוריתם אי דטרמיניסטי בתור מסלול בגרף אשר מייצג את הקונפיגורציות האפשריות השונות בחישוב, ניתן לצמצם את השאלה האם האלגוריתם עונה "כן" על קלט מסוים לשאלה אם קיים בגרף הקונפיגורציות שמתאר את ריצתו על קלט זה מסלול מהקונפיגורציה ההתחלתית לקונפיגורציה שבה האלגוריתם עונה "כן" (ניתן להניח ללא הגבלת הכלליות כי קיימת רק אחת כזו).
בעיית הישיגות בגרף ניתנות לפתרון אי דטרמיניסטי בזיכרון  \ O(\log(n)):
ההוכחה למשפט אימרמן מבוססת על כך שגם הבעיה המשלימה - הבדיקה האם בגרף לא קיים מסלול מ- \ s אל  \ t - ניתנת לביצוע באופן אי דטרמיניסטי בזיכרון  \ O(\log(n)). כלומר, קיימת מכונת טיורינג לא-דטרמיניסטית שמקבלת כקלט את צומת המקור  \ s וצומת היעד  \ t ועונה "כן" אם  \ t אינו יָשִׁיג מ- \ s (לפחות עבור בחירה אי-דטרמיניסטית יחידה שמבצע האלגוריתם). לעומת זאת אם קיים מסלול  \ s אל  \ t, האלגוריתם יענה "לא" בכל אחד מהחישובים שהוא מבצע בהתאם לבחירות האי-דטרמיניסטיות.
אימרמן הראה כי אם האלגוריתם יודע מראש מהו מספר הצמתים הישיגים מ- \ s לכל היותר ב- \ i צעדים (נסמן מספר זה ב \ N_{i}), אז האלגוריתם יכול פשוט "לנחש" את אותם צמתים ישיגים (ניחוש של  \ N_{i} צמתים שונים, למשל על ידי מעבר סדרתי על כל הצמתים ובחירה אי דטרמיניסטית אם רוצים לבחור אותו או לא), ופשוט לבדוק האם הם ישיגים מ \ s (באופן אי-דטרמיניסטי, בזיכרון  \ O(\log(n)), כפי שתואר מעלה). אם אכן האלגוריתם בחר את  \ N_{i} הצמתים ה"נכונים" (אלו שבאמת ישיגים מ- \ s), הוא בודק האם הצומת  \ t הוא אחד מהם. אם  \ t אחד מהצמתים הישיגים, האלגוריתם עונה "לא", ואחרת עונה "כן". אם אחת הבדיקות במהלך הדרך נכשלה האלגוריתם מחזיר תשובה "לא" כברירת מחדל (למשל, היה והוגרל צומת "לא נכון" עבור הקבוצה של  \ N_{i} הצמתים הישיגים).
לפי תיאור האלגוריתם, קל לראות שאם המספר  \ N_{i} ידוע לאלגוריתם, ו- \ t אינו יָשיג מ- \ s, אז קיימת בחירה שבה האלגוריתם יבחר בדיוק את  \ N_{i} הצמתים הישיגים מ- \ s, יבדוק שכל אחד מהם אכן ישיג, יזהה ש- \ t אינו אחד מהם, ויחזיר תשובה "כן"
ואילו כאשר  \ t ישיג מ- \ s (ב-i צעדים), אזי האלגוריתם יחזיר תשובה "לא" עבור כל אחת מהבחירות שהוא יכול לבצע: או שאלגוריתם יכשל באחת מבדיקות הביניים (ואז יחזיר "לא"), או שיצליח בכל הבחירות, יזהה את קבוצת  \ N_{i} הצמתים הישיגים מ- \ s (ב-i צעדים), יבדוק שכל אחד מהם אכן יָשיג, ואז יזהה ש- \ t ישיג מ- \ s, ויחזיר תשובה "לא". הבדיקה המתוארת לעיל היא חסכונית מבחינת צריכת הזיכרון שלה - מעבר סדרתי על כל צומתי הגרף דורש רק  \ O(\log(n)) זיכרון, וכך גם הבדיקות הנוספות שתיארנו.
מכאן עולה כי אם נתון המספר  \ N_{n} (הצמתים הישיגים ב- n צעדים, כאשר  n הוא גודל הגרף), אז ניתן לפתור את הבעיה בזיכרון  \ O(\log(n)) - פשוט מוודאים ש- \ t אינו ישיג מ- \ s ב- \ n צעדים (ולכן אינו ישיג כלל).
מכיוון שהסתמכנו על ידיעה מראש של  \ N_{n}, על מנת להשלים את האלגורים נותר להסביר כיצד ניתן לחשב את  \ N_{n}.
החישוב מתבצע בצורה אינדוקטיבית, כלומר האלגוריתם מצליח לחשב את  \ N_{i+1} כאשר נתון לו המספר  \ N_{i}. מכיוון שהאלגוריתם אינו דטרמיניסטי, קיימת עבורו האפשרות לענות "לא" אם החישוב לא הצליח, עקב ניחוש שגוי (כל עוד קיים לפחות ניחוש אחד שיהיה תקין ויוביל לתשובה "כן")
ראשית, ברור כי  \ N_{0}=1 - על ידי מסלול מאורך 0 אפשר להגיע מ- \ s רק אל  \ s עצמו.
החישוב האינדוקטיבי (מ- \ N_{i} ל- \ N_{i+1}) מתנהל באופן הבא: האלגוריתם עובר סדרתית על כל צומתי הגרף. לכל צומת  \ v הוא מחפש צומת  \ u כך שיש קשת מ- \ u אל  \ v ובנוסף לכך קיים מסלול באורך  \ i לכל היותר מ- \ s אל  \ u. חיפוש שכזה מתבצע באופן דומה למתואר לעיל - האלגוריתם בוחר באופן אי דטרמיניסטי את כל הצמתים שמרחקם מ- \ s הוא לכל היותר  \ i, בודק שאכן נבחרו הצמתים הנכונים, ואז בודק אם ניתן להגיע מהם אל  \ v. כמקודם, דרישות הסיבוכיות של שלב זה הן  \ O(\log(n)). לבסוף, האלגוריתם מחזיק מונה הסופר את מספרם של הצמתים  \ v שקיימו את התנאי; לאחר שהאלגוריתם מסיים לעבור על כל צומתי הגרף, מספר זה הוא בדיוק  \ N_{i+1}. מכאן שניתן לחשב את  \ N_{n} באופן אינדוקטיבי.