From 837bed57525005f8a534266a11d9b5dbb0b80600 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Tue, 11 Jun 2024 18:32:54 +0200
Subject: [PATCH] Soundness

---
 aspUnify.tex | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/aspUnify.tex b/aspUnify.tex
index 29854e1..3e19a70 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -257,10 +257,19 @@ constraints in the original constraint set and
 there exists a typing for the remaining type placeholders 
 so that the constraint set is satisfied.
 
+\begin{lemma} \label{lemma:subtypeOnly}
+If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the right side of $\tv{a} \lessdot \type{T}$ constraints.
+\end{lemma}
+\begin{lemma} \label{lemma:reduceToSigma}
+If algorithm is successfull and $\type{T} \lessdot \tv{a}$ or $\tv{a} \doteq \type{T}$ or $\type{T} \doteq \tv{a}$ then $\sigma(\tv{a}) \neq \emptyset$
+\end{lemma}
 Proof:
 Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
+Then either the Solution-Sub generates a $\sigma'$ or the Solution rule can be used due to lemma \ref{lemma:reduceToSigma}.
 Or algorithm terminates with $\emptyset$.
 
+The Solution-Sub rule is always correct.
+
 Proof:
 \SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
 \newcommand*\ncasesmakelabel[1]{Case #1}
@@ -272,7 +281,6 @@ Proof:
   {\endproof}
 
 \begin{proof}
-  Some text or \texttt{\string\leavevmode} (so the enumerate starts in another line)
   \begin{enumerate}[ncases]
     \item $\tv{a} \lessdot \type{N}$.
     \begin{subproof}