refined core

4 files changed, 941 insertions, 512 deletions

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}
diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex
index 6764ea2..800e085 100644
--- a/chapters/core/soundness-proof/02-soundness-of-translation.tex
+++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex
@@ -3,7 +3,7 @@
 
 We need to prove that for each ONNX operator a semantically equivalent IN is produced.
 
-\paragraph{ReLU}
+\begin{lemma}
 The ONNX ReLU operator for an input tensor X and output tensor Y is defined as:
 $$
 Y = \max(0, X)
@@ -17,8 +17,9 @@ $$
 \llbracket \mathit{ReLU}(y_i) \sim x_i \rrbracket \Rightarrow y_i = \max(0, x_i)
 $$
 Which is identical to the ONNX definition.
+\end{lemma}
 
-\paragraph{Gemm}
+\begin{lemma}
 The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$
 and $\beta$ and output tensor Y is defined as:
 $$
@@ -40,15 +41,4 @@ $$
 \end{aligned}
 $$
 By substituting $v_i$, the result matches the ONNX definition.
-
-\paragraph{Identity}
-The ONNX Identity does not modify the numerical values of the tensors. As this operator results in a
-direct wire connection:
-$$
-y_i \sim x_i
-$$
-The semantic:
-$$
-\llbracket y_i \sim x_i \rrbracket \Rightarrow y_i = x_i
-$$
-trivially preserve the identity mapping.
+\end{lemma}
diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
index 2336135..be0870d 100644
--- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
+++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
@@ -1,507 +1,849 @@
 \subsection{Soundness of Interaction Rules}
 \label{sec:soundness-of-interaction-rules}
 
-\paragraph{Linear and Add}
-For the \textit{Linear} and \textit{Add} agents we have the interaction rule:
-$$
-\mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
-		& \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\
-		& \Rightarrow \mathit{out} = (q \cdot x + r) + b
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\
-		& \Rightarrow \mathit{out} = q \cdot x + (r + b)
-	\end{aligned}
-\end{aligned}
-$$
-Since $(q \cdot x + r) + b = q \cdot x + (r + b)$, the rule is sound.
-
-\paragraph{Linear and Mul}
-For the \textit{Linear} and \textit{Mul} agents we have the interaction rule:
-$$
-\mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
-		& \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\
-		& \Rightarrow \mathit{out} = (q \cdot x + r) \cdot b
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\
-		& \Rightarrow \mathit{out} = q \cdot b \cdot x + r \cdot b
-	\end{aligned}
-\end{aligned}
-$$
-Since $(q \cdot x + r) \cdot b = q \cdot b \cdot x + r \cdot b$, the rule is sound.
+\begin{lemma}
+	For the \textit{Linear} and \textit{Add} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
+			& \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\
+			& \Rightarrow \mathit{out} = (q \cdot x + r) + b
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\
+			& \Rightarrow \mathit{out} = q \cdot x + (r + b)
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $(q \cdot x + r) + b = q \cdot x + (r + b)$, the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and Add}
-For the \textit{Concrete} and \textit{Add} agents we have the interaction rule:
-$$
-\mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow
-\begin{cases}
-	\mathit{out} \sim b & \text{if } k = 0 \\
-	\mathit{AddCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise}
-\end{cases}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
-		& \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\
-		& \Rightarrow \mathit{out} = k + b
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 0 \\
-			\llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k + b & \text{otherwise}
-		\end{cases}
+\begin{lemma}
+	For the \textit{Linear} and \textit{Mul} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
+			& \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\
+			& \Rightarrow \mathit{out} = (q \cdot x + r) \cdot b
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\
+			& \Rightarrow \mathit{out} = q \cdot b \cdot x + r \cdot b
+		\end{aligned}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	0 + b = b & \text{if } k = 0 \\
-	k + b = k + b & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
+	$$
+	Since $(q \cdot x + r) \cdot b = q \cdot b \cdot x + r \cdot b$, the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and Mul}
-For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule:
-$$
-\mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow
-\begin{cases}
-	\mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} & \text{if } k = 0 \\
-	\mathit{out} \sim  b & \text{if } k = 1 \\
-	\mathit{MulCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise}
-\end{cases}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
-		& \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\
-		& \Rightarrow \mathit{out} = k \cdot b
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } k = 0 \\
-			\llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 1 \\
-			\llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k \cdot b & \text{otherwise}
-		\end{cases}
+\begin{lemma}
+	For the \textit{Concrete} and \textit{Add} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow
+	\begin{cases}
+		\mathit{out} \sim b & \text{if } k = 0 \\
+		\mathit{AddCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise}
+	\end{cases}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\
+			& \Rightarrow \mathit{out} = k + b
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 0 \\
+				\llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k + b & \text{otherwise}
+			\end{cases}
+		\end{aligned}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	0 \cdot b = 0 & \text{if } k = 0 \\
-	1 \cdot b = b & \text{if } k = 1 \\
-	k \cdot b = k \cdot b & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
+	$$
+	Since:
+	$$
+	\begin{cases}
+		0 + b = b & \text{if } k = 0 \\
+		k + b = k + b & \text{otherwise}
+	\end{cases}
+	$$
+	the rule is sound.
+\end{lemma}
 
-\paragraph{Linear and AddCheckLinear}
-For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule:
-$$
-\begin{aligned}
-	& \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\
-	& \quad \begin{cases}
-		\mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r,s,t = 0 \\
-		\mathit{out} \sim  \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} & \text{if } s,t = 0 \\
-		\mathit{out} \sim  \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} & \text{if } q,r = 0 \\
-		\begin{aligned}
-			& \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\
-			& \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\
-			& \mathit{out} \sim \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0)
+\begin{lemma}
+	For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow
+	\begin{cases}
+		\mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} & \text{if } k = 0 \\
+		\mathit{out} \sim  b & \text{if } k = 1 \\
+		\mathit{MulCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise}
+	\end{cases}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\
+			& \Rightarrow \mathit{out} = k \cdot b
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } k = 0 \\
+				\llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 1 \\
+				\llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k \cdot b & \text{otherwise}
+			\end{cases}
 		\end{aligned}
-		& \text{otherwise}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		0 \cdot b = 0 & \text{if } k = 0 \\
+		1 \cdot b = b & \text{if } k = 1 \\
+		k \cdot b = k \cdot b & \text{otherwise}
 	\end{cases}
-\end{aligned}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
-		& \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\
-		& \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\
-			\llbracket \mathit{out} \sim  \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\
-			\llbracket \mathit{out} \sim  \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = s \cdot y + t & \text{if } q,r = 0 \\
+	$$
+	the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		& \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\
+		& \quad \begin{cases}
+			\mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r,s,t = 0 \\
+			\mathit{out} \sim  \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} & \text{if } s,t = 0 \\
+			\mathit{out} \sim  \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} & \text{if } q,r = 0 \\
 			\begin{aligned}
-				& \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\
-				& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\
-				& \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\
-				& \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\
-				& \llbracket \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot (\mathit{out}_x + \mathit{out}_y) + 0
-			\end{aligned}\\
-			\Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise}
+				& \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\
+				& \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\
+				& \mathit{out} \sim \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0)
+			\end{aligned}
+			& \text{otherwise}
 		\end{cases}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	0 \cdot x + (0 + 0 \cdot y + 0) = 0 & \text{if } q,r,s,t = 0 \\
-	q \cdot x + (r + 0 \cdot y + 0) = q \cdot x + r & \text{if } s,t = 0 \\
-	0 \cdot x + (0 + s \cdot y + t) = s \cdot y + t & \text{if } q,r = 0 \\
-	q \cdot x + (r + s \cdot y + t) = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
-
-\paragraph{Linear and MulCheckLinear}
-For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule:
-$$
-\begin{aligned}
-	& \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\
-	& \quad \begin{cases}
-		\mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r = 0 \lor s,t = 0 \\
-		\begin{aligned}
-			& \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\
-			& \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\
-			& \mathit{out} \sim \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0)
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
+			& \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\
+			& \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\
+				\llbracket \mathit{out} \sim  \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\
+				\llbracket \mathit{out} \sim  \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = s \cdot y + t & \text{if } q,r = 0 \\
+				\begin{aligned}
+					& \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\
+					& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\
+					& \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\
+					& \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\
+					& \llbracket \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot (\mathit{out}_x + \mathit{out}_y) + 0
+				\end{aligned}\\
+				\Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise}
+			\end{cases}
 		\end{aligned}
-		& \text{otherwise}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		0 \cdot x + (0 + 0 \cdot y + 0) = 0 & \text{if } q,r,s,t = 0 \\
+		q \cdot x + (r + 0 \cdot y + 0) = q \cdot x + r & \text{if } s,t = 0 \\
+		0 \cdot x + (0 + s \cdot y + t) = s \cdot y + t & \text{if } q,r = 0 \\
+		q \cdot x + (r + s \cdot y + t) = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise}
 	\end{cases}
-\end{aligned}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
-		& \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\
-		& \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\
+	$$
+	the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		& \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\
+		& \quad \begin{cases}
+			\mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r = 0 \lor s,t = 0 \\
 			\begin{aligned}
-				& \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\
-				& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\
-				& \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\
-				& \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\
-				& \llbracket \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \mathit{out}_x \cdot \mathit{out}_y + 0
-			\end{aligned}\\
-			\Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise}
+				& \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\
+				& \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\
+				& \mathit{out} \sim \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0)
+			\end{aligned}
+			& \text{otherwise}
 		\end{cases}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0  \\
-	1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
-
-\paragraph{Concrete and AddCheckLinear}
-For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule:
-$$
-\mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
-		& \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\
-		& \Rightarrow \mathit{out} = q \cdot x + (r + j)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Linear}(x, q, r + j) \sim \mathit{out} \rrbracket \\
-		& \Rightarrow \mathit{out} = q \cdot x + (r + j)
-	\end{aligned}
-\end{aligned}
-$$
-Since $q \cdot x + (r + j) = q \cdot x + (r + j)$, the rule is sound.
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
+			& \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\
+			& \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\
+				\begin{aligned}
+					& \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\
+					& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\
+					& \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\
+					& \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\
+					& \llbracket \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \mathit{out}_x \cdot \mathit{out}_y + 0
+				\end{aligned}\\
+				\Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise}
+			\end{cases}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0  \\
+		1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise}
+	\end{cases}
+	$$
+	the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and MulCheckLinear}
-For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule:
-$$
-\mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
-		& \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\
-		& \Rightarrow \mathit{out} = q \cdot j \cdot x + r \cdot j
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \rrbracket \\
-		& \Rightarrow \mathit{out} = (q \cdot j) \cdot x + (r \cdot j)
-	\end{aligned}
-\end{aligned}
-$$
-Since $q \cdot j \cdot x + r \cdot j = (q \cdot j) \cdot x + (r \cdot j)$, the rule is sound.
+\begin{lemma}
+	For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
+			& \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\
+			& \Rightarrow \mathit{out} = q \cdot x + (r + j)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(x, q, r + j) \sim \mathit{out} \rrbracket \\
+			& \Rightarrow \mathit{out} = q \cdot x + (r + j)
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $q \cdot x + (r + j) = q \cdot x + (r + j)$, the rule is sound.
+\end{lemma}
 
-\paragraph{Linear and AddCheckConcrete}
-For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule:
-$$
-\mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
-		& \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\
-		& \Rightarrow \mathit{out} = k + (s \cdot y + t)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Linear}(y, s, t + k) \sim \mathit{out} \rrbracket \\
-		& \Rightarrow \mathit{out} = s \cdot y + (t + k)
-	\end{aligned}
-\end{aligned}
-$$
-Since $k + (s \cdot y + t) = s \cdot y + (t + k)$, the rule is sound.
+\begin{lemma}
+	For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
+			& \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\
+			& \Rightarrow \mathit{out} = q \cdot j \cdot x + r \cdot j
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \rrbracket \\
+			& \Rightarrow \mathit{out} = (q \cdot j) \cdot x + (r \cdot j)
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $q \cdot j \cdot x + r \cdot j = (q \cdot j) \cdot x + (r \cdot j)$, the rule is sound.
+\end{lemma}
 
-\paragraph{Linear and MulCheckConcrete}
-For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule:
-$$
-\mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
-		& \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\
-		& \Rightarrow \mathit{out} = k \cdot (s \cdot y + t)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \rrbracket \\
-		& \Rightarrow \mathit{out} = (s \cdot k) \cdot y + (t \cdot k)
-	\end{aligned}
-\end{aligned}
-$$
-Since $k \cdot (s \cdot y + t) = (s \cdot k) \cdot y + (t \cdot k)$, the rule is sound.
+\begin{lemma}
+	For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
+			& \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\
+			& \Rightarrow \mathit{out} = k + (s \cdot y + t)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(y, s, t + k) \sim \mathit{out} \rrbracket \\
+			& \Rightarrow \mathit{out} = s \cdot y + (t + k)
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k + (s \cdot y + t) = s \cdot y + (t + k)$, the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and AddCheckConcrete}
-For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule:
-$$
-\mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow
-\begin{cases}
-	\mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\
-	\mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise}
-\end{cases}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
-		& \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\
-		& \Rightarrow \mathit{out} = k + j
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 0 \\
-			\llbracket \mathit{out} \sim \mathit{Concrete}(k + j) \rrbracket \Rightarrow \mathit{out} = k + j & \text{otherwise}
-		\end{cases}
+\begin{lemma}
+	For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\
+			& \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\
+			& \Rightarrow \mathit{out} = k \cdot (s \cdot y + t)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \rrbracket \\
+			& \Rightarrow \mathit{out} = (s \cdot k) \cdot y + (t \cdot k)
+		\end{aligned}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	k + 0 = k & \text{if } j = 0 \\
-	k + j = k + j & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
+	$$
+	Since $k \cdot (s \cdot y + t) = (s \cdot k) \cdot y + (t \cdot k)$, the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and MulCheckConcrete}
-For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule:
-$$
-\mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow
-\begin{cases}
-	\mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\
-	\mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\
-	\mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise}
-\end{cases}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
-		& \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\
-		& \Rightarrow \mathit{out} = k \cdot j
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } j = 0 \\
-			\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 1 \\
-			\llbracket \mathit{out} \sim \mathit{Concrete}(k \cdot j) \rrbracket \Rightarrow \mathit{out} = k \cdot j & \text{otherwise}
-		\end{cases}
+\begin{lemma}
+	For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow
+	\begin{cases}
+		\mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\
+		\mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise}
+	\end{cases}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
+			& \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\
+			& \Rightarrow \mathit{out} = k + j
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 0 \\
+				\llbracket \mathit{out} \sim \mathit{Concrete}(k + j) \rrbracket \Rightarrow \mathit{out} = k + j & \text{otherwise}
+			\end{cases}
+		\end{aligned}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	k \cdot 0 = 0 & \text{if } j = 0 \\
-	k \cdot 1 = k & \text{if } j = 1 \\
-	k \cdot j = k \cdot j & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
+	$$
+	Since:
+	$$
+	\begin{cases}
+		k + 0 = k & \text{if } j = 0 \\
+		k + j = k + j & \text{otherwise}
+	\end{cases}
+	$$
+	the rule is sound.
+\end{lemma}
 
-\paragraph{Linear and ReLU}
-For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule:
-$$
-\begin{aligned}
-	& \mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow
-	\mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x);
-	\mathit{out} \sim \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0)
-\end{aligned}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(q, x, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
-		& \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\
-		& \Rightarrow \mathit{out} = \max(0, q \cdot x + r)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow w = q \cdot x + r \\
-		& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w \rrbracket \Rightarrow \mathit{out}_x = w \\
-		& \llbracket \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \max(0, \mathit{out}_x) + 0 \\
-		& \Rightarrow \mathit{out} = 1 \cdot \max(0, q \cdot x + r) + 0
-	\end{aligned}
-\end{aligned}
-$$
-Since $\max(0, q \cdot x + r) = 1 \cdot \max(0, q \cdot x + r) + 0$ the rule is sound.
+\begin{lemma}
+	For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow
+	\begin{cases}
+		\mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\
+		\mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\
+		\mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise}
+	\end{cases}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\
+			& \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\
+			& \Rightarrow \mathit{out} = k \cdot j
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } j = 0 \\
+				\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 1 \\
+				\llbracket \mathit{out} \sim \mathit{Concrete}(k \cdot j) \rrbracket \Rightarrow \mathit{out} = k \cdot j & \text{otherwise}
+			\end{cases}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		k \cdot 0 = 0 & \text{if } j = 0 \\
+		k \cdot 1 = k & \text{if } j = 1 \\
+		k \cdot j = k \cdot j & \text{otherwise}
+	\end{cases}
+	$$
+	the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and ReLU}
-For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule:
-$$
-\mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow
-\begin{cases}
-	\mathit{out} \sim \mathit{Concrete}(k) & \text{if } k > 0 \\
-	\mathit{out} \sim \mathit{Concrete}(0) & \text{otherwise}
-\end{cases}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
-		& \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\
-		& \Rightarrow \mathit{out} = \max(0, k)
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } k > 0 \\
-			\llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{otherwise}
-		\end{cases}
+\begin{lemma}
+	For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		\mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow
+		& \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\
+		& \mathit{out} \sim \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0)
+	\end{aligned}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
+			& \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\
+			& \Rightarrow \mathit{out} = \max(0, q \cdot x + r)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow w = q \cdot x + r \\
+			& \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w \rrbracket \Rightarrow \mathit{out}_x = w \\
+			& \llbracket \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \max(0, \mathit{out}_x) + 0 \\
+			& \Rightarrow \mathit{out} = 1 \cdot \max(0, q \cdot x + r) + 0
+		\end{aligned}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	\max(0, k) = k & \text{if } k > 0 \\
-	\max(0, k) = 0 & \text{otherwise}
-\end{cases}
-$$
-the rule is sound.
+	$$
+	Since $\max(0, q \cdot x + r) = 1 \cdot \max(0, q \cdot x + r) + 0$ the rule is sound.
+\end{lemma}
 
-\paragraph{Linear and Materialize}
-For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule:
-$$
-\begin{aligned}
-	& \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\
-	& \quad \begin{cases}
-		\mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\
-		\mathit{out} \sim x & \text{if } q = 1, r = 0 \\
-		\mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) & \text{if } q = 1 \\
-		\mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) & \text{if } r = 0 \\
-		\mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) & \text{otherwise}
+\begin{lemma}
+	For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow
+	\begin{cases}
+		\mathit{out} \sim \mathit{Concrete}(k) & \text{if } k > 0 \\
+		\mathit{out} \sim \mathit{Concrete}(0) & \text{otherwise}
+	\end{cases}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\
+			& \Rightarrow \mathit{out} = \max(0, k)
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } k > 0 \\
+				\llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{otherwise}
+			\end{cases}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		\max(0, k) = k & \text{if } k > 0 \\
+		\max(0, k) = 0 & \text{otherwise}
 	\end{cases}
-\end{aligned}
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
-		& \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\
-		& \Rightarrow \mathit{out} = q \cdot x + r
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: }
-		\begin{cases}
-			\llbracket \mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\
-			\llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\
-			\llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\
-			\llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\
-			\llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\
+	$$
+	the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		& \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\
+		& \quad \begin{cases}
+			\mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\
+			\mathit{out} \sim x & \text{if } q = 1, r = 0 \\
+			\mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) & \text{if } q = 1 \\
+			\mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) & \text{if } r = 0 \\
+			\mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) & \text{otherwise}
 		\end{cases}
 	\end{aligned}
-\end{aligned}
-$$
-Since:
-$$
-\begin{cases}
-	0 \cdot x + r = r & \text{if } q = 0 \\
-	1 \cdot x + 0 = x & \text{if } q = 1, r = 0 \\
-	1 \cdot x + r = x + r & \text{if } q = 1 \\
-	q \cdot x + 0 = q	\cdot x & \text{if } r = 0 \\
-	q \cdot x + r = q \cdot x + r & \text{otherwise} \\
-\end{cases}
-$$
-the rule is sound.
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\
+			& \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\
+			& \Rightarrow \mathit{out} = q \cdot x + r
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+			\begin{cases}
+				\llbracket \mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\
+				\llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\
+				\llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\
+				\llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\
+				\llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\
+			\end{cases}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since:
+	$$
+	\begin{cases}
+		0 \cdot x + r = r & \text{if } q = 0 \\
+		1 \cdot x + 0 = x & \text{if } q = 1, r = 0 \\
+		1 \cdot x + r = x + r & \text{if } q = 1 \\
+		q \cdot x + 0 = q	\cdot x & \text{if } r = 0 \\
+		q \cdot x + r = q \cdot x + r & \text{otherwise} \\
+	\end{cases}
+	$$
+	the rule is sound.
+\end{lemma}
 
-\paragraph{Concrete and Materialize}
-For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule:
-$$
-\mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{Concrete}(k) \sim \mathit{out} \\
-$$
-We need to show that the LHS and RHS are semantically equivalent:
-$$
-\begin{aligned}
-	& \begin{aligned}
-		\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
-		& \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} =  w \\
-		& \Rightarrow \mathit{out} = k
-	\end{aligned} \\
-	& \begin{aligned}
-		\text{RHS: } & \llbracket \mathit{Concrete}(k) \sim \mathit{out} \rrbracket \\
-		& \Rightarrow \mathit{out} = k 
-	\end{aligned}
-\end{aligned}
-$$
-Since $k = k$, the rule is sound.
+\begin{lemma}
+	For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{TermConcrete}(k) \sim \mathit{out} \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} =  w \\
+			& \Rightarrow \mathit{out} = k
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermConcrete}(k) \sim \mathit{out} \rrbracket \\
+			& \Rightarrow \mathit{out} = k 
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k = k$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Linear} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(z, q, r) \sim w \rrbracket \Rightarrow z\cdot q + r = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow z \cdot q + r = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Linear}(z_1, q, r) \sim x \rrbracket \Rightarrow z_1 \cdot q + r = x \\
+			& \llbracket \mathit{Linear}(z_2, q, r) \sim y \rrbracket \Rightarrow z_2 \cdot q + r = y \\
+			& \llbracket \mathit{Dup}(z_1, z_2) \sim z \rrbracket \Rightarrow z = z_1 = z_2 \\
+			& \Rightarrow z \cdot q + r = x \land z \cdot q + r = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $z \cdot q + r = x = y \iff z \cdot q + r = x \land z \cdot q + r = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Linear} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{Linear}(x, q, r) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow x\cdot q + r = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow x \cdot q + r \in \mathbb{R}
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Eraser} \sim x \rrbracket \\
+			& \Rightarrow x \in \mathbb{R}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $x \cdot q + r \in \mathbb{R} \iff x \in \mathbb{R}$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Concrete} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Concrete}(k) \sim x; \mathit{Concrete}(k) \sim y \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow k = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Concrete}(k) \sim x \rrbracket \Rightarrow k = x \\
+			& \llbracket \mathit{Concrete}(k) \sim y \rrbracket \Rightarrow k = y \\
+			& \Rightarrow k = x \land k = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k = x = y \iff k = x \land k = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{Concrete} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{Concrete}(k) \bowtie \mathit{Eraser} \Rightarrow  \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow k \in \mathbb{R} 
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		\mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermAdd}(a_1, b_1) \sim x; \mathit{TermAdd}(a_2, b_2) \sim y; \\
+		& \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\
+	\end{aligned}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermAdd}(a, b) \sim w \rrbracket \Rightarrow a + b = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow a + b = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermAdd}(a_1, b_1) \sim x \rrbracket \Rightarrow a_1 + b_1 = x \\
+			& \llbracket \mathit{TermAdd}(a_2, b_2) \sim y \rrbracket \Rightarrow a_2 + b_2 = y \\
+			& \llbracket \mathit{Dup}(a_1, a_2) \sim a \rrbracket \Rightarrow a = a_1 = a_2 \\
+			& \llbracket \mathit{Dup}(b_1, b_2) \sim b \rrbracket \Rightarrow b = b_1 = b_2 \\
+			& \Rightarrow a + b = x \land a + b = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $a + b = x = y \iff a + b = x \land a + b = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermAdd} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{TermAdd}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermAdd}(a, b) \sim w \rrbracket \Rightarrow a + b = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow a + b \in \mathbb{R}
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Eraser} \sim a \rrbracket \Rightarrow a \in \mathbb{R} \\
+			& \llbracket \mathit{Eraser} \sim b \rrbracket \Rightarrow b \in \mathbb{R} \\
+			& \Rightarrow a \in \mathbb{R} \land b \in \mathbb{R}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $a + b \in \mathbb{R} \iff a \in \mathbb{R} \land b \in \mathbb{R}$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\begin{aligned}
+		\mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\
+		& \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\
+	\end{aligned}
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermMul}(a, b) \sim w \rrbracket \Rightarrow a \cdot b = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow a \cdot b = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermMul}(a_1, b_1) \sim x \rrbracket \Rightarrow a_1 \cdot b_1 = x \\
+			& \llbracket \mathit{TermMul}(a_2, b_2) \sim y \rrbracket \Rightarrow a_2 \cdot b_2 = y \\
+			& \llbracket \mathit{Dup}(a_1, a_2) \sim a \rrbracket \Rightarrow a = a_1 = a_2 \\
+			& \llbracket \mathit{Dup}(b_1, b_2) \sim b \rrbracket \Rightarrow b = b_1 = b_2 \\
+			& \Rightarrow a \cdot b = x \land a \cdot b = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $a \cdot b = x = y \iff a \cdot b = x \land a \cdot b = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermMul} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{TermMul}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermMul}(a, b) \sim w \rrbracket \Rightarrow a \cdot b = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow a \cdot b \in \mathbb{R}
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Eraser} \sim a \rrbracket \Rightarrow a \in \mathbb{R} \\
+			& \llbracket \mathit{Eraser} \sim b \rrbracket \Rightarrow b \in \mathbb{R} \\
+			& \Rightarrow a \in \mathbb{R} \land b \in \mathbb{R}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $a \cdot b \in \mathbb{R} \iff a \in \mathbb{R} \land b \in \mathbb{R}$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermReLU}(z_1) \sim x; \mathit{TermReLU}(z_2) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermReLU}(z) \sim w \rrbracket \Rightarrow \max(0, z) = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow \max(0, z) = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermReLU}(z_1) \sim x \rrbracket \Rightarrow \max(0, z_1) = x \\
+			& \llbracket \mathit{TermReLU}(z_2) \sim y \rrbracket \Rightarrow \max(0, z_2) = y \\
+			& \llbracket \mathit{Dup}(z_1, z_2) \sim z \rrbracket \Rightarrow z = z_1 = z_2 \\
+			& \Rightarrow \max(0, z) = x \land \max(0, z) = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $\max(0, z) = x = y \iff \max(0, z) = x \land \max(0, z) = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermReLU} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{TermReLU}(x) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermReLU}(x) \sim w \rrbracket \Rightarrow \max(0, x) = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow \max(0, x) \in \mathbb{R}
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{Eraser} \sim x \rrbracket \\
+			& \Rightarrow x \in \mathbb{R}
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $\max(0, x) \in \mathbb{R} \iff x \in \mathbb{R}$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermConcrete}(k) \sim x; \mathit{TermConcrete}(k) \sim y \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermConcrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow k = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermConcrete}(k) \sim x \rrbracket \Rightarrow k = x \\
+			& \llbracket \mathit{TermConcrete}(k) \sim y \rrbracket \Rightarrow k = y \\
+			& \Rightarrow k = x \land k = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k = x = y \iff k = x \land k = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermConcrete} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{TermConcrete}(k) \bowtie \mathit{Eraser} \Rightarrow  \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermConcrete}(k) \sim w \rrbracket \Rightarrow k = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow k \in \mathbb{R} 
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule:
+	$$
+	\mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermSymbolic}(id) \sim x; \mathit{TermSymbolic}(id) \sim y \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermSymbolic}(id) \sim w \rrbracket \Rightarrow x_{id} = w \\
+			& \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\
+			& \Rightarrow x_{id} = x = y
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: } & \llbracket \mathit{TermSymbolic}(id) \sim x \rrbracket \Rightarrow x_{id} = x \\
+			& \llbracket \mathit{TermSymbolic}(id) \sim y \rrbracket \Rightarrow x_{id} = y \\
+			& \Rightarrow x_{id} = x \land x_{id} = y
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $x_{id} = x = y \iff x_{id} = x \land x_{id} = y$, the rule is sound.
+\end{lemma}
+
+\begin{lemma}
+	For the \textit{TermSymbolic} and \textit{Eraser} agents we have the interaction rule:
+	$$
+	\mathit{TermSymbolic}(id) \bowtie \mathit{Eraser} \Rightarrow  \\
+	$$
+	We need to show that the LHS and RHS are semantically equivalent:
+	$$
+	\begin{aligned}
+		& \begin{aligned}
+			\text{LHS: } & \llbracket \mathit{TermSymbolic}(id) \sim w \rrbracket \Rightarrow x_{id} = w \\
+			& \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\
+			& \Rightarrow x_{id} \in \mathbb{R} 
+		\end{aligned} \\
+		& \begin{aligned}
+			\text{RHS: }
+		\end{aligned}
+	\end{aligned}
+	$$
+	Since $x_{id} \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+\end{lemma}
diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
index b0a7906..d0cec53 100644
--- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex
+++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
@@ -1,28 +1,117 @@
 \subsection{Soundness of Reduction}
 \label{sec:soundness-of-reduction}
 
-Let $\text{IN}_0$ be the IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be
-the IN after $n$ reduction steps. Then we need to prove:
-$$
-\forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket
-$$
+\begin{lemma}
+	A valid IN satisfies the following properties:
+	\begin{itemize}
+		\item \textbf{DAG}: the net forms a DAG where the roots are the free wires representing the network
+			outputs.
+		\item \textbf{Orientation}: carrier agents always have their principal ports oriented toward the outputs,
+			while operator and intermediate agents always have their principal ports oriented toward the
+			inputs. No interaction rule introduces carriers facing the input nor operators or
+			intermediates facing the output.
+		\item \textbf{Restricted Interaction}: the net is constructed such that active pairs only occur between a
+			carrier agent and an operator/intermediate agent. Because of \textbf{Orientation}, neither
+			carrier nor operator agents interact with agents of the same type. Terminal agents do not
+			interact with computational operators because they are wrapped in a \textit{Linear} agent.
+	\end{itemize}
+\end{lemma}
 
-\paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial
-$\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly
-match the mathematical definition of the ONNX operators in $\text{NN}$.
+\begin{theorem}
+	Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be
+	the IN after $n$ reduction steps, then:
+	\begin{equation}
+	\forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket
+	\end{equation}
+\end{theorem}
 
-\paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$.
-If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair
-$A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}},
-the mathematical definition is preserved after any reduction step, it follows that:
-$$
-\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket
-$$
-By the inductive hypothesis:
-$$
-\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket
-$$
+\begin{proof}
+	We will proceed by induction on the number $n$ of reduction steps:
+	\paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial
+	$\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly
+	match the mathematical definition of the ONNX operators in $\text{NN}$, it follows that:
+	\begin{equation}
+	\llbracket \text{IN}_{0} \rrbracket = \llbracket \text{NN} \rrbracket
+	\end{equation}
 
-By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the
-original $\text{NN}$ at every step of the reduction process. Additionally, since IN are confluent,
-the reduced mathematical expression is unique regardless of order in which rules are applied.
+	\paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$.
+	If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair
+	$A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}},
+	the mathematical definition is preserved after any reduction step, it follows that:
+	\begin{equation}
+	\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket
+	\end{equation}
+	By the inductive hypothesis:
+	\begin{equation}
+	\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket
+	\end{equation}
+	By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the
+	original $\text{NN}$ at every step of the reduction process.
+\end{proof}
+
+\begin{theorem}
+	For any valid $\text{IN}_0$ translated from a neural network $\text{NN}$, the reduction process
+	$\text{IN}_0 \to \text{IN}_1 \to \dots \to \text{IN}_n$ reaches a unique normal form, an IN with no active pair, in a
+	finite number of steps $n$.
+\end{theorem}
+
+\begin{proof}
+	We define a potential function $\Phi$. We need to show that:
+	\begin{equation}
+	\Phi(\text{IN}_n) > \Phi(\text{IN}_{n+1}) \quad \forall n \in \mathbb{N}
+	\end{equation}
+	The potential function is defined as:
+	\begin{equation}
+	\Phi(\text{IN}_n) = \sum_{a \in \text{Agents}(\text{IN}_n)} \begin{cases}
+		4 + 3^{D-d(a)} & \text{ if }a\text{ is of type computational operator} \\
+		3 + 3^{D-d(a)} & \text{ if }a\text{ is of type intermediate} \\
+		1 + 3^{D-d(a)} & \text{ if }a\text{ is a Materialize agent} \\
+		3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\
+		0 & \text{ if }a\text{ is a Carrier, Terminal}
+	\end{cases}
+	\end{equation}
+	where $d(a)$ is the distance of the agent $a$ from the nearest output wire and $D$ the maximum depth
+	of $\text{IN}_0$,
+	We observe that every reduction step $n \to n+1$ strictly reduces $\Phi$:
+	\begin{itemize}
+		\item \textbf{Carrier with Computational Operator}: If a carrier $c$ interacts with an operator agent $o$, it
+			either gets pruned into a new carrier agent closer to the root:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 0 = \Phi(\text{IN}_{n+1})
+			\end{equation}
+			or absorbed into an intermediate agent:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 3 + 3^{D-d(c)} = \Phi(\text{IN}_{n+1})
+			\end{equation}
+		\item \textbf{Carrier with Intermediate}: If a carrier $c$ interacts with an intermediate agent $i$, it
+			either gets pruned into a new carrier agent closer to the root:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1})
+			\end{equation}
+			or temporary Linear agents are wired with Materialize agents, which are then forced to
+			interact to produce terminal agents, then wrapped into a new Linear agent:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} = 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1})
+			\end{equation}
+			If the carrier $c$ interacts with a Materialize agent $i$:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 1 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1})
+			\end{equation}
+		\item \textbf{Carrier with Structural Operator}: If a carrier $c$ is duplicated with the \textit{Dup} or \textit{Eraser}
+			agent $a$, it traverses the agent structure:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
+			\end{equation}
+			if the Dup or Eraser agent interacts with a TermAdd or TermMul, two new agents are created at
+			each auxillary port:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
+			\end{equation}
+	\end{itemize}
+	Since $\Phi$ is a non-negative strictly decreasing function, the reduction
+	process must terminate in a finite number of steps $n$.
+
+	Additionally, since each active pair has exactly one applicable rule the reduction is
+	deterministic. Strong confluence follows immediately, meaning that the normal form is unique
+	regardless of order in which rules are applied.
+\end{proof}