In this example, we have a map that has 3 entries:

And we want to update the key "city" with a new value "Denver"

The map is then updated to:

Key	Value
name	John
city	Denver
country	USA

Step 1 sets "processed" to an empty map and "key found" to false.

Step 2 looks at the first "remaining" entry. Since the first key "name" does not match the key "city," we can just move "name": "John" to the "processed" map.

Step 3 again looks at the first "remaining" entry, which is now "city." This matches the key we are trying to update, so the value "New York" is replaced withe new value "Denver" and prepended to the "processed" map. Also, "key found" is now set to true.

In step 4, since we found the key, we just move "country":"USA" to the "processed" map.

In step 5, "remaining" is now empty. Thus the "processed" map now has all up-to-date entries, and we just need to reverse the entries.

Steps 6 - 9 performs the reverse operation, and from there, we use the Transitive Property of Equality a few times to arrive at the our claim.

Quiz (1 point)

• result of storing value at key: key in map: entries = output of function store_compute where input key is key, value is value, map is entries, and processed map is [ ]
• output of function store_compute where input key is key, value is value, map is [ entry lkey: lvalue, remaining ], and processed map is kvs = output of function store_compute where input key is key, value is value, map is remaining, and processed map is [ entry lkey: lvalue, kvs ]
• output of function store_compute where input key is key, value is value, map is [ entry key: old_value, remaining ], and processed map is kvs = output of function store_compute where input key is key, value is value, map is remaining, and processed map is [ entry key: value, kvs ]
• output of function store_compute where input key is key, value is value, map is [ entry lkey: lvalue, remaining ], and processed map is kvs = output of function store_compute where input key is key, value is value, map is remaining, and processed map is [ entry lkey: lvalue, kvs ]
• output of function store_compute where input key is key, value is value, map is [ ], and processed map is kvs = reverse of kvs
• reverse of xs = reverse of remaining stack xs and already reversed stack [ ]
• reverse of remaining stack [ x, xs ] and already reversed stack ys = reverse of remaining stack xs and already reversed stack [ x, ys ]
• reverse of remaining stack [ x, xs ] and already reversed stack ys = reverse of remaining stack xs and already reversed stack [ x, ys ]
• reverse of remaining stack [ x, [ ] ] and already reversed stack ys = [ x, ys ]

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• if the following are true:

  • a = b
  • b = c

  then a = c

• 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.