refinement

8 files changed, 176 insertions, 129 deletions

diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex
index a8c1317..31b61a7 100644
--- a/chapters/core/03-benchmarks.tex
+++ b/chapters/core/03-benchmarks.tex
@@ -3,83 +3,101 @@
 
 This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}.
 
-VEIN was tested with the following hardware:
+\textbf{VEIN} was tested with the following hardware:
 \begin{itemize}
 	\item \textbf{CPU}: AMD Ryzen 7 5700x3D
 	\item \textbf{RAM}: 16GiB
 \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~\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.
+using the 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. For longer runs, only execution is reported. We defined the following benchmarks:
+\begin{itemize}
+	\item \textbf{Iris}: Network trained on the Iris flowers dataset presented by Fisher~\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.
+	\item \textbf{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$.
+	\item \textbf{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$.
+	\item \textbf{MNIST}: Network trained on the 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.
+\end{itemize}
 
 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}.
+In the Iris and MNIST datasets, we tested equivalence between a neural network 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:
+For two neural networks $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}
+	\item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \; F(x) = F'(x)$.
+	\item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \; ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$.
+	\item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \; \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}
 
+We compare the verification time between a direct translation of the ONNX network into a Z3 formula
+and the \textbf{VEIN} framework.
+
 \begin{table}[H]
 	\centering
-	\begin{tabular}[t]{ccccc}
-		\hline
-		Benchmark & Equivalence & Time & Status \\
-		\hline
-		Iris (Stably Active) & Strict & 521.6ms ± 11.5ms & SAT \\
-		Iris (Stably Active) & Epsilon & 515.9ms ± 4.2ms & UNSAT \\
-		Iris (Stably Active) & Argmax & 519.5ms ± 6.0ms & UNSAT \\
-		Iris (Stably Inactive) & Strict & 581.9ms ± 6.2ms & UNSAT \\
-		Iris (Stably Inactive) & Epsilon & 593.8ms ± 6.9ms & UNSAT \\
-		Iris (Stably Inactive) & Argmax & 886.4ms ± 10.3ms & UNSAT \\
-		Iris (To Wide) & Strict & 595.4ms ± 11.3ms & UNSAT \\
-		Iris (To Wide) & Epsilon & 587.0ms ± 4.9ms & UNSAT \\
-		Iris (To Wide) & Argmax & 783.5ms ± 4.4ms & UNSAT \\
-		Iris (To Deep) & Strict & 581.4ms ± 6.6ms & UNSAT \\
-		Iris (To Deep) & Epsilon & 583.1ms ± 5.7ms & UNSAT \\
-		Iris (To Deep) & Argmax & 716.3ms ± 4.7ms & UNSAT \\
-		Pendulum & Strict & 43.276s ± 0.143s & SAT \\
-		Pendulum & Epsilon & 340.293s ± 2.843s & UNSAT \\
-		Pendulum & Argmax & 61.935s ± 0.148s & SAT \\
-		Double Integrator & Strict & 538.952s ± 7.207s & SAT \\
-		Double Integrator & Epsilon & 137.720s ± 0.419s & SAT \\
-		Double Integrator & Argmax & 618.705s ± 6.821s & SAT \\
-		MNIST (Stably Active) & Strict & 18.947s ± 0.034s & SAT \\
-		MNIST (Stably Active) & Epsilon & 18.980s ± 0.032s & UNSAT \\
-		MNIST (Stably Active) & Argmax & 18.906s ± 0.019s & UNSAT \\
-		MNIST (Stably Inactive) & Strict & 14.699s ± 0.024s & UNSAT \\
-		MNIST (Stably Inactive) & Epsilon & 14.702s ± 0.012s & UNSAT \\
-		MNIST (Stably Inactive) & Argmax & TIMEOUT & UNKNOWN \\
-		MNIST (To Wide) & Strict & 20.990s ± 0.181s & UNSAT \\
-		MNIST (To Wide) & Epsilon & 20.860s ± 0.022s & UNSAT \\
-		MNIST (To Wide) & Argmax & TIMEOUT & UNKNOWN \\
-		MNIST (To Deep) & Strict & 20.901s ± 0.027s & UNSAT \\
-		MNIST (To Deep) & Epsilon & 20.947s ± 0.035s & UNSAT \\
-		MNIST (To Deep) & Argmax & TIMEOUT & UNKNOWN \\
-	\end{tabular}
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}[t]{ccccc}
+			\hline
+			Benchmark & Equivalence & Direct & VEIN & Status \\
+			\hline
+			Iris (Stably Active) & Strict & 265.2ms ± 6.8ms & 521.6ms ± 11.5ms & SAT \\
+			Iris (Stably Active) & Epsilon $\epsilon=0.1$ & 271.4ms ± 5.2ms & 515.9ms ± 4.2ms & UNSAT \\
+			Iris (Stably Active) & Argmax & 267.9ms ± 9.5ms & 519.5ms ± 6.0ms & UNSAT \\
+			Iris (Stably Inactive) & Strict & 278.3ms ± 7.7ms & 581.9ms ± 6.2ms & UNSAT \\
+			Iris (Stably Inactive) & Epsilon $\epsilon=0.1$ & 283.2ms ± 9.0ms & 593.8ms ± 6.9ms & UNSAT \\
+			Iris (Stably Inactive) & Argmax & 287.6ms ± 2.6ms & 886.4ms ± 10.3ms & UNSAT \\
+			Iris (Deep To Wide) & Strict & 269.5ms ± 5.1ms & 595.4ms ± 11.3ms & UNSAT \\
+			Iris (Deep To Wide) & Epsilon $\epsilon=0.1$ & 273.7ms ± 5.6ms & 587.0ms ± 4.9ms & UNSAT \\
+			Iris (Deep To Wide) & Argmax & 296.5ms ± 8.5ms & 783.5ms ± 4.4ms & UNSAT \\
+			Iris (Wide To Deep) & Strict & 271.5ms ± 7.7ms & 581.4ms ± 6.6ms & UNSAT \\
+			Iris (Wide To Deep) & Epsilon $\epsilon=0.1$ & 272.3ms ± 6.6ms & 583.1ms ± 5.7ms & UNSAT \\
+			Iris (Wide To Deep) & Argmax & 1.280s ± 0.019s & 716.3ms ± 4.7ms & UNSAT \\
+			Pendulum & Strict & 20m 47.679s & 43.276s ± 0.143s & SAT \\
+			Pendulum & Epsilon $\epsilon=0.1$ & 37m 54.754s & 340.293s ± 2.843s & UNSAT \\
+			Pendulum & Argmax & 24m 56.327s & 61.935s ± 0.148s & SAT \\
+			Double Integrator & Strict & 27m 45.657s & 538.952s ± 7.207s & SAT \\
+			Double Integrator & Epsilon $\epsilon=0.1$ & 59m 51.718s & 137.720s ± 0.419s & SAT \\
+			Double Integrator & Argmax & 41m 21.147s & 618.705s ± 6.821s & SAT \\
+			MNIST (Stably Active) & Strict & 740.5ms ± 4.7ms & 18.947s ± 0.034s & SAT \\
+			MNIST (Stably Active) & Epsilon $\epsilon=0.1$ & 1.571s ± 0.010s & 18.980s ± 0.032s & UNSAT \\
+			MNIST (Stably Active) & Argmax & 794.7ms ± 7.3ms & 18.906s ± 0.019s & UNSAT \\
+			MNIST (Stably Inactive) & Strict & TIMEOUT & 14.699s ± 0.024s & UNSAT \\
+			MNIST (Stably Inactive) & Epsilon $\epsilon=0.1$ & TIMEOUT & 14.702s ± 0.012s & UNSAT \\
+			MNIST (Stably Inactive) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
+			MNIST (Deep To Wide) & Strict & 692.2ms ± 5.6ms & 20.990s ± 0.181s & UNSAT \\
+			MNIST (Deep To Wide) & Epsilon $\epsilon=0.1$ & 691.4ms ± 3.2 ms & 20.860s ± 0.022s & UNSAT \\
+			MNIST (Deep To Wide) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
+			MNIST (Wide To Deep) & Strict & 718.3ms ± 4.8ms & 20.901s ± 0.027s & UNSAT \\
+			MNIST (Wide To Deep) & Epsilon $\epsilon=0.1$ & 722.1ms ± 6.0 ms & 20.947s ± 0.035s & UNSAT \\
+			MNIST (Wide To Deep) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
+		\end{tabular}
+	}
 	\caption{Benchmark table.}
 	\label{tab:benchmarks}
 \end{table}
+
+We make three observations:
+\begin{itemize}
+	\item On Iris, the direct translation is consistently faster by a roughly constant
+		margin, suggesting a fixed \textbf{VEIN} pipeline overhead.
+	\item On Pendulum and Double Integrator, the pattern reverses: \textbf{VEIN} outperforms the direct
+		translation by up to two orders of magnitude.
+	\item MNIST is mixed: most variants favor the direct translation, except Stably Inactive,
+		where the direct encoding times out while \textbf{VEIN} finishes in ~15s. We hypothesize this is because
+		direct encoding may face branching from the unpruned network that \textbf{VEIN} folds during
+		preprocessing.
+\end{itemize}
+Additionally, we identify two false SAT results (Stably Active transformation). These are caused
+by floating-point error introduced by the INPLA float attributes instead of using real numbers.
diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex
index eeebf47..57d3195 100644
--- a/chapters/core/implementation/01-inpla.tex
+++ b/chapters/core/implementation/01-inpla.tex
@@ -1,7 +1,7 @@
 \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 \textbf{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.
@@ -24,7 +24,7 @@ INPLA evaluates nets which consist of connections between terms. Terms are built
 <term> ::= <name> | <agent>
 <name> ::= <nameID>
 <agent> ::= <agentID>
-					| <agentID> ['(' <term> ',' ... ',' <term> ')']
+          | <agentID> ['(' <term> ',' ... ',' <term> ')']
 \end{verbatim}
 \end{small}
 \begin{itemize}
@@ -37,12 +37,12 @@ Interaction rules rewrite connections between agents:
 \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
+Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successor 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:
 \begin{small}
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index 49a8a70..8b02c3c 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -1,7 +1,7 @@
 \subsection{Interaction Rules}
 \label{sec:interaction-rules}
 
-The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups:
+The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into five groups:
 \begin{itemize}
 	\item
 		\textbf{Carriers}: Agents that contain float attributes.
@@ -179,7 +179,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 			(m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm]
 		\end{tabular}
 	}
-	\caption{Agents used in VEIN.}
+	\caption{Agents used in \textbf{VEIN}.}
 	\label{fig:agents}
 \end{figure}
 
@@ -495,7 +495,7 @@ If, instead, the first operand is a \textit{Linear} agents and the second is a \
 are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the
 attribute of the \textit{Concrete} agent to the attribute that represents the constant of the \textit{Linear} agent.
 For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system multiplies the attribute of
-the \textit{Concrete} agent to both the attributes of the \textit{Linear}
+the \textit{Concrete} agent to both the attributes of the \textit{Linear}.
 
 % Concrete >< AddCheckLinear
 \begin{figure}[H]
diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex
index 0a2eec0..b86e060 100644
--- a/chapters/core/implementation/03-translation.tex
+++ b/chapters/core/implementation/03-translation.tex
@@ -9,7 +9,8 @@ necessary copies of a value required by the next operations. Since nodes do not
 nodes will utilize their outputs, the translation layer traverses the DAG in reverse order
 to be able to instantiate the correct number of \textit{Dup} agents. The main algorithm, illustrated
 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.
+name to a list of ports, to keep track of the graph traversal. The ONNX operators supported are Gemm
+(General matrix multiplication) and ReLU.
 
 \begin{algorithm}[H]
 	\caption{Backwards ONNX-to-IN Translation}
@@ -79,9 +80,9 @@ To maximize the concurrency of the INPLA engine, the translation layer avoids ge
 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
+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.
+\textit{Fan-Out} they face the root.
 
 \begin{algorithm}[H]
 	\caption{Balanced Fan-In}
diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex
index a40df41..6023c2e 100644
--- a/chapters/core/implementation/04-python-module.tex
+++ b/chapters/core/implementation/04-python-module.tex
@@ -1,8 +1,8 @@
 \subsection{Python Module}
 \label{sec:python-module}
 
-The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of
-the \texttt{z3.Solver} class offered in the Z3 python
+The core functionality of the \textbf{VEIN} system is implemented via the \texttt{vein.Solver}, an extension of
+the \texttt{z3.Solver} class offered in the Z3 Python
 package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice
 ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API.
 
@@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che
 called.
 
 The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}}
-format. It should contain the input and output symbolic variables declaration, optional range
+format. It should contain the input and output symbolic variables declarations, optional range
 constraints on the input variables and the properties to be verified. For Multi-Network (relational)
 verification, the system ensures that multiple networks share the same input symbolic variables.
 This approach allows Z3 to compare their outputs directly given the same inputs.
diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex
index 800e085..4477581 100644
--- a/chapters/core/soundness-proof/02-soundness-of-translation.tex
+++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex
@@ -20,8 +20,7 @@ Which is identical to the ONNX definition.
 \end{lemma}
 
 \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:
+The ONNX Gemm operator for input tensors A, B, C, input $\alpha$ and $\beta$ and output tensor Y is defined as:
 $$
 Y = \alpha \cdot A \cdot B + \beta \cdot C
 $$
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 26f7e13..6957c3c 100644
--- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
+++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
@@ -1,6 +1,8 @@
 \subsection{Soundness of Interaction Rules}
 \label{sec:soundness-of-interaction-rules}
 
+We need to prove that each interaction rule does not alter the semantics of the IN.
+
 \begin{lemma}
 	For the \textit{Linear} and \textit{Add} agents we have the interaction rule:
 	$$
@@ -146,8 +148,7 @@
 			& \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: }
+		& \text{RHS: } \resizebox{0.85\linewidth}{!}{$
 			\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 \\
@@ -161,7 +162,7 @@
 				\end{aligned}\\
 				\Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise}
 			\end{cases}
-		\end{aligned}
+		$}
 	\end{aligned}
 	$$
 	Since:
@@ -200,8 +201,7 @@
 			& \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: }
+		& \text{RHS: } \resizebox{0.85\linewidth}{!}{$
 			\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}
@@ -213,15 +213,17 @@
 				\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:
 	$$
+	\resizebox{0.95\linewidth}{!}{$
 	\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}
@@ -317,11 +319,13 @@
 \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}
+	\begin{aligned}
+		& \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\
+		& \quad \begin{cases}
+			\mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\
+			\mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise}
+		\end{cases}
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$
@@ -353,12 +357,14 @@
 \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}
+	\begin{aligned}
+		& \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\
+		& \quad \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}
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$
@@ -458,13 +464,13 @@
 	$$
 	\begin{aligned}
 		& \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\
-		& \quad \begin{cases}
+		& \quad \resizebox{0.85\linewidth}{!}{$ \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{cases} $}
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -477,13 +483,16 @@
 		\end{aligned} \\
 		& \begin{aligned}
 			\text{RHS: }
-			\begin{cases}
+			\resizebox{0.9\linewidth}{!}{$ \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}
+				\begin{aligned}
+					& \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \\
+					& \Rightarrow \mathit{out} = q \cdot x + r
+				\end{aligned} & \text{otherwise} \\
+			\end{cases} $}
 		\end{aligned}
 	\end{aligned}
 	$$
@@ -526,9 +535,10 @@
 	For the \textit{Linear} and \textit{Dup} agents we have the interaction rule:
 	$$
 	\begin{aligned}
-		\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
+		& \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{Linear}(z_1, q, r) \sim x; \\
+		& \quad \mathit{Linear}(z_2, q, r) \sim y;	\\
+		& \quad \mathit{Dup}(z_1, z_2) \sim z
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -620,8 +630,11 @@
 	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\\
+		& \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{TermAdd}(a_1, b_1) \sim x; \\
+		& \quad \mathit{TermAdd}(a_2, b_2) \sim y; \\
+		& \quad \mathit{Dup}(a_1, a_2) \sim a; \\
+		& \quad \mathit{Dup}(b_1, b_2) \sim b
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -671,9 +684,11 @@
 	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
+		& \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{TermMul}(a_1, b_1) \sim x; \\
+		& \quad \mathit{TermMul}(a_2, b_2) \sim y; \\
+		& \quad \mathit{Dup}(a_1, a_2) \sim a; \\
+		& \quad \mathit{Dup}(b_1, b_2) \sim b
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -723,10 +738,10 @@
 	For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule:
 	$$
 	\begin{aligned}
-		\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
+		& \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{TermReLU}(z_1) \sim x; \\
+		& \quad \mathit{TermReLU}(z_2) \sim y; \\
+		& \quad \mathit{Dup}(z_1, z_2) \sim z
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -774,9 +789,9 @@
 	For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule:
 	$$
 	\begin{aligned}
-		\mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow
-		& \mathit{TermConcrete}(k) \sim x; \\
-		& \mathit{TermConcrete}(k) \sim y
+		& \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{TermConcrete}(k) \sim x; \\
+		& \quad \mathit{TermConcrete}(k) \sim y
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -822,9 +837,9 @@
 	For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule:
 	$$
 	\begin{aligned}
-		\mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow
-		& \mathit{TermSymbolic}(id) \sim x; \\
-		& \mathit{TermSymbolic}(id) \sim y
+		& \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
+		& \quad \mathit{TermSymbolic}(id) \sim x; \\
+		& \quad \mathit{TermSymbolic}(id) \sim y
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
index d0cec53..15cc4f4 100644
--- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex
+++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
@@ -1,7 +1,7 @@
 \subsection{Soundness of Reduction}
 \label{sec:soundness-of-reduction}
 
-\begin{lemma}
+\begin{property}
 	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
@@ -15,7 +15,7 @@
 			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}
+\end{property}
 
 \begin{theorem}
 	Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be
@@ -65,9 +65,9 @@
 	\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} \\
+		1 + 3^{D-d(a)} & \text{ if }a\text{ is a \textit{Materialize} agent} \\
 		3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\
-		0 & \text{ if }a\text{ is a Carrier, Terminal}
+		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
@@ -88,30 +88,44 @@
 			\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:
+			or temporary Linear agents are wired with \textit{Materialize} agents, which are then forced to
+			interact to produce terminal agents, then wrapped into a new \textit{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})
+			\begin{aligned}
+				\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{aligned}
 			\end{equation}
-			If the carrier $c$ interacts with a Materialize agent $i$:
+			If the carrier $c$ interacts with a \textit{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}
+		\item \textbf{Carrier with Structural Operator}: If a carrier $c$ interacts with a \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:
+			if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermAdd} or \textit{TermMul}, two new agents are created at
+			each auxiliary port:
 			\begin{equation}
 			\Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
 			\end{equation}
+			if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermReLU}, one new agent is created at the 
+			auxiliary port:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
+			\end{equation}
+			if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermConcrete} or \textit{TermSymbolic}, no new agents are
+			created:
+			\begin{equation}
+			\Phi(\text{IN}_n) = 3^{D-d(a)} > 0 = \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
+	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.
+	regardless of the order in which rules are applied.
 \end{proof}