Ignore:
Timestamp:
Dec 1, 2010, 11:27:04 PM (10 years ago)
Author:
sacerdot
Message:
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File:
1 edited

Legend:

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

    r351 r357  
    1 include "Universes.ma".
    2 include "Plogic/equality.ma".
    3 include "Connectives.ma".
    4 include "Nat.ma".
    51include "Exponential.ma".
    6 include "Bool.ma".
    72include "BitVector.ma".
    8 include "List.ma".
    93
    10 ndefinition one ≝ S Z.
    11 ndefinition two ≝ (S(S(Z))).
    12 ndefinition three ≝ two + one.
    13 ndefinition four ≝ two + two.
    14 ndefinition five ≝ three + two.
    15 ndefinition six ≝ three + three.
    16 ndefinition seven ≝ three + four.
    17 ndefinition eight ≝ four + four.
    18 ndefinition nine ≝ five + four.
    19 ndefinition ten ≝ five + five.
    20 ndefinition eleven ≝ six + five.
    21 ndefinition twelve ≝ six + six.
    22 ndefinition thirteen ≝ seven + six.
    23 ndefinition fourteen ≝ seven + seven.
    24 ndefinition fifteen ≝ eight + seven.
    25 ndefinition sixteen ≝ eight + eight.
    26 ndefinition seventeen ≝ nine + eight.
    27 ndefinition eighteen ≝ nine + nine.
    28 ndefinition nineteen ≝ ten + nine.
    29 ndefinition twenty_four ≝ sixteen + eight.
    30 ndefinition thirty_two ≝ sixteen + sixteen.
    31 ndefinition one_hundred ≝ ten * ten.
    32 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
    33 ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
    34 ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
    35 ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
    36 ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
    37 ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
    38 ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
    39 ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
    40 ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
    41 ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
    42 ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
    43 ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
    44 ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
    45 ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
    46 ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
    47 ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
    48 ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
    49 ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
    50 ndefinition two_hundred ≝ one_hundred + one_hundred.
    51 ndefinition two_hundred_and_two ≝ two_hundred + two.
    52 ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
    53 ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
    54 ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
    55 ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
    56 ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
    57 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    58 ndefinition two_hundred_and_fifty_six ≝
    59   one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
    60    
    614ndefinition nat_of_bool ≝
    625  λb: Bool.
Note: See TracChangeset for help on using the changeset viewer.