Corrections mot prove

sections/correctness.tex

@@ -141,7 +141,7 @@ In particular this also means that:
 This proof can be done by induction on the length of the execution path of the program $P$.
 Let's consider $\Gamma |- P$ and a state $\sigma |- \Gamma$.
 \begin{itemize}
-\item Let's proove that if $(P, \sigma) \rightarrow^0 \sigma' or (P, \sigma) \rightarrow^0 (S, \sigma')$ then $\sigma' |- \Gamma$.
+\item Let's prove that if $(P, \sigma) \rightarrow^0 \sigma' or (P, \sigma) \rightarrow^0 (S, \sigma')$ then $\sigma' |- \Gamma$.
 Because $\sigma = (S, \sigma')$ is impossible, we are in the case where $\sigma = \sigma'$.
 By hypothesis, $\sigma |- \Gamma$, so $\sigma' |- \Gamma$.
 
@@ -154,7 +154,7 @@ There is no transition from a terminal state, so this is trivially true.
 \item $s = (S, \sigma'')$
 By induciton we know that $\sigma'' |- \Gamma$.
 
-We can proove by induction on the structure of $S$ that
+We can prove by induction on the structure of $S$ that
 $(S, \sigma'') \rightarrow \sigma' => \sigma' |- \Gamma$ and
 $(S, \sigma'') \rightarrow (S', \sigma') => \sigma' |- \Gamma$.