diff --git a/concurgames.sty b/concurgames.sty
index b3342d5..de40d8e 100644
--- a/concurgames.sty
+++ b/concurgames.sty
@@ -46,6 +46,9 @@
 \newcommand{\proc}{\mathbb{P}}
 \newcommand{\chan}{\mathbb{C}}
 
+\newcommand{\validctx}{\mathcal{L}}
+\newcommand{\freevars}{\operatorname{fv}}
+
 % Copycat
 \newcommand{\CC}{{\rm C\!\!\!C}}
 \newcommand{\cc}{\mathrm{\,c\!\!\!\!c\,}}
diff --git a/report.tex b/report.tex
index 2cf982e..483c6ee 100644
--- a/report.tex
+++ b/report.tex
@@ -692,18 +692,13 @@ We can now equip \llccs{} with denotational semantics, interpreting the
 language as strategies as defined in figure~\ref{fig:llccs:interp}.
 
 \begin{figure}[h]
-	\begin{minipage}[t]{0.45\textwidth} \begin{align*}
-		\seman{x^A} &\eqdef \cc_{\seman{A}} \\
+	\begin{align*}
+		\seman{x^A} &\eqdef \cc_{\seman{A}} &
+		\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B} \\
 		\seman{t^{A \linarrow B}~u^{A}} &\eqdef
 			\cc_{A \linarrow B} \strComp \left( \seman{t} \parallel \seman{u}
 			\right) \\
-		\seman{\lambda x^A \cdot t} &\eqdef \seman{t}
-	\end{align*} \end{minipage} \hfill
-	\begin{minipage}[t]{0.45\textwidth} \begin{align*}
-		\seman{\alpha} &\eqdef \ominus \\
-		\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B} \\
-	\end{align*}\end{minipage}
-	\begin{align*}
+		\seman{\lambda x^A \cdot t} &\eqdef \seman{t} \\
 		\seman{P \parallel Q} &\eqdef \left(
 			\begin{tikzpicture}[baseline, scale=0.8]
 				\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
@@ -797,10 +792,69 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 	\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
 \end{figure}
 
+A lot of these interpretations is what was expected: $\proc$ and $\chan$ have
+the same interpretation as presented before, $1$ is interpreted as the game
+playing \textit{done} while $0$ does not, the arrow is the type introduced for
+functions.
+
+A variable is represented by a \emph{copycat} of its type, to keep a version of
+the variable in the environment, reflecting the judgement $x:A \vdash x:A$.
+Same goes for the abstraction: the typing rule states that given a term
+verifying $\Gamma, x:A \vdash t:B$, we should obtain a term verifying $\Gamma
+\vdash \lambda x^A \cdot t : A \linarrow B$. The only thing we have to do is to
+``move'' $x$ from the environment to the term, which is transcribed by the
+associativity of $\parallel$. In the application, one can notice that the
+copycat wires up perfectly $\seman{t} \parallel \seman{u}$: the version of $x$
+from the environment of $t$ is connected to $u$, and the output of $t$ is
+connected to the output of the term.
+
+In the representation above, the drawn strategies are organized in columns: for
+instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
+\parallel P^\perp \parallel P$. Each column of events stands for one of those
+games, in this order.
+
 
 %%%%%%%%%%%%%%%%%%%%%
 \subsection{Adequacy}
 
+\todo{A bit more structure}
+
+\begin{theorem}[Adequacy]
+	The previous interpretation is \emph{adequate} with the operational
+	semantics, that is
+	\[ \forall P \textit{ st. } \vdash P : \proc,~
+	\left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \]
+\end{theorem}
+
+\begin{definition}[Evaluation in a context]
+	For $l$ a list of channels and $P$ a term, the evaluation of $P$ in the
+	context $l$, $\seman{P}_l$, is defined by induction by $\seman{P}_{[]}
+	\eqdef \seman{P}$ and $\seman{P}_{h::t} \eqdef \seman{(\nu h)P}_t$.
+\end{definition}
+
+\begin{definition}[valid contexts]
+	The \emph{valid contexts} for a reduction $P \redarrow{x} Q$, $\validctx_{P
+	\redarrow{x} Q}$, is the set of lists of channels such that, for each list
+	$l$,
+	\begin{enumerate}[(i)]
+		\item $\forall a:\chan \in \freevars(P)~\st~\bar{a} \in \freevars(P),~
+			a \in l \text{ or } \bar{a} \in l$;
+		\item if $x = a : \chan$, $a \not\in l$;
+		\item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$.
+	\end{enumerate}
+
+\end{definition}
+
+This result is mostly a consequence of the following lemma:
+
+\begin{lemma}
+	$\forall P \redarrow{x} Q, \forall l \in \validctx_{P \redarrow{x} Q}$,
+	\begin{itemize}
+		\item if $x = \tau$, then $\seman{P}_l = \seman{Q}_l$;
+		\item if $x = a: \chan$, then \qtodo{what?}
+	\end{itemize}
+\end{lemma}
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Implementation of deterministic concurrent games}