using official template + fixing language errorsthesis

3 files changed, 40 insertions, 40 deletions

diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex
index 4477581..83c0f26 100644
--- a/chapters/core/soundness-proof/02-soundness-of-translation.tex
+++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex
@@ -1,7 +1,7 @@
 \subsection{Soundness of Translation}
 \label{sec:soundness-of-translation}
 
-We need to prove that for each ONNX operator a semantically equivalent IN is produced.
+We need to prove that for each ONNX operator, a semantically equivalent IN is produced.
 
 \begin{lemma}
 The ONNX ReLU operator for an input tensor X and output tensor Y is defined as:
@@ -20,7 +20,7 @@ Which is identical to the ONNX definition.
 \end{lemma}
 
 \begin{lemma}
-The ONNX Gemm 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 6957c3c..02005e3 100644
--- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
+++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
@@ -4,7 +4,7 @@
 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:
+	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 \\
 	$$
@@ -26,7 +26,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{Mul} agents we have the interaction rule:
+	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 \\
 	$$
@@ -48,7 +48,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{Add} agents we have the interaction rule:
+	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}
@@ -84,7 +84,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule:
+	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}
@@ -123,7 +123,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule:
+	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 \\
@@ -178,7 +178,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule:
+	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 \\
@@ -229,7 +229,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule:
+	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} \\
 	$$
@@ -251,7 +251,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule:
+	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} \\
 	$$
@@ -273,7 +273,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule:
+	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} \\
 	$$
@@ -295,7 +295,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule:
+	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} \\
 	$$
@@ -317,7 +317,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule:
+	For the \textit{Concrete} and \textit{AddCheckConcrete} agents, we have the interaction rule:
 	$$
 	\begin{aligned}
 		& \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\
@@ -355,7 +355,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule:
+	For the \textit{Concrete} and \textit{MulCheckConcrete} agents, we have the interaction rule:
 	$$
 	\begin{aligned}
 		& \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\
@@ -396,7 +396,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule:
+	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
@@ -424,7 +424,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule:
+	For the \textit{Concrete} and \textit{ReLU} agents, we have the interaction rule:
 	$$
 	\mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow
 	\begin{cases}
@@ -460,7 +460,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule:
+	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 \\
@@ -510,7 +510,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule:
+	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} \\
 	$$
@@ -532,7 +532,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{Dup} agents we have the interaction rule:
+	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 \\
@@ -561,7 +561,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Linear} and \textit{Eraser} agents we have the interaction rule:
+	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 \\
 	$$
@@ -583,7 +583,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{Dup} agents we have the interaction rule:
+	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 \\
 	$$
@@ -606,7 +606,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{Concrete} and \textit{Eraser} agents we have the interaction rule:
+	For the \textit{Concrete} and \textit{Eraser} agents, we have the interaction rule:
 	$$
 	\mathit{Concrete}(k) \bowtie \mathit{Eraser} \Rightarrow  \\
 	$$
@@ -623,11 +623,11 @@ We need to prove that each interaction rule does not alter the semantics of the
 		\end{aligned}
 	\end{aligned}
 	$$
-	Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+	Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound.
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule:
+	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 \\
@@ -658,7 +658,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermAdd} and \textit{Eraser} agents we have the interaction rule:
+	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 \\
 	$$
@@ -681,7 +681,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule:
+	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 \\
@@ -712,7 +712,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermMul} and \textit{Eraser} agents we have the interaction rule:
+	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 \\
 	$$
@@ -735,7 +735,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule:
+	For the \textit{TermReLU} and \textit{Dup} agents, we have the interaction rule:
 	$$
 	\begin{aligned}
 		& \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
@@ -764,7 +764,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermReLU} and \textit{Eraser} agents we have the interaction rule:
+	For the \textit{TermReLU} and \textit{Eraser} agents, we have the interaction rule:
 	$$
 	\mathit{TermReLU}(x) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\
 	$$
@@ -786,7 +786,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule:
+	For the \textit{TermConcrete} and \textit{Dup} agents, we have the interaction rule:
 	$$
 	\begin{aligned}
 		& \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
@@ -813,7 +813,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermConcrete} and \textit{Eraser} agents we have the interaction rule:
+	For the \textit{TermConcrete} and \textit{Eraser} agents, we have the interaction rule:
 	$$
 	\mathit{TermConcrete}(k) \bowtie \mathit{Eraser} \Rightarrow  \\
 	$$
@@ -830,11 +830,11 @@ We need to prove that each interaction rule does not alter the semantics of the
 		\end{aligned}
 	\end{aligned}
 	$$
-	Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+	Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound.
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule:
+	For the \textit{TermSymbolic} and \textit{Dup} agents, we have the interaction rule:
 	$$
 	\begin{aligned}
 		& \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\
@@ -861,7 +861,7 @@ We need to prove that each interaction rule does not alter the semantics of the
 \end{lemma}
 
 \begin{lemma}
-	For the \textit{TermSymbolic} and \textit{Eraser} agents we have the interaction rule:
+	For the \textit{TermSymbolic} and \textit{Eraser} agents, we have the interaction rule:
 	$$
 	\mathit{TermSymbolic}(id) \bowtie \mathit{Eraser} \Rightarrow  \\
 	$$
@@ -878,5 +878,5 @@ We need to prove that each interaction rule does not alter the semantics of the
 		\end{aligned}
 	\end{aligned}
 	$$
-	Since $x_{id} \in \mathbb{R}$ is not violated by RHS, the rule is sound.
+	Since $x_{id} \in \mathbb{R}$ is not violated by the 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 15cc4f4..c373657 100644
--- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex
+++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
@@ -4,8 +4,8 @@
 \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
-			outputs.
+		\item \textbf{Acyclic}: the net forms a forest 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
@@ -29,7 +29,7 @@
 	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:
+	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}
@@ -37,7 +37,7 @@
 	\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:
+	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}
@@ -122,7 +122,7 @@
 			\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
+	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