Backus–Naur記法

まず $m=2$ の場合を $n$ に関する帰納法で示す。$\alpha\beta\Rightarrow^{n}\gamma$ とする。$n=0$ なら $\gamma=\alpha\beta$ であり、$\gamma_1=\alpha$、$\gamma_2=\beta$、$n_1=n_2=0$ とすればよい。$n\ge1$ とする。最初の一歩は、文字列 $\alpha\beta$ の中のある非終端記号 $A$ の一つの出現を規則 $A\to\rho$ で置き換える。$\alpha\beta$ の各記号は $\alpha$ 由来か $\beta$ 由来かのいずれか一方であるから、この出現は $\alpha$ の内部にあるか $\beta$ の内部にあるかのどちらかである。$\alpha$ の内部にある場合、$\alpha=\alpha'A\alpha''$ と書け、一歩の後の文字列は $(\alpha'\rho\alpha'')\beta$ で、$(\alpha'\rho\alpha'')\beta\Rightarrow^{n-1}\gamma$ である。帰納法の仮定により $\gamma=\gamma_1\gamma_2$、$\alpha'\rho\alpha''\Rightarrow^{m_1}\gamma_1$、$\beta\Rightarrow^{m_2}\gamma_2$、$m_1+m_2=n-1$ となる分解がある。このとき $\alpha\Rightarrow\alpha'\rho\alpha''\Rightarrow^{m_1}\gamma_1$ だから $n_1=m_1+1$、$n_2=m_2$ とすればよい。出現が $\beta$ の内部にある場合も対称に同じ議論が通る。
一般の $m$ は $m$ に関する帰納法による。$m=1$ は自明である。$m\ge2$ のとき、$\alpha_1\cdots\alpha_m=(\alpha_1\cdots\alpha_{m-1})\alpha_m$ に $m=2$ の場合を適用して $\gamma=\gamma'\gamma_m$、$\alpha_1\cdots\alpha_{m-1}\Rightarrow^{n'}\gamma'$、$\alpha_m\Rightarrow^{n_m}\gamma_m$、$n'+n_m=n$ を得、$\gamma'$ に帰納法の仮定を適用すればよい。
最後に $\alpha_j=x\in\Sigma$ のとき、生成規則の左辺は非終端記号であるから、終端記号だけからなる文字列 $x$ には導出の一歩を適用できない。よって $x\Rightarrow^{n_j}\gamma_j$ は $n_j=0$、$\gamma_j=x$ のときに限る。

はじめに、導出は前後に文脈を付けても実行できることに注意する。すなわち $\beta\Rightarrow^{*}\beta'$ ならば任意の $\gamma,\delta$ について $\gamma\beta\delta\Rightarrow^{*}\gamma\beta'\delta$ である。実際、$\beta$ から $\beta'$ への導出の各一歩は $\beta$ の中の非終端記号の一つの出現の置き換えであり、同じ出現を $\gamma\beta\delta$ の中で置き換えれば同じ歩数の導出が得られる。
(1) $F_P(L)\subset L$ を示す。$A\to\alpha\in P$、$\alpha=x_1\cdots x_m$、$w=w_1\cdots w_m\in\alpha[L]$ とする。$x_j\in N$ なら $w_j\in L(x_j)$ だから $x_j\Rightarrow^{*}w_j$ であり、$x_j\in\Sigma$ なら $w_j=x_j$ だから $x_j\Rightarrow^{0}w_j$ である。上の注意により
$$A\Rightarrow x_1x_2\cdots x_m\Rightarrow^{*}w_1x_2\cdots x_m\Rightarrow^{*}w_1w_2x_3\cdots x_m\Rightarrow^{*}\cdots\Rightarrow^{*}w_1w_2\cdots w_m=w$$
となり、$w\in L(A)$ である。
次に $L\subset F_P(L)$ を示す。$w\in L(A)$ とし、$A\Rightarrow^{n}w$ とする。$w\in\Sigma^{*}$ かつ $A\notin\Sigma$ だから $n\ge1$ であり、最初の一歩はある規則 $A\to\alpha\in P$ による $A\Rightarrow\alpha$ で、$\alpha\Rightarrow^{n-1}w$ である。$\alpha=\varepsilon$ のときは、$\varepsilon$ は非終端記号を含まないので書き換えられず、$w=\varepsilon\in\alpha[L]$ である。$\alpha=x_1\cdots x_m$（$m\ge1$）のときは、lem-bnf-derivation-splitting により $w=w_1\cdots w_m$、$x_j\Rightarrow^{n_j}w_j$ と分解でき、$x_j\in\Sigma$ なら $w_j=x_j$、$x_j\in N$ なら $w_j$ は $w$ の部分文字列ゆえ終端記号列なので $w_j\in L(x_j)$ である。よって $w\in\alpha[L]\subset F_P(L)_A$。
(2) $X$ を $P$ について閉じている族とする。「$A\in N$、$A\Rightarrow^{n}w$、$w\in\Sigma^{*}$ ならば $w\in X_A$」を $n$ に関する強帰納法（数学的帰納法）で示す。(1) の後半と同様に $n\ge1$ で、最初の一歩は $A\Rightarrow\alpha$（$A\to\alpha\in P$）、$\alpha\Rightarrow^{n-1}w$ である。$\alpha=\varepsilon$ なら $w=\varepsilon\in\alpha[X]\subset F_P(X)_A\subset X_A$。$\alpha=x_1\cdots x_m$（$m\ge1$）なら lem-bnf-derivation-splitting により $w=w_1\cdots w_m$、$x_j\Rightarrow^{n_j}w_j$、$n_1+\cdots+n_m=n-1$ と分解でき、$x_j\in\Sigma$ なら $w_j=x_j$、$x_j\in N$ なら $n_j\le n-1< n$ だから帰納法の仮定により $w_j\in X_{x_j}$ である。よって $w\in\alpha[X]\subset F_P(X)_A\subset X_A$。
最後の主張を確かめる。方程式系の任意の解 $X$ は $F_P(X)=X\subset X$ ゆえ閉じているので、(2) により $L\subset X$ であり、(1) により $L$ 自身が解だから、$L$ は最小解である。また、すべての成分を $\Sigma^{*}$ とした族は閉じているので閉じている族は存在し、閉じている族全体の共通部分を $I$（成分ごとに $I_B:=\bigcap_X X_B$）とおくと、単調性により各閉じた $X$ について $F_P(I)\subset F_P(X)\subset X$ だから $F_P(I)\subset I$、すなわち $I$ も閉じている。(2) により $L\subset I$、(1) により $L$ は閉じているので $I\subset L$。よって $L=I$ である。

$X_A:=\{w\in\Sigma^{*}\mid\mathcal{P}_A(w)\}$ とおく。仮定はちょうど、各 $A\to\alpha\in P$ について $\alpha[X]\subset X_A$、すなわち $F_P(X)\subset X$ を意味する。よって prop-bnf-least-solution (2) により $L(A)\subset X_A$ である。

$X_b:=\{0,1\}$、$X_{B'}:=\{0,1\}^{+}$、$X_B:=\{0\}\cup1\{0,1\}^{*}$ とおく。
（$L\subset X$）族 $X$ が閉じていることを規則ごとに確かめる。$b\to0$、$b\to1$：$0,1\in X_b$。$B'\to b$：$X_b\subset X_{B'}$。$B'\to bB'$：$X_bX_{B'}\subset\{0,1\}^{+}$。$B\to b$：$0\in X_B$、$1=1\varepsilon\in1\{0,1\}^{*}\subset X_B$。$B\to1B'$：$1X_{B'}=1\{0,1\}^{+}\subset1\{0,1\}^{*}$。よって cor-bnf-structural-induction により $L(b)\subset X_b$、$L(B')\subset X_{B'}$、$L(B)\subset X_B$。
（$X\subset L$）$b\Rightarrow0$、$b\Rightarrow1$ より $X_b\subset L(b)$。$u\in\{0,1\}^{+}$ について $u\in L(B')$ を $|u|$ に関する帰納法で示す。$|u|=1$ なら $B'\Rightarrow b\Rightarrow u$。$|u|\ge2$ なら $u=cu'$（$c\in\{0,1\}$、$u'\in\{0,1\}^{+}$）と書け、帰納法の仮定 $B'\Rightarrow^{*}u'$ と文脈を付けた導出により $B'\Rightarrow bB'\Rightarrow cB'\Rightarrow^{*}cu'=u$。最後に $B\Rightarrow b\Rightarrow0$、$B\Rightarrow b\Rightarrow1$、および $u\in\{0,1\}^{+}$ について $B\Rightarrow1B'\Rightarrow^{*}1u$ により $X_B\subset L(B)$。

$X_S:=\{a^{n}b^{n}\mid n\in\mathbb{N}\}$ とおく。
（$L(S)\subset X_S$）規則 $S\to\varepsilon$ について $\varepsilon=a^{0}b^{0}\in X_S$。規則 $S\to aSb$ について、$w=a^{n}b^{n}\in X_S$ なら $awb=a^{n+1}b^{n+1}\in X_S$。よって $X_S$ は閉じており、cor-bnf-structural-induction により $L(S)\subset X_S$。
（$X_S\subset L(S)$）$n$ に関する帰納法で $a^{n}b^{n}\in L(S)$ を示す。$n=0$ なら $S\Rightarrow\varepsilon$。$n\ge1$ なら帰納法の仮定 $S\Rightarrow^{*}a^{n-1}b^{n-1}$ と文脈を付けた導出により $S\Rightarrow aSb\Rightarrow^{*}a\,a^{n-1}b^{n-1}\,b=a^{n}b^{n}$。

文字列 $w$ に現れる $($ の個数を $\ell(w)$、$)$ の個数を $r(w)$ とし、性質 $\mathcal{P}_\varphi(w)$ を $\ell(w)=r(w)$ とする。規則ごとに確かめる。$\varphi\to p$、$\varphi\to\top$、$\varphi\to\bot$：右辺は括弧を含まない $1$ 記号なので $\ell=r=0$。$\varphi\to(\lnot\varphi)$：$\ell(u)=r(u)$ なら $\ell((\lnot u))=1+\ell(u)=1+r(u)=r((\lnot u))$。$\varphi\to(\varphi\land\varphi)$：$\ell(u)=r(u)$、$\ell(v)=r(v)$ なら
$$\ell((u\land v))=1+\ell(u)+\ell(v)=1+r(u)+r(v)=r((u\land v))$$
であり、$\lor$、$\to$ も同様。よって cor-bnf-structural-induction により $L(\varphi)$ のすべての元が $\mathcal{P}_\varphi$ を満たす（この文法は規則が無限個だが、ex-bnf-propositional-formula で述べたとおり系はそのまま適用できる）。