Proof: Get Key Value Control Map At 12

Let's prove the following theorem:

if Control Map at time 12 = [ entry 0: (pair ("if", False)), [ ] ], then value at 0 in map (Control Map at time 12) = pair ("if", False)

Proof:

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

Given

1	Control Map at time 12 = [ entry 0: (pair ("if", False)), [ ] ]

Proof Table

#	Claim	Reason
1	value at 0 in map (Control Map at time 12) = value at 0 in map [ entry 0: (pair ("if", False)), [ ] ]	if Control Map at time 12 = [ entry 0: (pair ("if", False)), [ ] ], then value at 0 in map (Control Map at time 12) = value at 0 in map [ entry 0: (pair ("if", False)), [ ] ] (Substitution)
2	value at 0 in map [ entry 0: (pair ("if", False)), [ ] ] = pair ("if", False)	value at 0 in map [ entry 0: (pair ("if", False)), [ ] ] = pair ("if", False) (Get Map Entry Property)
3	value at 0 in map (Control Map at time 12) = pair ("if", False)	if value at 0 in map (Control Map at time 12) = value at 0 in map [ entry 0: (pair ("if", False)), [ ] ] and value at 0 in map [ entry 0: (pair ("if", False)), [ ] ] = pair ("if", False), then value at 0 in map (Control Map at time 12) = pair ("if", False) (Transitive Property of Equality)

Comments

Please log in to add comments