From d3e761a2286d04a3c0005b199653df2f6501f070 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Fri, 19 Jun 2026 12:39:13 +0200
Subject: refined core

---
 .../core/soundness-proof/01-mathematical-definitions.tex     | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'chapters/core/soundness-proof/01-mathematical-definitions.tex')

diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex
index 19059ad..4bcb9df 100644
--- a/chapters/core/soundness-proof/01-mathematical-definitions.tex
+++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex
@@ -27,10 +27,18 @@ The agents are defined as:
 		where $x, \mathit{out}$ are wires.
 	\item $\llbracket \mathit{Materialize}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = x$\\
 		where $x, \mathit{out}$ are wires.
-	\item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a + b$\\
+	\item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \iff \mathit{out} = a + b$\\
 		where $a, b, \mathit{out}$ are wires.
-	\item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a \cdot b$\\
+	\item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \iff \mathit{out} = a \cdot b$\\
 		where $a, b, \mathit{out}$ are wires.
 	\item $\llbracket \mathit{TermReLU}(x) \sim \mathit{out} \rrbracket \iff \mathit{out} = \max(0, x)$\\
 		where $x, \mathit{out}$ are wires.
+	\item $\llbracket \mathit{TermSymbolic}(id) \sim \mathit{out} \rrbracket \iff \mathit{out} = x_{id}$\\
+		where $\mathit{out}$ is a wire and $id$ is a variable identifier.
+	\item $\llbracket \mathit{TermConcrete}(k) \sim \mathit{out} \rrbracket \iff \mathit{out} = k$\\
+		where $\mathit{out}$ is a wire and $k \in \mathbb{R}$ is an attribute.
+	\item $\llbracket \mathit{Dup}(x, y) \sim z \rrbracket \iff z = x = y$\\
+		where $x, y, z$ are wires.
+	\item $\llbracket \mathit{Eraser} \sim x \rrbracket \iff x \in \mathbb{R}$\\
+		where $x$ is a wire. \textit{Eraser} effectively removes any constraints.
 \end{itemize}
-- 
cgit v1.2.3

