Proof: Map Does Not Have Key Example

Let's prove the following theorem:

map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = False

In this example, we prove that the map [ entry "OH":"Ohio", [ entry "AK":"Alaska", [ entry "IA":"Iowa", [ ] ] ] ] does not have key "TX."

At each step, we observe the first entry in the map. If the key in the first entry is equal to "TX," then we have shown that the map contains key "AK." If not, pop the first entry off of the map and repeat. If the map is empty, then we have shown that "TX" does not exist in the map.

For instance, the following:

map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX"

is equal to:

map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX"

which is equal to:

map [ entry "IA": "Iowa", [ ] ] contains key "TX"

which is equal to:

map [ ] contains key "TX"

which is False.

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table

#	Claim	Reason
1	map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX"	map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" (Map Has Key Continue Property)
2	map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = map [ entry "IA": "Iowa", [ ] ] contains key "TX"	map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = map [ entry "IA": "Iowa", [ ] ] contains key "TX" (Map Has Key Continue Property)
3	map [ entry "IA": "Iowa", [ ] ] contains key "TX" = map [ ] contains key "TX"	map [ entry "IA": "Iowa", [ ] ] contains key "TX" = map [ ] contains key "TX" (Map Has Key Continue Property)
4	map [ ] contains key "TX" = False	map [ ] contains key "TX" = False (Empty Map Has Key Property)
5	map [ entry "IA": "Iowa", [ ] ] contains key "TX" = False	if map [ entry "IA": "Iowa", [ ] ] contains key "TX" = map [ ] contains key "TX" and map [ ] contains key "TX" = False, then map [ entry "IA": "Iowa", [ ] ] contains key "TX" = False (Transitive Property of Equality)
6	map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = False	if map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = map [ entry "IA": "Iowa", [ ] ] contains key "TX" and map [ entry "IA": "Iowa", [ ] ] contains key "TX" = False, then map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = False (Transitive Property of Equality)
7	map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = False	if map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" and map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "TX" = False, then map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = False (Transitive Property of Equality)

Comments

Please log in to add comments