- Timestamp:
- Feb 16, 2013, 6:49:13 PM (7 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r2664 r2672 166 166 @execute_1_and_program_counter_after_other_in_lockstep0 assumption. 167 167 qed. 168 169 lemma nat_of_bitvector_lt_bound:170 ∀n: nat.171 ∀b: BitVector n.172 nat_of_bitvector n b < 2^n.173 #n #b cases daemon174 qed.175 168 176 169 lemma sublist_tal_pc_list_all_program_counter_list: -
src/ASM/Arithmetic.ma
r2311 r2672 161 161 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ 162 162 λn,v. nat_of_bitvector_aux n O v. 163 164 lemma nat_of_bitvector_aux_lt_bound: 165 ∀n.∀v:BitVector n. ∀m,l:nat. 166 m < 2^l → nat_of_bitvector_aux n m v < 2^(n+l). 167 #n #v elim v normalize // -n 168 #n #hd #tl #IH #m #l #B cases hd normalize nodelta 169 @(transitive_le … (IH ? (S l) …)) 170 [2,4: /2 by le_exp/ 171 |1,3: @(transitive_le … (2 * (S m))) 172 [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/ 173 |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]] 174 qed. 175 176 lemma nat_of_bitvector_lt_bound: 177 ∀n: nat. ∀b: BitVector n. nat_of_bitvector n b < 2^n. 178 #n #b lapply (nat_of_bitvector_aux_lt_bound n b 0 0 ?) // <plus_n_O // 179 qed. 163 180 164 181 lemma bitvector_of_nat_ok:
Note: See TracChangeset
for help on using the changeset viewer.