Proof: Set Key Example 2

Let's prove the following theorem:

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

Key	Value
name	John
city	New York
country	USA

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.

Proof:

Proof Table

#	Claim	Reason
1	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ]	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ] (Set Key and Value Property 1)
2	output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ]	output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] (Set Key Value List Skip)
3	output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ]	output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] (Set Key Value List Replace)
4	output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ]	output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] (Set Key Value List Skip 2)
5	output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ]	output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] (Set Key Value List Reverse)
6	reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ]	reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] (Reversing a List Property 1)
7	reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ]	reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] (Reversing a List Property 3)
8	reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ]	reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] (Reversing a List Property 3)
9	reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ]	reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ] (Reversing a List Property 4)
10	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ] and output of function store_compute where input key is "city", value is "Denver", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] (Transitive Property of Equality)
11	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] and output of function store_compute where input key is "city", value is "Denver", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed map is [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] (Transitive Property of Equality)
12	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and output of function store_compute where input key is "city", value is "Denver", map is [ entry "country": "USA", [ ] ], and processed map is [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] (Transitive Property of Equality)
13	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and output of function store_compute where input key is "city", value is "Denver", map is [ ], and processed map is [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] (Transitive Property of Equality)
14	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and reverse of [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] (Transitive Property of Equality)
15	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] and reverse of remaining stack [ entry "country": "USA", [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] (Transitive Property of Equality)
16	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] and reverse of remaining stack [ entry "city": "Denver", [ entry "name": "John", [ ] ] ] and already reversed stack [ entry "country": "USA", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] (Transitive Property of Equality)
17	result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ]	if result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] and reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ], then result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments