we know that $p\in P-\{o\}$. This, together with $x\in X_{n+1}\subseteq V_0$, implies that $(p,x)\in [(P-\{o\})\times V_0] \subseteq k_n$. Given $[(P-\{o\})\times V_0] \subseteq k_n$ and $V_0=Knowledge(k_n)$, the condition $k_\sigma\subseteq k_n$ is equivalent to $$\begin{array}{l} X_\sigma=\{v: (o,v)\in k_\sigma\} \subseteq \{v: (o,v)\in k_n\} =X_n \mbox{ and}\\ \{v:(o,v)\in k_\sigma\}\subseteq V_0.\end{array}$$ Since $x\in X_{n+1}\subseteq V_0$, $\{v:(o,v)\in k_\sigma\}\subseteq V_0$ gives us $(p,x,o,k_\sigma)\in R(k_0)$. Therefore, case ii) holds if and only if there exists a set $X_\sigma\subseteq X_n$ such that $X_\sigma\rightarrow x$. By Definition (\[gR-def\]), case i) or case ii) holds if and only if $x\in g_{R,k_0}(X_n)$. Hence, $X_{n+1}=g_{R,k_0}(X_n)$ and the lemma follows by induction on $n$.

$\Box$

Detecting Intruders {#kf-completeness}
-------------------

Let $m$ be the total number of values used in a single protocol session, including the subterms of each composite value. Suppose that Oscar can use only the primitives which [*compose*]{} or [*decompose*]{} inputs and for which the composition rules have no collisions (e.g encryptor/decryptor). Then, the theory in [@RT2001] implies the following: if there exists an attack in which Oscar uses $w$ parallel protocol sessions, then such an attack need not involve more than $w\cdot m$ values. From (\[v0\]) we infer that this corresponds to a valid state of knowledge $f_R^*(k_\sigma)$ derived from the 