Lösung

Beweis: kodiere F_k(p, q)$\iff$p$\to^{{\leq 2^k}}_{}$q, es gibt einen Pfad der Länge $\leq$ 2^k von p nach q, durch QBF der Größe O(k).

F₀(p, q) : = (p = q) $\vee$ (p$\to^{1}_{}$q)

F_k+1(p, q) : = $\exists$m$\forall$x$\forall$y(((x = p $\wedge$ y = m) $\vee$ (x = m $\wedge$ y = q)) $\Rightarrow$ F_k(x, y))

Anwendung (Projekte!): (lange) Ableitungen (Schleifen) in längenerhaltenden Ersetzungssystemen, in Verschiebepuzzles (Lunar Lockout, Sokoban,...)