Ignore:
Timestamp:
Dec 1, 2010, 4:30:46 PM (9 years ago)
Author:
mulligan
Message:

No more axioms but the paralogisms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r349 r351  
    200200  let bitvector ≝ bitvector_of_list biglist in
    201201  let difference ≝ n - size in
    202     match greater_than_b size n with
    203       [ true ⇒ max n
    204       | false ⇒ ? (pad difference size bitvector)
    205       ].
    206       nnormalize.
    207       nrewrite > (plus_minus_inverse_right n ?).
    208       #H.
    209       nassumption.
     202   less_than_or_equal_b_elim …
     203    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉))
     204    (λH:¬(size ≤ n). max n).
     205 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
    210206nqed.
    211207
Note: See TracChangeset for help on using the changeset viewer.