Changeset 1521 for src/ASM/BitVectorTrie.ma
 Timestamp:
 Nov 21, 2011, 1:06:01 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1516 r1521 354 354 #t cases(BitVectorTrie_Sn … t) 355 355 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 356 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???)))] normalize // @IH //356 [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH // 357 357  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 358 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???)))] normalize358 [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize 359 359 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 360 360 qed. … … 458 458 #t cases(BitVectorTrie_Sn … t) 459 459 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 460 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???)))] normalize // @IH //460 [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH // 461 461  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 462 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???)))] normalize462 [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize 463 463 [3,4: cases tl' //  *: @lookup_opt_prepare_trie_for_insertion_miss //]]] 464 464 qed.
Note: See TracChangeset
for help on using the changeset viewer.