Ignore:
Timestamp:
Nov 25, 2011, 1:20:41 PM (9 years ago)
Author:
mulligan
Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1535 r1562  
    5959qed.
    6060
     61axiom 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
    6167lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
    6268#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     
    105111qed.
    106112
     113lemma 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
     117qed.
     118
    107119lemma lookup_add_miss : ∀tag,A,m,i,j,a.
    108120  i ≠ j →
     
    111123@lookup_opt_insert_miss /2/
    112124qed.
     125
     126axiom 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.
    113129
    114130lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
Note: See TracChangeset for help on using the changeset viewer.