Proof: Delete Key Example

Let's prove the following theorem:

In this example, we have the following map:

Key	Value
name	John
city	New York
country	USA

We prove that, when the key "country" and its value is deleted, the map will change to:

Key	Value
name	John
city	New York

This proof iterates through the entries in the map. The first key is "name", which doesn't match "country," so we just move it to processed. The first key in the map is now "city," which does not match the key we are looking for, so we just move the entry to "processed." The first (and last) key in the map is now "country." This matches the key we are looking for. Thus, we pop this from the map but we don't paste it into "processed." Now "processed" has all the entries except the entry with the key "country." From there, we just need to reverse "processed."

Proof:

Proof Table

#	Claim	Reason
1	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ]	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ] (Delete Key Property)
2	output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ]	output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] (Delete Entry Key Property 3)
3	output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Delete Entry Key Property 3)
4	output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Delete Entry Key Property 2)
5	output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Delete Key Property 4)
6	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)
7	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)
8	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)
9	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ] and output of function delete_entry where input key is "country", map is [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ], and processed is [ ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ], then result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] (Transitive Property of Equality)
10	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] and output of function delete_entry where input key is "country", map is [ entry "city": "New York", [ entry "country": "USA", [ ] ] ], and processed is [ entry "name": "John", [ ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ], then result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Transitive Property of Equality)
11	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and output of function delete_entry where input key is "country", map is [ entry "country": "USA", [ ] ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ], then result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Transitive Property of Equality)
12	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and output of function delete_entry where input key is "country", map is [ ], and processed is [ entry "city": "New York", [ entry "name": "John", [ ] ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ], then result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of [ entry "city": "New York", [ entry "name": "John", [ ] ] ] (Transitive Property of Equality)
13	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = 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 deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "city": "New York", [ entry "name": "John", [ ] ] ] and already reversed stack [ ] (Transitive Property of Equality)
14	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = 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 deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = reverse of remaining stack [ entry "name": "John", [ ] ] and already reversed stack [ entry "city": "New York", [ ] ] (Transitive Property of Equality)
15	result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ]	if result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = 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 deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments