From ef964d1d348c65597eb6f7221c1ca2be66a1cbca Mon Sep 17 00:00:00 2001
From: rensink <arend.rensink@utwente.nl>
Date: Wed, 28 Aug 2024 16:26:00 +0200
Subject: [PATCH] Exporation document

---
 doc/exploration/explore.tex | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/doc/exploration/explore.tex b/doc/exploration/explore.tex
index b91f2a238..57382450a 100644
--- a/doc/exploration/explore.tex
+++ b/doc/exploration/explore.tex
@@ -104,7 +104,13 @@
 \Tdepth_D & : s\mapsto\begin{cases}
 \Tdepth(p') & \text{if $s=\prm p$} \\
 \Tdepth(q) & \text{if $s=q\notin S_C$} \\
-\Tdepth_C(s) & \text{otherwise.}
-\end{cases}
+\Tdepth_C(s) & \text{otherwise}
+\end{cases} \\
+\Closed_D & = \Closed_C \cup\gensetof{\prm p}{p'\ngoesto} \\
+\Stable_D & = \Stable_C \cup \gensetof{\prm p}{\Tdepth(p')=0} \enspace.
 \end{align*}
+%
+For $\ttrans_C$, however, the case is less easy. For the purpose of this construction, we introduce several auxiliary data structures.
+
+
 \end{document}