Changeset 1516 for src/ASM/BitVectorZ.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorZ.ma

    r891 r1516  
    5858#n #bv elim bv
    5959[ //
    60 | #m * #t #IH whd in ⊢ (??%) //
     60| #m * #t #IH whd in ⊢ (??%); //
    6161] qed.
    6262
     
    109109| #tl #_ normalize @le_S_S
    110110  change with (? ≤ pos_length one + m)
    111   generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl
     111  generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl
    112112  [ // | #o * #t normalize #IH #p <plus_n_Sm
    113113    change with (? ≤ pos_length (p1 p) + o)
     
    145145theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n.
    146146#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))
    148148  cases (Z_of_unsigned_bitvector n (negation_bv n t)) //
    149149  #p *
    150 | #t whd in ⊢ (?%?) //
     150| #t whd in ⊢ (?%?); //
    151151] qed.
Note: See TracChangeset for help on using the changeset viewer.