[+] A4 P2.3.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