Add details about full abstraction

concurgames.sty

@@ -14,6 +14,8 @@
 \newcommand{\con}{\operatorname{Con}}
 \newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
 
+\newcommand{\obseq}{\simeq_\text{obs}}
+
 \newcommand{\cov}{{{\mathrel-\joinrel\subset}}}
 \newcommand{\longcov}[1]{{\stackrel{#1}
 	{\mathrel-\joinrel\relbar\joinrel\subset\,}}}

math.sty

@@ -9,6 +9,13 @@
 \usepackage{mathtools}
 
 \newcommand{\eqdef}{{~\coloneqq~}}
+\newcommand{\lAnd}{~\&~}
+
+\newcommand{\overOr}[2]{\begin{array}{r l}
+	& #1 \\
+	\textit{or} & \\
+	& #2
+\end{array}}
 
 \newcommand{\id}{\operatorname{id}}
 

report.tex

@@ -1089,11 +1089,28 @@ not be too hard to lift it to a language closer to real-world programming
 languages, through the inclusion of the imperative primitives found in the
 literature.
 
-I also explored the possibility to reach a full-abstraction result, but
+\medskip
-abandoned this path by lack of time. Indeed, this would have required either to
+
-modify \llccs{} or to restrict the authorized strategies, because of the
+I also explored the possibility to reach a full-abstraction result. The
-following legal strategy, which cannot be expressed as the semantics of a term
+full-abstraction property states that two terms are \emph{observationally
-in \llccs{}:
+equivalent} if and only if their (denotational) semantics are equal, that is,
+in this context,
+for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
+
+\[
+	\left[ \forall \calC[-] \text{ a context }\,:\,
+		\left( \vdash \calC[P] : \proc \right),~
+		\calC[P] \Downarrow \iff \calC[Q] \Downarrow
+		\right]
+	\quad\iff\quad
+	\left( \seman{P} = \seman{Q} \right)
+\]
+
+Yet, by lack of time, I had to abandon this path. Indeed, this would have
+required either to modify \llccs{} or to restrict the authorized strategies,
+because of the following legal strategy, which cannot be expressed as the
+semantics of a term in \llccs{}:
+
 \[ \begin{tikzpicture}
 	\node (0P) at (2,2) {$\proc$};
 	\node (0C) at (0,2) {$\chan$};