refined core

15 files changed, 1439 insertions, 591 deletions

diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex
index fc4017a..8f46660 100644
--- a/chapters/01-introduction.tex
+++ b/chapters/01-introduction.tex
@@ -20,7 +20,7 @@ either hold or are violated. The kind of properties that can be verified are two
 An example of a Multi-Network property is equivalence between different neural networks; this
 verification is crucial when replacing a neural network with a smaller, equivalent one. Techniques
 based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in the verification
-algorithm, however, as networks grow in depth and width, the number of non-linear components, most
+algorithm. However, as networks grow in depth and width, the number of non-linear components, most
 notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is the input to the
 neuron.} (ReLU) activation function, creates an exponential search space for the solver. Because of
 this issue, running a solver against a raw, unoptimized network is often computationally prohibitive.
diff --git a/chapters/03-core.tex b/chapters/03-core.tex
index f9a4cab..170cf06 100644
--- a/chapters/03-core.tex
+++ b/chapters/03-core.tex
@@ -3,7 +3,7 @@
 
 This chapter contains details on framework implementation (\textbf{\Cref{sec:implementation}}), the
 proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}) and a collection of data
-gathered from benchmarks (\textbf{\Cref{sec:benchmarks}})
+gathered from benchmarks (\textbf{\Cref{sec:benchmarks}}).
 
 \input{chapters/core/01-implementation}
 
diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex
index 3e8fa20..32154ef 100644
--- a/chapters/core/01-implementation.tex
+++ b/chapters/core/01-implementation.tex
@@ -1,7 +1,7 @@
 \section{Implementation}
 \label{sec:implementation}
 
-This sections contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}),
+This section contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}),
 the interaction rules designed (\textbf{\Cref{sec:interaction-rules}}), the algorithm used in the
 ONNX-to-IN translation (\textbf{\Cref{sec:translation}}) and the Python module (\textbf{\Cref{sec:python-module}}).
 
diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex
index 40c1986..132b56d 100644
--- a/chapters/core/03-benchmarks.tex
+++ b/chapters/core/03-benchmarks.tex
@@ -1,4 +1,86 @@
 \section{Benchmarks}
 \label{sec:benchmarks}
 
-% This section contains the varius benchmarks
+This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}.
+
+VEIN was tested on a laptop Zenbook UX3402ZA with:
+\begin{itemize}
+	\item \textbf{CPU}: 12th Gen Intel Core i5-1240P
+	\item \textbf{RAM}: 8GiB
+	\item \textbf{SWAP}: 16GiB on NVMe
+\end{itemize}
+using Hyperfine\footnote{\href{https://github.com/sharkdp/hyperfine}{\textbf{Hyperfine Github repository}}.}
+benchmarking tool. Hyperfine runs the test ten times, then reports the mean and standard deviation of
+execution time.
+
+\paragraph{Iris}
+Dataset of iris flowers presented by Fisher et al.~\cite{fisher1936iris}. It consists of three
+species of flower (\textit{Iris setosa}, \textit{Iris virginica} and \textit{Iris versicolor}) with fifty samples each. Each
+sample has four features: width and length of sepals and petals.
+\paragraph{Pendulum}
+A neural safety certificate for stabilizing a pendulum to its upright position under a bound on its
+angle $\theta$, with state $x=[\theta,\dot\theta]\in\mathbb{R}^2$ and nonlinear dynamics.
+\paragraph{Double Integrator}
+A neural safety certificate for stabilizing a second-order linear system to the origin under a bound
+on its position $p$, with state $x=[p,\dot p]\in\mathbb{R}^2$.
+\paragraph{MNIST}
+Widely known dataset of handwritten digits presented by LeCun et al.~\cite{lecun2010mnist}. It
+consists of 60'000 training images and 10'000 testing images.
+
+Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et
+al.~\cite{kaulen20256thinternationalverificationneural}. We check equivalence between a pre-trained
+and a fine-tuned network for each task.
+
+In the Iris and MNIST dataset, we tested equivalence between a NN and its ad-hoc transformation,
+such as pruning always positive or negative ReLUs, as presented by Kumar et al.~\cite{kumar2019equivalentapproximatetransformationsdeep},
+or changing the architecture from wide to deep and viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}.
+
+For two NN $F: \mathbb{R}^n \to \mathbb{R}^m$ and $F': \mathbb{R}^n \to \mathbb{R}^m$, Eleftheriadis et al.~\cite{eleftheriadis2022equivalence}
+define three kinds of equivalence:
+\begin{itemize}
+	\item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \quad F(x) = F'(x)$.
+	\item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \quad ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$.
+	\item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \quad \mathtt{argmax}(F(x))=\mathtt{argmax}(F'(x))$ where \texttt{argmax}
+		is the function that returns the index of the maximum value of a vector.
+\end{itemize}
+
+\begin{table}[H]
+	\centering
+	\begin{tabular}[t]{ccccc}
+		\hline
+		Benchmark & Equivalence & Direct [s] & VEIN [s] & Status \\
+		\hline
+		Iris (Stably Active) & Strict & 0.0 & 0.0 & X \\
+		Iris (Stably Active) & Epsilon & 0.0 & 0.0 & X \\
+		Iris (Stably Active) & Argmax & 0.0 & 0.0 & X \\
+		Iris (Stably Inactive) & Strict & 0.0 & 0.0 & X \\
+		Iris (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\
+		Iris (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\
+		Iris (To Wide) & Strict & 0.0 & 0.0 & X \\
+		Iris (To Wide) & Epsilon & 0.0 & 0.0 & X \\
+		Iris (To Wide) & Argmax & 0.0 & 0.0 & X \\
+		Iris (To Deep) & Strict & 0.0 & 0.0 & X \\
+		Iris (To Deep) & Epsilon & 0.0 & 0.0 & X \\
+		Iris (To Deep) & Argmax & 0.0 & 0.0 & X \\
+		Pendulum & Strict & 0.0 & 88.427 ± 0.670 & SAT \\
+		Pendulum & Epsilon & 0.0 & 0.0 & X \\
+		Pendulum & Argmax & 0.0 & 0.0 & X \\
+		Double Integrator & Strict & 0.0 & 0.0 & X \\
+		Double Integrator & Epsilon & 0.0 & 0.0 & X \\
+		Double Integrator & Argmax & 0.0 & 0.0 & X \\
+		MNIST (Stably Active) & Strict & 0.0 & 0.0 & X \\
+		MNIST (Stably Active) & Epsilon & 0.0 & 0.0 & X \\
+		MNIST (Stably Active) & Argmax & 0.0 & 0.0 & X \\
+		MNIST (Stably Inactive) & Strict & 0.0 & 0.0 & X \\
+		MNIST (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\
+		MNIST (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\
+		MNIST (To Wide) & Strict & 0.0 & 0.0 & X \\
+		MNIST (To Wide) & Epsilon & 0.0 & 0.0 & X \\
+		MNIST (To Wide) & Argmax & 0.0 & 0.0 & X \\
+		MNIST (To Deep) & Strict & 0.0 & 0.0 & X \\
+		MNIST (To Deep) & Epsilon & 0.0 & 0.0 & X \\
+		MNIST (To Deep) & Argmax & 0.0 & 0.0 & X \\
+	\end{tabular}
+	\caption{Benchmark table.}
+	\label{tab:benchmarks}
+\end{table}
diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex
index 5b2eab9..eeebf47 100644
--- a/chapters/core/implementation/01-inpla.tex
+++ b/chapters/core/implementation/01-inpla.tex
@@ -1,7 +1,7 @@
-\subsection{Inpla fork}
+\subsection{INPLA fork}
 \label{sec:inpla}
 
-The  VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}},
+The VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}},
 a multi-threaded parallel interpreter of IN. Performance and ease of use motivated the choice of
 INPLA. Additionally, it supports attribute values, which is a special extension that allows agents
 to hold numerical values at their ports.
@@ -18,38 +18,48 @@ Several modifications adapt INPLA to the pipeline of the framework:
 \end{itemize}
 
 \paragraph{INPLA syntax}
-INPLA evaluates nets, they consist of connections between terms. Terms are built on names and agents:
+INPLA evaluates nets which consist of connections between terms. Terms are built on names and agents:
+\begin{small}
 \begin{verbatim}
 <term> ::= <name> | <agent>
 <name> ::= <nameID>
 <agent> ::= <agentID>
-          | <agentID> ['(' <term> ',' ... ',' <term> ')']
+					| <agentID> ['(' <term> ',' ... ',' <term> ')']
 \end{verbatim}
+\end{small}
 \begin{itemize}
 	\item \textbf{Name}: it works as a buffer between terms.
 	\item \textbf{Agent}: it works as a constructor and de-constructor (defined functions).
 \end{itemize}
 A connection is a relation between two terms and the symbol \texttt{\~} expresses this relation.
 Interaction rules rewrite connections between agents:
+\begin{small}
 \begin{verbatim}
 <interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';'
 <rule-agent> ::= <agentID>
-               | <agentID> '(' <name> ',' ... ',' <name> ')'
+							 | <agentID> '(' <name> ',' ... ',' <name> ')'
 \end{verbatim}
+\end{small}
 
 \paragraph{Example}
 Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For
 instance, 0, 1, 2, 3 are expressed as \texttt{Z}, \texttt{S(Z)}, \texttt{S(S(Z))}, \texttt{S(S(S(Z)))}. Here, let's think about an
-increment operation "inc" such that:
+increment operation ``inc'' such that:
+\begin{small}
 \begin{verbatim}
 inc(n) = S(n).
 \end{verbatim}
+\end{small}
 This is written as the following rules:
+\begin{small}
 \begin{verbatim}
 inc(r) >< Z => r ~ S(Z);
 inc(r) >< S(x) => r ~ S(S(x));
 \end{verbatim}
+\end{small}
 Then, the result of \texttt{inc(r) \~{} S(S(Z))} is:
+\begin{small}
 \begin{verbatim}
 r ~ S(S(S(Z)));
 \end{verbatim}
+\end{small}
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index b657ee9..49a8a70 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -10,13 +10,17 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 			\item \textbf{Concrete}: Represents a constant value $k$.
 		\end{itemize}
 	\item
-		\textbf{Operators}: Agents that perform some kind of operation on the carrier agents.
+		\textbf{Computational Operators}: Agents that perform some kind of operation on the carrier agents.
 		\begin{itemize}
 			\item \textbf{Add}: Binary operator for addition.
 			\item \textbf{Mul}: Binary operator for multiplication.
 			\item \textbf{ReLU}: Unary operator for rectified linear unit.
+		\end{itemize}
+	\item
+		\textbf{Structural Operators}: Agents that perform some kind of operation on net structure.
+		\begin{itemize}
 			\item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents.
-			\item \textbf{Duplicator}: Built-in INPLA unary operator to duplicate other agents.
+			\item \textbf{Dup}: Built-in INPLA unary operator to duplicate other agents.
 		\end{itemize}
 	\item
 		\textbf{Intermediates}: Agents needed to perform each step of the operators.
@@ -28,32 +32,37 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 			\item \textbf{Materialize}: Converts a Linear agent into an explicit representation for the SMT solver.
 		\end{itemize}
 	\item
-		\textbf{Inerts}: Agents that compose the normal form.
+		\textbf{Terminals}: Agents that compose the normal form.
 		\begin{itemize}
 			\item \textbf{TermAdd}: This agent is parsed as addition for the SMT solver.
 			\item \textbf{TermMul}: This agent is parsed as multiplication for the SMT solver.
 			\item \textbf{TermReLU}: This agent is parsed as rectified linear unit for the SMT solver.
-			\item \textbf{Symbolic}: This agent is parsed as specific variable for the SMT solver.
+			\item \textbf{TermSymbolic}: This agent is parsed as a specific variable for the SMT solver.
+			\item \textbf{TermConcrete}: This agent is parsed as a real value for the SMT solver.
 		\end{itemize}
 \end{itemize}
 
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
-		\begin{tabular}{cccc}
+		\begin{tabular}{ccccc}
 			% Linear
+			&
 			\begin{tikzpicture}
 				\agentLinear{L}{q}{r}
 				\inetwirefree(L.pal) \inetwirefree(L.pax)
 				\node[below] at (L.above pal) {$\mathit{out}$};
 				\node[above] at (L.above pax) {$\mathit{x}$};
 			\end{tikzpicture} &
+			&
 			% Concrete
 			\begin{tikzpicture}
 				\agentConcrete{C}{k}
 				\inetwirefree(C.pal)
 				\node[below] at (C.above pal) {$\mathit{out}$};
-			\end{tikzpicture} &
+			\end{tikzpicture} & \\
+			& (a) $\mathit{Linear}$ & & (b) $\mathit{Concrete}$ & \\[0.5cm]
+
 			% Add
 			\begin{tikzpicture}
 				\agentAdd{A}
@@ -69,9 +78,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 				\node[below] at (M.above pal) {$\mathit{a}$};
 				\node[above] at (M.above pax 1) {$\mathit{out}$};
 				\node[above] at (M.above pax 2) {$\mathit{b}$};
-			\end{tikzpicture} \\
-			(a) $\mathit{Linear}$ & (b) $\mathit{Concrete}$ & (c) $\mathit{Add}$ & (d) $\mathit{Mul}$ \\[0.5cm]
-
+			\end{tikzpicture} &
 			% ReLU
 			\begin{tikzpicture}
 				\agentReLU{R}
@@ -79,13 +86,6 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 				\node[below] at (R.above pal) {$\mathit{x}$};
 				\node[above] at (R.above pax) {$\mathit{out}$};
 			\end{tikzpicture} &
-			% Materialize
-			\begin{tikzpicture}
-				\agentMaterialize{MAT}
-				\inetwirefree(MAT.pal) \inetwirefree(MAT.pax)
-				\node[below] at (MAT.above pal) {$\mathit{x}$};
-				\node[above] at (MAT.above pax) {$\mathit{out}$};
-			\end{tikzpicture} &
 			% Eraser
 			\begin{tikzpicture}
 				\agentEraser{E}
@@ -100,7 +100,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 				\node[above] at (D.above pax 1) {$\mathit{d_{1}}$};
 				\node[above] at (D.above pax 2) {$\mathit{d_{2}}$};
 			\end{tikzpicture} \\
-			(e) $\mathit{ReLU}$ & (f) $\mathit{Materialize}$ & (g) $\mathit{Eraser}$ & (h) $\mathit{Duplicator}$ \\[0.5cm]
+			(c) $\mathit{Add}$ & (d) $\mathit{Mul}$ & (e) $\mathit{ReLU}$ & (f) $\mathit{Eraser}$ & (g) $\mathit{Duplicator}$ \\[0.5cm]
 
 			% AddCheckLinear
 			\begin{tikzpicture}
@@ -131,8 +131,15 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 				\inetwirefree(MC.pal) \inetwirefree(MC.pax)
 				\node[below] at (MC.above pal) {$\mathit{b}$};
 				\node[above] at (MC.above pax) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% Materialize
+			\begin{tikzpicture}
+				\agentMaterialize{MAT}
+				\inetwirefree(MAT.pal) \inetwirefree(MAT.pax)
+				\node[below] at (MAT.above pal) {$\mathit{x}$};
+				\node[above] at (MAT.above pax) {$\mathit{out}$};
 			\end{tikzpicture} \\
-			(i) $\mathit{AddCheckLinear}$ & (j) $\mathit{MulCheckLinear}$ & (k) $\mathit{AddCheckConcrete}$ & (l) $\mathit{MulCheckConcrete}$ \\[0.5cm]
+			(h) $\mathit{AddCheckLinear}$ & (i) $\mathit{MulCheckLinear}$ & (j) $\mathit{AddCheckConcrete}$ & (k) $\mathit{MulCheckConcrete}$ & (l) $\mathit{Materialize}$ \\[0.5cm]
 
 			% TermAdd
 			\begin{tikzpicture}
@@ -157,13 +164,19 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 				\node[below] at (TR.above pal) {$\mathit{out}$};
 				\node[above] at (TR.above pax) {$\mathit{x}$};
 			\end{tikzpicture} &
-			% Symbolic
+			% TermSymbolic
 			\begin{tikzpicture}
-				\agentSymbolic{S}{id}
+				\agentTermSymbolic{S}{id}
 				\inetwirefree(S.pal)
 				\node[below] at (S.above pal) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% TermConcrete
+			\begin{tikzpicture}
+				\agentTermConcrete{C}{k}
+				\inetwirefree(C.pal)
+				\node[below] at (C.above pal) {$\mathit{out}$};
 			\end{tikzpicture} \\
-			(m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{Symbolic}$ \\[0.5cm]
+			(m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm]
 		\end{tabular}
 	}
 	\caption{Agents used in VEIN.}
@@ -178,7 +191,7 @@ operators need to check one operand a time. For this reason \textit{Add} and \te
 principal port faces the other operand.
 
 % Linear >< Add
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentLinear{L}{q}{r}[90]
@@ -200,7 +213,7 @@ principal port faces the other operand.
 \end{figure}
 
 % Linear >< Mul
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentLinear{L}{q}{r}[90]
@@ -230,7 +243,7 @@ This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1
 before it is even invoked.
 
 % Concrete >< Add
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -270,7 +283,7 @@ before it is even invoked.
 \end{figure}
 
 % Concrete >< Mul
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -338,7 +351,7 @@ to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Lin
 $q=1,r=0$.
 
 % Linear >< AddCheckLinear
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -426,7 +439,7 @@ $q=1,r=0$.
 \end{figure}
 
 % Linear >< MulCheckLinear
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -485,7 +498,7 @@ For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system
 the \textit{Concrete} agent to both the attributes of the \textit{Linear}
 
 % Concrete >< AddCheckLinear
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentConcrete{C}{j}[90]
@@ -505,7 +518,7 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear}
 \end{figure}
 
 % Concrete >< MulCheckLinear
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentConcrete{C}{j}[90]
@@ -529,7 +542,7 @@ In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \text
 we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}.
 
 % Linear >< AddCheckConcrete
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentLinear{L}{s}{t}[90]
@@ -549,7 +562,7 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a
 \end{figure}
 
 % Linear >< MulCheckConcrete
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\interactionrule{
 		\agentLinear{L}{s}{t}[90]
@@ -574,7 +587,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 \textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules.
 
 % Concrete >< AddCheckConcrete
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -610,7 +623,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 \end{figure}
 
 % Concrete >< MulCheckConcrete
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -659,7 +672,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 \end{figure}
 
 \paragraph{Linear/Concrete with ReLU}
-When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no
+When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is not
 enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
 the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}.
 In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent
@@ -667,7 +680,7 @@ meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either
 if $k>0$ or with attribute equal $0$ otherwise.
 
 % Linear >< ReLU
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\interactionrule{
@@ -693,7 +706,7 @@ if $k>0$ or with attribute equal $0$ otherwise.
 \end{figure}
 
 % Concrete >< ReLU
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -729,13 +742,13 @@ if $k>0$ or with attribute equal $0$ otherwise.
 \end{figure}
 
 \paragraph{Linear/Concrete with Materialize}
-When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd} and \textit{TermMul}
+When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd}, \textit{TermMul} and \textit{TermConcrete}
 to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}.
-When a \textit{Concrete} needs to be materialized nothing needs to be done and it is directly wired to output
+When a \textit{Concrete} needs to be materialized it is converted into \textit{TermConcrete} as illustrated in
 \textbf{\Cref{fig:rule-concrete-materialize}}.
 
 % Linear >< Materialize
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\begin{tabular}{c}
@@ -750,8 +763,8 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 			}{
 				\agentTermAdd{TA}[90]
 				\agentTermMul[left=of TA.pax 1]{TM}[90]
-				\agentConcrete[left=of TA.pax 2, below=of TM]{C1}{r}[90]
-				\agentConcrete[left=of TM.pax 1]{C2}{q}[90]
+				\agentTermConcrete[left=of TA.pax 2, below=of TM]{C1}{r}[90]
+				\agentTermConcrete[left=of TM.pax 1]{C2}{q}[90]
 				\inetwire(TA.pax 1)(TM.pal) \inetwire(TA.pax 2)(C1.pal) \inetwire(TM.pax 1)(C2.pal)
 				\inetwirefree(TA.pal) \inetwirefree(TM.pax 2)
 				\node [left] at (TM.above pax 2) {$\mathit{x}$};
@@ -767,7 +780,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [left] at (L.above pax) {$\mathit{x}$};
 				\node [right] at (MAT.above pax) {$\mathit{out}$};
 			}{
-				\agentConcrete{C}{r}[90]
+				\agentTermConcrete{C}{r}[90]
 				\agentEraser[below=of C]{E}[90]
 				\inetwirefree(C.pal) \inetwirefree(E.pal)
 				\node [right] at (C.above pal) {$\mathit{out}$};
@@ -798,7 +811,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [right] at (MAT.above pax) {$\mathit{out}$};
 			}{
 				\agentTermAdd{TA}[90]
-				\agentConcrete[left=of TA.right pax]{C}{r}[90]
+				\agentTermConcrete[left=of TA.right pax]{C}{r}[90]
 				\inetwire(C.pal)(TA.pax 2)
 				\inetwirefree(TA.pax 1) \inetwirefree(TA.pal)
 				\node [left] at (TA.above pax 1) {$\mathit{x}$};
@@ -815,7 +828,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [right] at (MAT.above pax) {$\mathit{out}$};
 			}{
 				\agentTermMul{TM}[90]
-				\agentConcrete[left=of TM.left pax]{C}{q}[90]
+				\agentTermConcrete[left=of TM.left pax]{C}{q}[90]
 				\inetwire(C.pal)(TM.pax 1)
 				\inetwirefree(TM.pax 2) \inetwirefree(TM.pal)
 				\node [left] at (TM.above pax 2) {$\mathit{x}$};
@@ -828,7 +841,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 \end{figure}
 
 % Concrete >< Materialize
-\begin{figure}[ht]
+\begin{figure}[H]
 	\centering
 	\resizebox{\textwidth}{!}{
 		\interactionrule{
@@ -838,7 +851,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 			\inetwirefree(MAT.pax)
 			\node [right] at (MAT.above pax) {$\mathit{out}$};
 		}{
-			\agentConcrete{C}{k}[90]
+			\agentTermConcrete{C}{k}[90]
 			\inetwirefree(C.pal)
 			\node [right] at (C.above pal) {$\mathit{out}$};
 		}
diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex
index 638ff17..0a2eec0 100644
--- a/chapters/core/implementation/03-translation.tex
+++ b/chapters/core/implementation/03-translation.tex
@@ -11,15 +11,7 @@ to be able to instantiate the correct number of \textit{Dup} agents. The main al
 in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interactions} dictionary data-structure, that maps each tensor
 name to a list of ports, to keep track of the graph traversal.
 
-To maximize the concurrency of the INPLA engine, the translation layer avoids generating linear
-chains of agents, opting instead for balanced binary trees for signal distribution (single input to
-multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}}
-and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains)
-is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the
-agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the
-\textit{Fan-Out} they are facing the root.
-
-\begin{algorithm}[ht]
+\begin{algorithm}[H]
 	\caption{Backwards ONNX-to-IN Translation}
 	\label{alg:onnx-to-in}
 	\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
@@ -67,22 +59,31 @@ agents together: in the \textit{Fan-In} the principal port of the agents are fac
 					$S.\text{append}(root \sim sink)$
 				}
 			}
-			\Case{Identity}{
-				$interactions[N.input] \leftarrow interactions[N.output]$
-			}
 		}
 	}
 
 	\ForEach{neuron $x$ in $G.input$}{
 		$sink \leftarrow \text{BalancedFanOut}(interactions[G.input][x], \text{Dup}, S)$
 
-		$S.\text{append}(sink \sim \text{Linear}(\text{Symbolic}(x), 1.0, 0.0))$
+		$S.\text{append}(sink \sim \text{Linear}(\text{TermSymbolic}(x), 1.0, 0.0))$
+	}
+
+	\ForEach{$y$ in $\text{len}(interactions[G.output])$}{
+		$S.\text{append}(result_y)$
 	}
 
 	\Return{S}
 \end{algorithm}
 
-\begin{algorithm}[ht]
+To maximize the concurrency of the INPLA engine, the translation layer avoids generating linear
+chains of agents, opting instead for balanced binary trees for signal distribution (single input to
+multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}}
+and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains)
+is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the
+agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the
+\textit{Fan-Out} they are facing the root.
+
+\begin{algorithm}[H]
 	\caption{Balanced Fan-In}
 	\label{alg:balanced-fan-in}
 	\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
@@ -111,8 +112,7 @@ agents together: in the \textit{Fan-In} the principal port of the agents are fac
 	\Return{$T[0]$}
 \end{algorithm}
 
-
-\begin{algorithm}[ht]
+\begin{algorithm}[H]
 	\caption{Balanced Fan-Out}
 	\label{alg:balanced-fan-out}
 	\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
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}
diff --git a/cmds.tex b/cmds.tex
new file mode 100644
index 0000000..b7f3534
--- /dev/null
+++ b/cmds.tex
@@ -0,0 +1,196 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%							COMMANDS						  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	TODO annotations
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\MP}[1]{\todo[color=blue!30]{MP TODO: #1}}
+\newcommand{\MPin}[1]{\todo[color=blue!30,inline]{MP TODO: #1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Math formatting
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% some shortcuts
+\newcommand{\mi}[1]{\ensuremath{\mathit{#1}}}
+\newcommand{\mr}[1]{\ensuremath{\mathrm{#1}}}
+\newcommand{\mt}[1]{\ensuremath{\texttt{#1}}}
+\newcommand{\mtt}[1]{\ensuremath{\mathtt{#1}}}
+\newcommand{\mf}[1]{\ensuremath{\mathbf{#1}}}
+\newcommand{\mk}[1]{\ensuremath{\mathfrak{#1}}}
+\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
+\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
+\newcommand{\mb}[1]{\ensuremath{\mathbb{#1}}}
+\newcommand{\msc}[1]{\ensuremath{\mathscr{#1}}}
+
+\DeclareMathOperator\mydefsym{\ensuremath{\iangleq}}
+\newcommand{\bnfdef}[0]{\ensuremath{\mathrel{::=}}}
+\newcommand{\isdef}[0]{\ensuremath{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\sffamily def}}}{=}}}}
+
+% http://tex.stackexchange.com/questions/5502/how-to-get-a-mid-binary-relation-that-grows
+\newcommand{\relmiddle}[1]{\mathrel{}\middle#1\mathrel{}}
+\newcommand{\myset}[2]{\ensuremath{\left\{#1 ~\relmiddle|~ #2\right\}}}
+
+\newcommand{\divr}[0]{\ensuremath{\!\!\Uparrow}\xspace}
+\newcommand{\term}[0]{\ensuremath{\!\!\Downarrow}\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Compiler 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\genlang}[2]{\ensuremath{\lambda^{#1}_{#2}}}
+\newcommand{\genlangF}[2]{\ensuremath{F^{#1}_{#2}}}
+
+\newcommand{\ulc}[0]{\bl{\genlang{u}{}}}
+\newcommand{\stlc}[0]{\src{\genlang{\tau}{}}}
+\newcommand{\sysf}[0]{\oth{\genlangF{\forall}{}}}
+
+\newcommand{\funname}[1]{\mtt{#1}}
+\newcommand{\fun}[2]{\ensuremath{{\bl{\funname{#1}\left(#2\right)}}}\xspace}
+\newcommand{\dom}[1]{\fun{dom}{#1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Language shortcuts
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\ctx}[0]{\ensuremath{\mk{C}}}
+\newcommand{\ctxh}[1]{\ctx\hole{#1}}
+\newcommand{\hole}[1]{\ensuremath{\left[#1\right]}}
+\newcommand{\evalctx}[0]{\ensuremath{\mb{E}}}
+
+\newcommand{\srce}[0]{\src{\emptyset}\xspace}
+\newcommand{\trge}[0]{\trgb{\emptyset}\xspace}
+\newcommand{\come}[0]{\com{\emptyset}\xspace}
+\newcommand{\othe}[0]{\oth{\emptyset}\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Language formatting
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\neutcol}[0]{black}
+\newcommand{\stlccol}[0]{RoyalBlue}
+\newcommand{\ulccol}[0]{RedOrange}
+\newcommand{\commoncol}[0]{black}    % CarnationPink
+\newcommand{\othercol}[0]{CarnationPink}
+
+\newcommand{\col}[2]{\ensuremath{{\color{#1}{#2}}}}
+
+\newcommand{\src}[1]{\ms{\col{\stlccol}{#1}}}
+\newcommand{\trgb}[1]{\ensuremath{\bm{\col{\ulccol }{#1}}}}
+\newcommand{\trg}[1]{{\mf{\col{\ulccol }{#1}}}}
+\newcommand{\oth}[1]{\mi{\col{\othercol }{#1}}}
+% MARCO: \bm is notorious to break things around. it's there only to make bold math letters. we can remove it if necessary.
+% it is currently removed -- the paretheses are still there though -- as it did go beyond its scope, i did not know how to remove it (\mr did nont work)
+% it was affecting stuff inside the compilation brackets, making source stuff bold ... 
+%if we know of a solution, we can add \bm at the beginning here and the bold-removal command in the core of \compgen
+\newcommand{\bl}[1]{\col{\neutcol }{#1}}
+\newcommand{\com}[1]{\mi{\col{\commoncol }{#1}}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Type rules
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcounter{typerule}
+\crefname{typerule}{rule}{rules}
+
+\newcommand{\typeruleInt}[5]{%									    % #1 is the title, #2 is the hypotheses. #3 is the thesis, #4 is the label for referencing
+	\def\thetyperule{#1}%
+	\refstepcounter{typerule}%
+	\label{tr:#4}%
+  \ensuremath{\begin{array}{c}#5 \inference{#2}{#3}\end{array}} 
+}
+\newcommand{\typerule}[4]{%									        % #1 is the title, #2 is the hypotheses. #3 is the thesis, #4 is the label for referencing
+  \typeruleInt{#1}{#2}{#3}{#4}{\textsf{\scriptsize ({#1})} \\      }
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%	Contextual equivalence
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\DeclareMathOperator\niff{\ensuremath{\nLeftrightarrow}}
+\DeclareMathOperator\nsimeq{\ensuremath{\mathrel{\not\simeq}}}
+
+\DeclareMathOperator\ceq{\ensuremath{\mathrel{\simeq_{\mi{ctx}}}}}
+\DeclareMathOperator\nceq{\mathrel{\nsimeq_{\mi{ctx}}}}
+
+\DeclareMathOperator\ceqs{\src{\ceq}}
+\DeclareMathOperator\ceqt{\trgb{\ceq}}
+\DeclareMathOperator\ceqo{\oth{\ceq}}
+
+\DeclareMathOperator\nceqs{\src{\nceq}}
+\DeclareMathOperator\nceqt{\trgb{\nceq}}
+\DeclareMathOperator\nceqo{\oth{\nceq}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Missing envs
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\theoremstyle{definition}
+\newtheorem{assumption}{Assumption}
+\newtheorem{notation}{Notation}
+\newtheorem{definition}{Definition}
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}
+\newtheorem{property}{Property}
+\newtheorem{example}{Example}
+\newtheorem{informal}{Informal definition}
+\newtheorem{corollary}{Corollary}
+
+\Crefname{corollary}{Corollary}{Corollaries}
+\Crefname{informal}{Definition}{Definition}
+\Crefname{assumption}{Assumption}{Assumptions}
+\crefname{assumption}{Assumption}{Assumptions}
+\Crefname{property}{Property}{Properties}
+\crefname{property}{Property}{Properties}
+\Crefname{lstlisting}{Listing}{Listings}
+\Crefname{problem}{Problem}{Problems}
+\Crefname{equation}{Rule}{Rules}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Lambda 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\DeclareMathOperator\op{\ensuremath{\oplus}}
+
+\newcommand{\lam}[2]{\ensuremath{\lambda #1\ldotp #2}}
+\newcommand{\pair}[1]{\ensuremath{\left\langle#1\right\rangle}}
+\newcommand{\projone}[1]{\ensuremath{#1.1}}
+\newcommand{\projtwo}[1]{\ensuremath{#1.2}}
+\newcommand{\caseof}[3]{\ensuremath{{case}~#1~{of}~\inl{x_1}\mapsto #2\mid\inr{x_2}\mapsto #3}}
+\newcommand{\inl}[1]{\ensuremath{{inl}~#1}}
+\newcommand{\inr}[1]{\ensuremath{{inr}~#1}}
+\newcommand{\fold}[1]{\ensuremath{{fold}_{#1}}}
+\newcommand{\unfold}[1]{\ensuremath{{unfold}_{#1}}}
+\newcommand{\Lam}[2]{\ensuremath{\Lambda #1\ldotp #2}}
+\newcommand{\tapp}[2]{\ensuremath{#1 \hole{#2}}}
+\newcommand{\pack}[3]{\ensuremath{{pack}~\pair{#1,#2}~{as}~#3}}
+\newcommand{\unpack}[4]{\ensuremath{{unpack}~#1~{as}~\pair{#2,#3}~{in}~#4}}
+
+\newcommand{\type}[3]{\ensuremath{ \left\{#1:#2\relmiddle|#3 \right\}}}
+
+\newcommand{\matgen}[2]{\ensuremath{\mu #1\ldotp#2}}
+\newcommand{\mat}[0]{\matgen{\alpha}{\tau}}
+\newcommand{\fatgen}[2]{\ensuremath{\forall #1\ldotp#2}}
+\newcommand{\fat}[0]{\fatgen{\alpha}{\tau}}
+\newcommand{\eatgen}[2]{\ensuremath{\exists #1\ldotp#2}}
+\newcommand{\eat}[0]{\eatgen{\alpha}{\tau}}
+% \newcommand{\fatgent}[2]{\ensuremath{\trgb{\forall} #1\ldotp#2}}
+% \newcommand{\fatt}[0]{\fatgent{\alpt}{\tat}}
+% \newcommand{\eatgent}[2]{\ensuremath{\trgb{\exists} #1\ldotp#2}}
+% \newcommand{\eatt}[0]{\eatgent{\alpt}{\tat}}
+
+\newcommand{\fail}[0]{\mi{fail}}
+
+\newcommand{\redgen}[1]{\ensuremath{ \hookrightarrow^{#1} }}
+\newcommand{\nredgen}[1]{\ensuremath{\not\hookrightarrow^{#1}}}
+\DeclareMathOperator\red{\redgen{}}
+
+\newcommand{\nred}[0]{\nredgen{}}
+\newcommand{\redstar}[0]{\redgen{*}}
+
+\newcommand{\bigredgen}[1]{\ensuremath{ \Downarrow^{#1} }}
+\newcommand{\nbigredgen}[1]{\ensuremath{\not\Downarrow^{#1}}}
+\DeclareMathOperator\bigs{\bigredgen{}}
+
+\newcommand{\credgen}[1]{\ensuremath{ \leadsto^{#1} }}
+\newcommand{\ncredgen}[1]{\ensuremath{\not\leadsto^{#1}}}
+\DeclareMathOperator\cred{\credgen{}}
+\DeclareMathOperator\credp{\credgen{p}}
+
+\newcommand{\subst}[2]{\ensuremath{\bl{\left[#1\relmiddle/#2\right]}}} %replace 1 in place of 2
+\newcommand{\subs}[2]{\subst{\src{#1}}{\src{#2}}}
+\newcommand{\subt}[2]{\subst{\trg{#1}}{\trg{#2}}}
+\newcommand{\subo}[2]{\subst{\oth{#1}}{\oth{#2}}}
diff --git a/macros.tex b/macros.tex
index 32b4789..333f3ac 100644
--- a/macros.tex
+++ b/macros.tex
@@ -58,9 +58,13 @@
 \newcommand{\agentTermReLU}[2][]{% [#1=options, #2=name]
 	\inetcell[arity=1, #1](#2){$\mathit{TR}$}
 }
-% Symbolic
-\newcommand{\agentSymbolic}[3][]{% [#1=options, #2=name, #3=symbol]
-	\inetcell[arity=0, #1](#2){$\mathit{S_{#3}}$}
+% TermSymbolic
+\newcommand{\agentTermSymbolic}[3][]{% [#1=options, #2=name, #3=symbol]
+	\inetcell[arity=0, #1](#2){$\mathit{TS_{#3}}$}
+}
+% TermConcrete
+\newcommand{\agentTermConcrete}[3][]{% [#1=options, #2=name, #3=k]
+	\inetcell[arity=0, #1](#2){$\mathit{TC}_{#3}$}
 }
 % Interaction Rule
 \newcommand{\interactionrule}[3][]{
diff --git a/main.tex b/main.tex
index 21356f3..384a751 100644
--- a/main.tex
+++ b/main.tex
@@ -10,10 +10,11 @@
 \usepackage[nameinlink]{cleveref}
 \usepackage{xspace}
 \usepackage[colorinlistoftodos]{todonotes}
-% \usepackage[scaled=.83]{beramono} 
+\usepackage[scaled=.83]{beramono} 
 \usepackage{lineno}
 \usepackage{tikz-inet}
 \usepackage{stmaryrd}
+\usepackage{float}
 
 \usetikzlibrary{calc}
 \linenumbers
@@ -21,6 +22,7 @@
 \Crefname{algocf}{Algorithm}{Algorithms}
 
 \input{macros}
+\input{cmds}
 
 \title{VEIN: VErification via Interaction Nets for Neural Networks}
 \author{Eric Marin}
diff --git a/references.bib b/references.bib
index 8ddabea..194a8b4 100644
--- a/references.bib
+++ b/references.bib
@@ -16,9 +16,9 @@
 }
 @inproceedings{demoura2008z3,
 	author="de Moura, Leonardo
-	and Bj{\o}rner, Nikolaj",
+		and Bj{\o}rner, Nikolaj",
 	editor="Ramakrishnan, C. R.
-	and Rehof, Jakob",
+		and Rehof, Jakob",
 	title="Z3: An Efficient SMT Solver",
 	booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
 	year="2008",
@@ -28,4 +28,116 @@
 	abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.",
 	isbn="978-3-540-78800-3"
 }
+@misc{kumar2019equivalentapproximatetransformationsdeep,
+	title={Equivalent and Approximate Transformations of Deep Neural Networks}, 
+	author={Abhinav Kumar and Thiago Serra and Srikumar Ramalingam},
+	year={2019},
+	eprint={1905.11428},
+	archivePrefix={arXiv},
+	primaryClass={cs.LG},
+	url={https://arxiv.org/abs/1905.11428}, 
+}
+@article{JMLR:v24:21-0579,
+	author  = {Fenglei Fan and Rongjie Lai and Ge Wang},
+	title   = {Quasi-Equivalence between Width and Depth of Neural Networks},
+	journal = {Journal of Machine Learning Research},
+	year    = {2023},
+	volume  = {24},
+	number  = {183},
+	pages   = {1--22},
+	url     = {http://jmlr.org/papers/v24/21-0579.html}
+}
+@misc{kaulen20256thinternationalverificationneural,
+	title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, 
+	author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu},
+	year={2025},
+	eprint={2512.19007},
+	archivePrefix={arXiv},
+	primaryClass={cs.LG},
+	url={https://arxiv.org/abs/2512.19007}, 
+}
+@article{fisher1936iris,
+	author = {FISHER, R. A.},
+	title = {THE USE OF MULTIPLE MEASUREMENTS IN TAXONOMIC PROBLEMS},
+	journal = {Annals of Eugenics},
+	volume = {7},
+	number = {2},
+	pages = {179-188},
+	doi = {https://doi.org/10.1111/j.1469-1809.1936.tb02137.x},
+	url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1469-1809.1936.tb02137.x},
+	eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1469-1809.1936.tb02137.x},
+	abstract = {The articles published by the Annals of Eugenics (1925–1954) have been made available online as an historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice against racial, ethnic and disabled groups. The online publication of this material for scholarly research purposes is not an endorsement of those views nor a promotion of eugenics in any way.},
+	year = {1936}
+}
+@article{lecun2010mnist,
+	title={MNIST handwritten digit database},
+	author={LeCun, Yann and Cortes, Corinna and Burges, CJ},
+	journal={ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist},
+	volume={2},
+	year={2010}
+}
+@InProceedings{eleftheriadis2022equivalence,
+	author="Eleftheriadis, Charis
+		and Kekatos, Nikolaos
+		and Katsaros, Panagiotis
+		and Tripakis, Stavros",
+	editor="Bogomolov, Sergiy
+		and Parker, David",
+	title="On Neural Network Equivalence Checking Using SMT Solvers",
+	booktitle="Formal Modeling and Analysis of Timed Systems",
+	year="2022",
+	publisher="Springer International Publishing",
+	address="Cham",
+	pages="237--257",
+	abstract="Two pretrained neural networks are deemed (approximately) equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with (approximately) equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case when using knowledge distillation, adversarial training, etc. In this paper, we present a method to solve various strict and approximate equivalence checking problems for neural networks, by reducing them to SMT satisfiability checking problems. This work explores the utility and limitations of the neural network equivalence checking framework, and proposes avenues for future research and improvements toward more scalable and practically applicable solutions. We present experimental results, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.",
+	isbn="978-3-031-15839-1"
+}
+
+@article{rosenblatt1958perceptron,
+  added-at = {2017-07-19T15:29:59.000+0200},
+  author = {Rosenblatt, F.},
+  biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez},
+  citeulike-article-id = {13697582},
+  citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519},
+  doi = {10.1037/h0042519},
+  interhash = {dc0cef9dc06033a04f525efdcde7a660},
+  intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9},
+  issn = {0033-295X},
+  journal = {Psychological Review},
+  keywords = {imported},
+  number = 6,
+  pages = {386--408},
+  posted-at = {2016-05-02 20:23:36},
+  priority = {2},
+  timestamp = {2017-07-19T15:31:02.000+0200},
+  title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}},
+  url = {http://dx.doi.org/10.1037/h0042519},
+  volume = 65,
+  year = 1958
+}
+
+@inproceedings{katz2017reluplex,
+	title={Reluplex: An efficient SMT solver for verifying deep neural networks},
+	author={Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J},
+	booktitle={International Conference on Computer Aided Verification},
+	pages={97--117},
+	year={2017},
+	organization={Springer}
+}
+
+@inproceedings{katz2019marabou,
+	title={The Marabou framework for verification and analysis of deep neural networks},
+	author={Katz, Guy and Huang, Derek A and Ibeling, Duligur and Julian, Kyle and Burns, Ryan and Sadigh, Dorsa and Barrett, Clark and Dill, David L and Kochenderfer, Mykel J},
+	booktitle={International Conference on Computer Aided Verification},
+	pages={443--452},
+	year={2019},
+	organization={Springer}
+}
+
+@article{barrett2016smtlib,
+	title={The SMT-LIB standard: Version 2.6},
+	author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare},
+	journal={Department of Computer Science, The University of Iowa, Tech. Rep},
+	year={2016}
+}