Proof: Get Key Value Control Map At 13

Let's prove the following theorem:

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

Proof:

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

Given

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

Proof Table

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

Comments

Please log in to add comments