Changeset 1919 for src/ASM/ASMCostsSplit.ma
 Timestamp:
 May 7, 2012, 11:12:13 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1899 r1919 41 41 λ${ident E}.$s ] ] (refl ? $t) }. 42 42 43 lemma succ_nat_of_bitvector_aux_half_add_1: 44 ∀n: nat. 45 ∀bv: BitVector n. 46 ∀buffer: nat. 47 ∀power_proof: nat_of_bitvector … bv < 2^n  1. 48 S (nat_of_bitvector_aux n buffer bv) = 49 nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)). 50 #n #bv elim bv 51 [1: 52 #buffer normalize #absurd 53 cases (lt_to_not_zero … absurd) 54 2: 55 #n' #hd #tl #inductive_hypothesis #buffer 56 cases daemon 57 ] 58 qed. 59 60 lemma succ_nat_of_bitvector_half_add_1: 61 ∀n: nat. 62 ∀bv: BitVector n. 63 ∀power_proof: nat_of_bitvector … bv < 2^n  1. 64 S (nat_of_bitvector … bv) = nat_of_bitvector … 65 (\snd (half_add n (bitvector_of_nat … 1) bv)). 66 #n #bv elim bv 67 [1: 68 normalize #absurd 69 cases (lt_to_not_zero … absurd) 70 2: 71 #n' #hd #tl #inductive_hypothesis 72 cases daemon 73 ] 74 qed. 75 43 76 let rec traverse_code_internal 44 77 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
Note: See TracChangeset
for help on using the changeset viewer.