Proof: Find Value Example
Let's prove the following theorem:
index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = 2
In this example, we prove that the list
[3, [2, [1, []]]]
Contains 1 at index 2.
We track the "current index" which is initially 0. Starting with the first element, if the element is not the value we are looking for, then we move on to the next element by popping the list and incrementing the current index by 1.
After a few iterations, the list becomes
[1, []]
and the current index is 2. At this point, the first element is the value we are looking for, so we stop.
Proof:
# | Claim | Reason |
---|---|---|
1 | index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 | index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 |
2 | not (3 = 1) | not (3 = 1) |
3 | index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) | if not (3 = 1), then index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) |
4 | 0 + 1 = 1 | 0 + 1 = 1 |
5 | index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) = index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 | if 0 + 1 = 1, then index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) = index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 |
6 | not (2 = 1) | not (2 = 1) |
7 | index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = index of value 1 in [ 1, [ ] ] with current index (1 + 1) | if not (2 = 1), then index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = index of value 1 in [ 1, [ ] ] with current index (1 + 1) |
8 | 1 + 1 = 2 | 1 + 1 = 2 |
9 | index of value 1 in [ 1, [ ] ] with current index (1 + 1) = index of value 1 in [ 1, [ ] ] with current index 2 | if 1 + 1 = 2, then index of value 1 in [ 1, [ ] ] with current index (1 + 1) = index of value 1 in [ 1, [ ] ] with current index 2 |
10 | 1 = 1 | 1 = 1 |
11 | index of value 1 in [ 1, [ ] ] with current index 2 = 2 | if 1 = 1, then index of value 1 in [ 1, [ ] ] with current index 2 = 2 |
12 | index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = 2 | if index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = index of value 1 in [ 1, [ ] ] with current index (1 + 1) and index of value 1 in [ 1, [ ] ] with current index (1 + 1) = index of value 1 in [ 1, [ ] ] with current index 2 and index of value 1 in [ 1, [ ] ] with current index 2 = 2, then index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = 2 |
13 | index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = 2 | if index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) and index of value 1 in [ 2, [ 1, [ ] ] ] with current index (0 + 1) = index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 and index of value 1 in [ 2, [ 1, [ ] ] ] with current index 1 = 2, then index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = 2 |
14 | index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = 2 | if index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 and index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] with current index 0 = 2, then index of value 1 in [ 3, [ 2, [ 1, [ ] ] ] ] = 2 |
Comments
Please log in to add comments