Proof: Setting a Key to a Value Example

Let's prove the following theorem:

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.

Proof:

Proof Table

#	Claim	Reason
1	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ]	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ] (Set Key and Value Property 1)
2	output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ]	output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] (Set Key Value List Replace)
3	output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] = reverse of [ entry "name": "Mike", [ ] ]	output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] = reverse of [ entry "name": "Mike", [ ] ] (Set Key Value List Reverse)
4	reverse of [ entry "name": "Mike", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ]	reverse of [ entry "name": "Mike", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] (Reversing a List Property 1)
5	reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] = [ entry "name": "Mike", [ ] ]	reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] = [ entry "name": "Mike", [ ] ] (Reversing a List Property 4)
6	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ]	if result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ] and output of function store_compute where input key is "name", value is "Mike", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ], then result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] (Transitive Property of Equality)
7	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "name": "Mike", [ ] ]	if result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] and output of function store_compute where input key is "name", value is "Mike", map is [ ], and processed map is [ entry "name": "Mike", [ ] ] = reverse of [ entry "name": "Mike", [ ] ], then result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "name": "Mike", [ ] ] (Transitive Property of Equality)
8	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ]	if result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "name": "Mike", [ ] ] and reverse of [ entry "name": "Mike", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ], then result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] (Transitive Property of Equality)
9	result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = [ entry "name": "Mike", [ ] ]	if result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] and reverse of remaining stack [ entry "name": "Mike", [ ] ] and already reversed stack [ ] = [ entry "name": "Mike", [ ] ], then result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = [ entry "name": "Mike", [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments