From ef1733c5682562eae0bc3271a0de8ff3b84fd626 Mon Sep 17 00:00:00 2001 From: Hykilpikonna Date: Tue, 9 Nov 2021 14:14:40 -0500 Subject: [PATCH] [O] A4 Change N_1 to M --- assignments/a4/a4.tex | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/assignments/a4/a4.tex b/assignments/a4/a4.tex index b9e0351..5b15a5b 100644 --- a/assignments/a4/a4.tex +++ b/assignments/a4/a4.tex @@ -143,30 +143,29 @@ Variables: In this proof, $N$ is the abbreviation for the list \texttt{nums\_so\ 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] $ +Let $M = N \cup \{ N[-2] + 6 \}$ be the list of the current iteration. \\ +We need to prove: $\forall i \in \{0, \dots, |M| - 3\}, M[i] + 6 = M[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[1.] Let $i < |M| - 3$ \\ + Since the new entry added to $M$ 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]$ \\ + \item[2.] Let $i = |M| - 3$ \\ + We need to prove: $M[|M| - 3] + 6 = M[|M| - 3 + 2]$ \\ + That is $M[-3] + 6 = M[-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]$ \\ + Since $M[:-1] = (N \cup \{ N[-2] + 6 \})[:-1] = N$, \\ + $M[:-1][|N| - 2] = M[|N| - 2] = N[-2]$ \\ + Since $M$ has one extra entry than $N$, $|M| = |N| + 1$ \\ + $M[|N| - 2] = M[|N| + 1 - 3] = M[|M| - 3] = M[-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]$ \\ + $M[-3] + 6 = N[-2] + 6$ \\ + Since $M[-1] = (N \cup \{ N[-2] + 6 \})[-1] = N[-2] + 6$ is it's last entry, \\ + $M[-3] + 6 = M[-1]$ \\ Which is what we want to show. - \end{enumerate} \end{proof}