有限オートマトン

状態 $p\in Q$ に対し、$p$ から $\varepsilon$ 遷移だけを $0$ 回以上たどって到達できる状態全体を $E(p)\subset Q$ とおく（$\varepsilon$ 閉包。$p\in E(p)$ である）。
$$\Delta':=\{\,(p,a,q)\mid a\in\Sigma,\ \exists p'\in E(p),\ \exists q'\in Q,\ (p',a,q')\in\Delta,\ q\in E(q')\,\},\qquad F':=\{\,p\in Q\mid E(p)\cap F\ne\emptyset\,\}$$
と定める。$\Delta'$ の各元は $\Sigma$ の記号をラベルに持つので $\mathcal{A}'$ は NFA である。
$L(\mathcal{A})\subset L(\mathcal{A}')$：$w=a_1\cdots a_n$（$a_i\in\Sigma$）の $\mathcal{A}$ における受理経路をとる。この経路は、$\varepsilon$ 遷移の列、$a_1$ を読む遷移、$\varepsilon$ 遷移の列、$a_2$ を読む遷移、$\ldots$、$a_n$ を読む遷移、$\varepsilon$ 遷移の列、という形に区切れる。$a_i$ を読む遷移を $(p_i',a_i,q_i')$ とし、$q_0':=q_0$ とおく。$i$ 番目の $\varepsilon$ 遷移の列は $q_{i-1}'$ から $p_i'$ に至るので $p_i'\in E(q_{i-1}')$ であり、$q_i'\in E(q_i')$ だから $(q_{i-1}',a_i,q_i')\in\Delta'$ である。最後の $\varepsilon$ 遷移の列は $q_n'$ から $F$ の元に至るので $q_n'\in F'$ である。よって $q_0',q_1',\ldots,q_n'$ は $\mathcal{A}'$ における $w$ の受理経路である。$n=0$ のときは、$q_0$ から $\varepsilon$ 遷移だけで $F$ に至るので $q_0\in F'$ であり、$\varepsilon\in L(\mathcal{A}')$。
$L(\mathcal{A}')\subset L(\mathcal{A})$：$\mathcal{A}'$ における $w=a_1\cdots a_n$ の受理経路 $s_0=q_0,s_1,\ldots,s_n\in F'$ をとる。各 $(s_{i-1},a_i,s_i)\in\Delta'$ について、定義にある $p'\in E(s_{i-1})$、$q'$ をとれば、$\mathcal{A}$ において $s_{i-1}$ から $\varepsilon$ 遷移で $p'$ へ、$a_i$ で $q'$ へ、$\varepsilon$ 遷移で $s_i$ へ移る経路がある。これらをつなぎ、最後に $s_n\in F'$ から $\varepsilon$ 遷移で $F$ の元へ移る経路を加えれば、$\mathcal{A}$ における $w$ の受理経路が得られる。$n=0$ のときは $q_0\in F'$ が $E(q_0)\cap F\ne\emptyset$ を意味し、$\varepsilon\in L(\mathcal{A})$ である。

prop-finite-automaton-epsilon-removal により、$\mathcal{A}=(Q,\Sigma,\Delta,q_0,F)$ は NFA としてよい。状態集合を $Q$ の冪集合 $\mathcal{P}(Q)$ とし、
$$T(S,a):=\{\,q\in Q\mid \exists p\in S,\ (p,a,q)\in\Delta\,\}\quad(S\subset Q,\ a\in\Sigma),\qquad F_{\mathcal{D}}:=\{\,S\subset Q\mid S\cap F\ne\emptyset\,\}$$
とおいて $\mathcal{D}:=(\mathcal{P}(Q),\Sigma,T,\{q_0\},F_{\mathcal{D}})$ と定める。$T$ は各 $(S,a)$ に対して $\mathcal{P}(Q)$ の元をちょうど一つ定める写像なので $\mathcal{D}$ は DFA である。
$w=a_1\cdots a_n$ に対し、$\mathcal{D}$ の状態列を $S_0:=\{q_0\}$、$S_i:=T(S_{i-1},a_i)$ とおくと、$i$ に関する帰納法により
$$S_i=\{\,q\in Q\mid \mathcal{A}\text{ において }q_0\text{ から }a_1\cdots a_i\text{ を読んで }q\text{ に至る経路がある}\,\}$$
が成り立つ。実際 $i=0$ では両辺とも $\{q_0\}$ であり、$i-1$ から $i$ へは、$a_1\cdots a_i$ を読む経路とは $a_1\cdots a_{i-1}$ を読む経路の末尾に遷移 $(p,a_i,q)$ を継ぎ足したものにほかならず、それは $T$ の定義そのものである。したがって $\mathcal{D}$ が $w$ を受理する（$S_n\cap F\ne\emptyset$）ことと、$\mathcal{A}$ において $w$ を読んで受理状態に至る経路があることは同値であり、$L(\mathcal{D})=L(\mathcal{A})$ である。状態数は $|\mathcal{P}(Q)|=2^{k}$ であり、$\{q_0\}$ から到達できる状態だけを残せばさらに減らせる。

$w\in\Sigma^{*}$ に関する帰納法により $\delta((p_1,p_2),w)=(\delta_1(p_1,w),\delta_2(p_2,w))$ が成り立つ（$w=\varepsilon$ では両辺 $(p_1,p_2)$、$w=w'a$ では定義から従う）。よって $\delta((q_1,q_2),w)\in F_1\times F_2$ は $\delta_1(q_1,w)\in F_1$ かつ $\delta_2(q_2,w)\in F_2$、すなわち $w\in L(\mathcal{A}_1)\cap L(\mathcal{A}_2)$ と同値である。受理状態集合を $(F_1\times Q_2)\cup(Q_1\times F_2)$ にすれば「かつ」が「または」に変わり、和集合が得られる。補集合については、DFA では各 $w$ について到達状態 $\delta(q_0,w)$ がただ一つ定まるので、$w\in L(\bar{\mathcal{A}})\iff\delta(q_0,w)\in Q\setminus F\iff w\notin L(\mathcal{A})$ である。

prop-finite-automaton-epsilon-removal の構成は状態集合を変えないので、$\mathcal{A}$ は状態数 $k$ の NFA としてよい。$L(\mathcal{A})\ne\emptyset$ とし、受理される文字列のうち長さが最小のもの $w=a_1\cdots a_n$ をとり、その受理経路 $p_0,p_1,\ldots,p_n$ をとる。$n\ge k$ と仮定すると、$p_0,\ldots,p_n$ は $n+1>k$ 個の状態からなるので、鳩の巣原理により $p_i=p_j$ となる $i< j$ がある。このとき $p_0,\ldots,p_i,p_{j+1},\ldots,p_n$ は文字列 $a_1\cdots a_ia_{j+1}\cdots a_n$ の受理経路であり（$p_i=p_j$ から $a_{j+1}$ で $p_{j+1}$ に移れる）、この文字列は $w$ より短い。これは $w$ の最小性に反する。よって $n< k$ である。空性の判定は、長さ $k$ 未満の文字列（有限個）のそれぞれについて受理経路の有無を調べればよい。