In this example, we have a map that has 1 entry:

entry "name":"John"

And we want to store a new value "Mike" for the key "name"

We want to prove that, after the update, the new map will be:

[entry "name":"Mike", [ ] ]

Step 1 uses Set Key and Value Property 1 which sets the "processed" to an empty map and "key found" to false.

Step 2 says we can add entry "name": Mike to the "processed" map.

In step 3, we have the final "processed" map and we just need to reverse the entries, but there is only 1 entry in this map, so the reverse of "processed" is the same as "processed."

The rest of the proof uses the transitive property to set the original expression equal to the new map.

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 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 [ ], 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, [ ] ] 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

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.

Step	Claim	Reason (optional)	Error Message (if any)
1
2
3
4
5
6
7
8
9
10

Add Step Reset

Become a subscriber to save your progress, see the correct answer, and more!