Changeset 1516 for src/ASM/BitVectorZ.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorZ.ma
r891 r1516 58 58 #n #bv elim bv 59 59 [ // 60  #m * #t #IH whd in ⊢ (??%) //60  #m * #t #IH whd in ⊢ (??%); // 61 61 ] qed. 62 62 … … 109 109  #tl #_ normalize @le_S_S 110 110 change with (? ≤ pos_length one + m) 111 generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl111 generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl 112 112 [ //  #o * #t normalize #IH #p <plus_n_Sm 113 113 change with (? ≤ pos_length (p1 p) + o) … … 145 145 theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n. 146 146 #n #bv @(vector_inv_n ? (S n) ? bv) * 147 [ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))147 [ #t whd in ⊢ (?%%); lapply (bv_Z_unsigned_min … (negation_bv n t)) 148 148 cases (Z_of_unsigned_bitvector n (negation_bv n t)) // 149 149 #p * 150  #t whd in ⊢ (?%?) //150  #t whd in ⊢ (?%?); // 151 151 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.