Changeset 1562 for src/common/Identifiers.ma
- Timestamp:
- Nov 25, 2011, 1:20:41 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Identifiers.ma
r1535 r1562 59 59 qed. 60 60 61 axiom eq_identifier_sym: 62 ∀tag: String. 63 ∀l : identifier tag. 64 ∀r : identifier tag. 65 eq_identifier tag l r = eq_identifier tag r l. 66 61 67 lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false. 62 68 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/ … … 105 111 qed. 106 112 113 lemma lookup_def_add_hit : ∀tag,A,m,i,a,d. 114 lookup_def tag A (add tag A m i a) i d = a. 115 #tag #A * #m * #i #a #d 116 @lookup_insert_hit 117 qed. 118 107 119 lemma lookup_add_miss : ∀tag,A,m,i,j,a. 108 120 i ≠ j → … … 111 123 @lookup_opt_insert_miss /2/ 112 124 qed. 125 126 axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d. 127 i ≠ j → 128 lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d. 113 129 114 130 lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
Note: See TracChangeset
for help on using the changeset viewer.