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.

Quiz (1 point)

• index of value v in els = index of value v in els with current index 0
• not (3 = 1)
• 0 + 1 = 1
• not (2 = 1)
• 1 + 1 = 2
• a = a

• if not (el = val), then index of value val in [ el, remain ] with current index idx = index of value val in remain with current index (idx + 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

• if not (el = val), then index of value val in [ el, remain ] with current index idx = index of value val in remain with current index (idx + 1)

• 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

• if el = val, then index of value val in [ el, remain ] with current index idx = idx

• if the following are true:

  • a = b
  • b = c
  • c = d

  then a = d

• if the following are true:

  • a = b
  • b = c
  • c = d

  then a = d

• if the following are true:

  • a = b
  • b = c

  then a = c

Please write your proof in the table below. Each row should contain one claim. The last claim is the statement that you are trying to prove.