TQBF
$ \mathsf{TQBF} := \{\ulcorner \psi \urcorner\ |\ \text{$\psi \in \text{QBF}$ is true}\}
定理： $ \mathsf{TQBF} \in \textbf{PSPACE}
Proof.
$ \psi := (Q_n x_n)...(Q_0 x_0) \phi(x_0,...,x_n) \in \text{QBF}とする
再帰的に関数$ A : \text{QBF} \to 2を定義する。$ A((Q_{n} x_{n})...(Q_0 x_0) \phi(x_0,...,x_{n}))の計算に必要な計算空間を$ s(n)とする
$ n = 0のとき$ \psiは変数を含まないから$ A(\psi)の計算空間は$ O(\|\psi\|)
$ n = m+1のとき
$ A((\forall x_{m+1})(Q_m x_m)... \phi'(...,x_m, x_{m+1})) := A((Q_m x_m)...\phi'(...,x_m, 0)) \land A((Q_m x_m)...\phi'(...,x_m, 1))
$ A((\exists x_{m+1})(Q_m x_m)... \phi'(...,x_m, x_{m+1})) := A((Q_m x_m)...\phi'(...,x_m, 0)) \lor A((Q_m x_m)...\phi'(...,x_m, 1))
$ A((Q_m x_m)...\phi'(...,x_m, 0))と$ A((Q_m x_m)...\phi'(...,x_m, 1))の計算は同一の空間を共有できるので$ s(m)。また入力$ (Q_m x_m)...\phi'(...,x_m, 0)は変更箇所の$ \phi部分のみ与えればいいので$ O(\|\phi\|)。よって計算空間は$ s(m)+O(\|\phi\|)
定理：$ \mathsf{TQBF} \in \textbf{NPSPACE-complete}
Proof.
$ L \in \textbf{NPSPACE}を仮定して$ L \le_p \mathsf{TQBF}を示す
$ M_{\_,\_,S(\|x\|)}(x) = L(x)を仮定する
QBF$ \psi_iを次のように定義する
$ \psi_0(C, C') := \left[\Phi_x(C, C')\right]^*
$ \psi_{i+1}(C, C') := \left[ \exists C''.\forall D^1.\forall D^1 \left[ \left[\left(D^1 = C \land D^2 = C''\right) \lor \left(D^1 = C'' \land D^2 = C'\right)\right] \to\psi_i(D^1, D^2) \right]\right]^*
$ [\_]^* はprenex normal formへの変換。これは多項式時間で行える
定義より$ \psi_i(C, C') = 1 \iff C \longrightarrow_M^{\le 2^i} C'
また$ \|\psi_{i+1}\| = \|\psi_i\| + O(m)より$ \|\psi_{i}\|=i \cdot m
コードのごみを削除する機構を含ませることで一定の終着状態$ T_0または$ T_1へ到達する計算時間は高々$ S'(\|x\|) = O(S(\|x\|))
よって$ x \in L \iff M_{\_,\_,S(\|x\|)}(x) = 1 \iff \psi_{S'(\|x\|)}(C_x, T_1) \in \mathsf{TQBF} ❏ よって明らかに
系：$ \textbf{PSPACE} = \textbf{NPSPACE}