Proof: Add Key Example

Let's prove the following theorem:

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

"name":"John"

And we want to store a new key "city" with value "New York".

The map is then updated to:

[ entry "name":"Mike", [ entry "city":"New York", [ ] ] ]

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

In step 2, we skip the key "name" since we are looking to replace the key "city".

In step 3, we have reached the end of the map and the key "city" has not yet been found, so we add the new "city":"New York" entry to the map. After that, we just reverse the new map and then use the Transitive Property of Equality to set the result to the new map.

Proof:

Proof Table

#	Claim	Reason
1	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", map is [ entry "name": "John", [ ] ], and processed map is [ ]	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", 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 "city", value is "New York", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ]	output of function store_compute where input key is "city", value is "New York", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "New York", map is [ ], 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 "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Set Key and Value Add Property)
4	reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ]	reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] (Reversing a List Property 1)
5	reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ]	reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] (Reversing a List Property 3)
6	reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ]	reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ] (Reversing a List Property 4)
7	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ]	if result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", map is [ entry "name": "John", [ ] ], and processed map is [ ] and output of function store_compute where input key is "city", value is "New York", map is [ entry "name": "John", [ ] ], and processed map is [ ] = output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ], then result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ] (Transitive Property of Equality)
8	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	if result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ] and output of function store_compute where input key is "city", value is "New York", map is [ ], and processed map is [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ], then result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Transitive Property of Equality)
9	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ]	if result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ], then result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] (Transitive Property of Equality)
10	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ]	if result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] and reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ], then result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] (Transitive Property of Equality)
11	result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ]	if result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] and reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ], then result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments