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:

View as a tree | View dependent proofs | Try proving it

Proof Table
# 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