azalea/CSC110
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[O] A4 Change N_1 to M

Browse Source
This commit is contained in:
Hykilpikonna
2021-11-09 14:14:40 -05:00
parent 023c0028dc
commit ef1733c568
1 changed files with 14 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files
assignments/a4/a4.tex
+14 -15
View File
@@ -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}