 Timestamp:
 Nov 24, 2011, 12:26:30 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1524 r1553 260 260 qed. 261 261 262 alias id "bvt_insert" = "cic:/matita/cerco/ASM/BitVectorTrie/insert.fix(0,2,5)". 263 262 264 let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ 263 265 (match b with … … 416 418 qed. 417 419 420 lemma 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 ] 428 qed. 429 418 430 lemma lookup_opt_prepare_trie_for_insertion_hit: 419 431 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
Note: See TracChangeset
for help on using the changeset viewer.