diff --git a/assignments/a4/a4.tex b/assignments/a4/a4.tex index ad706cc..b9e0351 100644 --- a/assignments/a4/a4.tex +++ b/assignments/a4/a4.tex @@ -137,8 +137,37 @@ By assumption 1, we know that $gcd(N[-2], 2) = 1$ and $gcd(N[-2], 3) = 1$ \end{proof} \item[b.] Loop Invariant 2 -\begin{proof} -TODO: Your proof goes here. +\begin{proof} : \\ +Variables: In this proof, $N$ is the abbreviation for the list \texttt{nums\_so\_far}, and $|N|$ represents the size of $N$. \\ +\\ +Assumption 1: The loop invariant 2 is true for the previous iteration. \\ +That is $\forall i_2 \in \{ 0, \dots, |N| - 3\}, N[i_2] + 6 = N[i_2 + 2]$ \\ +\\ +Let $N_1 = N \cup \{ N[-2] + 6 \}$ be the list of the current iteration. \\ +We need to prove: $\forall i \in \{0, \dots, |N_1| - 3\}, N_1[i] + 6 = N_1[i + 2] $ + +\begin{enumerate} + \item[1.] Let $i < |N_1| - 3$ \\ + Since the new entry added to $N_1$ is not included in $i$, this case is equivalent to the previous iteration, and we know that is true by assumption 1. + + \item[2.] Let $i = |N_1| - 3$ \\ + We need to prove: $N_1[|N_1| - 3] + 6 = N_1[|N_1| - 3 + 2]$ \\ + That is $N_1[-3] + 6 = N_1[-1]$ \\ + \\ + Let's start with a true statement: \\ + $N[-2] = N[-2]$ \\ + Since $N_1[:-1] = (N \cup \{ N[-2] + 6 \})[:-1] = N$, \\ + $N_1[:-1][|N| - 2] = N_1[|N| - 2] = N[-2]$ \\ + Since $N_1$ has one extra entry than $N$, $|N_1| = |N| + 1$ \\ + $N_1[|N| - 2] = N_1[|N| + 1 - 3] = N_1[|N_1| - 3] = N_1[-3] = N[-2]$ \\ + Add 6 to both sides: \\ + $N_1[-3] + 6 = N[-2] + 6$ \\ + Since $N_1[-1] = (N \cup \{ N[-2] + 6 \})[-1] = N[-2] + 6$ is it's last entry, \\ + $N_1[-3] + 6 = N_1[-1]$ \\ + Which is what we want to show. + + +\end{enumerate} \end{proof} \item[c.] Loop Invariant 3