Has Key Example

Proof: Map Has Key Example

Let's prove the following theorem:

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

In this example, we prove that the map [ entry "OH":"Ohio", [ entry "AK":"Alaska", [ entry "IA":"Iowa", [ ] ] ] ] contains key "AK." If there is an entry with key "AK," then the map contains "AK."

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

For instance, the following:

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

is equal to:

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

which is True.

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 "AK" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK" map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "AK" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK"
2 map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK" = True map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK" = True
3 map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "AK" = True if map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "AK" = map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK" and map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] contains key "AK" = True, then map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "AK" = True

Comments

Please log in to add comments