Ignore:
Timestamp:
Nov 24, 2011, 12:26:30 PM (8 years ago)
Author:
boender
Message:
  • added lookup_opt_lookup lemma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1524 r1553  
    260260qed.
    261261 
     262alias id "bvt_insert" = "cic:/matita/cerco/ASM/BitVectorTrie/insert.fix(0,2,5)".
     263
    262264let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
    263265  (match b with
     
    416418qed.
    417419
     420lemma lookup_opt_lookup:
     421  ∀A,n,b,t1,t2,x.
     422  lookup_opt A n b t1 = lookup_opt A n b t2 → lookup A n b t1 x = lookup A n b t2 x.
     423 #A #n #b #t1 #t2 #x lapply (refl ? (lookup_opt A n b t2))
     424 cases (lookup_opt A n b t2) in ⊢ (???% → %);
     425 [ #H2 #H1 >(lookup_opt_lookup_miss … H1) >(lookup_opt_lookup_miss … H2) //
     426 | #y #H2 #H1 >(lookup_opt_lookup_hit … y H1) >(lookup_opt_lookup_hit … y H2) //
     427 ]
     428qed.
     429   
    418430lemma lookup_opt_prepare_trie_for_insertion_hit:
    419431 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
Note: See TracChangeset for help on using the changeset viewer.