add proof for exercises 2.1-3

C02-Getting-Started/2.1.md

@@ -1,48 +1,49 @@
-### Exercises 2.1-1
-***
-Using Figure 2.2 as a model, illustrate the operation of INSERTION-SORT on the array A = [31, 41, 59, 26, 41, 58].
-
-### `Answer`
-![pic](./repo/s1/1.png)
-
-
-### Exercises 2.1-2
-***
-Rewrite the INSERTION-SORT procedure to sort into nonincreasing instead of nondecreasing order.
-
-### `Answer`
-![pic](./repo/s1/2.png)
-
-
-### Exercises 2.1-3
-***
-Consider the searching problem:
-
-* **Input**: A sequence of n numbers A = [a1, a2, . . . , an] and a value v.
-* **Output**: An index i such that v = A[i] or the special value NIL if v does not appear in A.
-
-
-Write pseudocode for **linear search**, which scans through the sequence, looking for v. Using a loop invariant, prove that your algorithm is correct. Make sure that your loop invariant fulfills the three necessary properties.
-
-### `Answer`
-![pic](./repo/s1/3.png)
-
-### Exercises 2.1-4
-***
-Consider the problem of adding two n-bit binary integers, stored in two n-element arrays A and B. The sum of the two integers should be stored in binary form in an (n + 1)-element array C. State the problem formally and write pseudocode for adding the two integers.
-
-### `Answer`
-![pic](./repo/s1/algorithm.png)
-
-```
-C = Array[A.length+1]
-carry <- 0,
-for i <- A.length to 1
-    C[i+1] <- (A[i] + B[i] + carry) % 2;
-    carry = (A[i] + B[i] + carry)/2;
-C[1] <- carry;
-return C
-```
-
-***
-Follow [@louis1992](https://github.com/gzc) on github to help finish this task.
+### Exercises 2.1-1
+***
+Using Figure 2.2 as a model, illustrate the operation of INSERTION-SORT on the array A = [31, 41, 59, 26, 41, 58].
+
+### `Answer`
+![pic](./repo/s1/1.png)
+
+
+### Exercises 2.1-2
+***
+Rewrite the INSERTION-SORT procedure to sort into nonincreasing instead of nondecreasing order.
+
+### `Answer`
+![pic](./repo/s1/2.png)
+
+
+### Exercises 2.1-3
+***
+Consider the searching problem:
+* **Input**: A sequence of n numbers A = [a1, a2, . . . , an] and a value v.* **Output**: An index i such that v = A[i] or the special value NIL if v does not appear in A.
+Write pseudocode for **linear search**, which scans through the sequence, looking for v. Using a loop invariant, prove that your algorithm is correct. Make sure that your loop invariant fulfills the three necessary properties.
+
+### `Answer`
+![pic](./repo/s1/3.png)
+
+Loop Invariant: all elements in subarray  A[1:j-1] (all elements before index j) do not equal to v.
+
+Proof:
+
+* **Initialization**: j = 1 when the loop begins and subarray A[1:j-1] is empty (note that the index starts from 1 not 0). Thus, it is a vacuous truth.
+* **Maintainance**:  The body of **for** loop works by checking A[j], A[j+1], A[j+2], and so on by one position to the right until the value equals to v is finded, at which point the loop would end by returning the value. The subarray of A[1:j-1] consists of values that has already been investigated, since the loop hasn't turned to terminate. We know the loop invariant is maintained.
+* **Termination**: There are two cases which lead to termination:
+   1. The value equals to v has been found (line 3): The value equals to v is found at index j, and it must be the first time value equals to v is founded or the loop would terminate ealier. Thus, all elements investiagted before (A[1:j-1]) do not contain v. The loop invariant holds. 
+
+   2. The value has not been found after investigating every element in the sequence (line 4): Since every element is checked and v is not found, the loop invariant must be true.
+
+
+### Exercises 2.1-4
+***
+Consider the problem of adding two n-bit binary integers, stored in two n-element arrays A and B. The sum of the two integers should be stored in binary form in an (n + 1)-element array C. State the problem formally and write pseudocode for adding the two integers.
+
+### `Answer`
+![pic](./repo/s1/4.png)
+
+
+
+***
+Follow [@louis1992](https://github.com/gzc) on github to help finish this task.
+