Proof: Get Key Example

Let's prove the following theorem:

value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = "Alaska"

In this example, we have the following map:

Key Value

OH Ohio

AK Alaska

IA Iowa

We claim that the value for key AK is Alaska. This proof iterates through the entries in the map. The first key is OH, which doesn't match AK, so we pop this entry. The first key in the map is now AK. This matches the key we are looking for, and the value for this key is "Alaska." Thus, we conclude that "AK" maps to "Alaska."

Key	Value
OH	Ohio
AK	Alaska
IA	Iowa

Proof:

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

Proof Table

#	Claim	Reason
1	value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ]	value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] (Get Map Entry Continue Property)
2	value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] = "Alaska"	value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] = "Alaska" (Get Map Entry Property)
3	value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = "Alaska"	if value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] and value at "AK" in map [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] = "Alaska", then value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = "Alaska" (Transitive Property of Equality)

Comments

Please log in to add comments