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/Nat.ma

    r352 r357  
    44include "Cartesian.ma".
    55include "Bool.ma".
    6 
    76include "Connectives.ma".
    87
     
    655654 #m n; napply less_than_b_elim.
    656655nqed.
     656
     657(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     658(* Numbers.                                                                   *)
     659(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     660
     661ndefinition one ≝ S Z.
     662ndefinition two ≝ (S(S(Z))).
     663ndefinition three ≝ two + one.
     664ndefinition four ≝ two + two.
     665ndefinition five ≝ three + two.
     666ndefinition six ≝ three + three.
     667ndefinition seven ≝ three + four.
     668ndefinition eight ≝ four + four.
     669ndefinition nine ≝ five + four.
     670ndefinition ten ≝ five + five.
     671ndefinition eleven ≝ six + five.
     672ndefinition twelve ≝ six + six.
     673ndefinition thirteen ≝ seven + six.
     674ndefinition fourteen ≝ seven + seven.
     675ndefinition fifteen ≝ eight + seven.
     676ndefinition sixteen ≝ eight + eight.
     677ndefinition seventeen ≝ nine + eight.
     678ndefinition eighteen ≝ nine + nine.
     679ndefinition nineteen ≝ ten + nine.
     680ndefinition twenty_four ≝ sixteen + eight.
     681ndefinition thirty_two ≝ sixteen + sixteen.
     682ndefinition one_hundred ≝ ten * ten.
     683ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
     684ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
     685ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
     686ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
     687ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
     688ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
     689ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
     690ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
     691ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
     692ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
     693ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
     694ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
     695ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
     696ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
     697ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
     698ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
     699ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
     700ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
     701ndefinition two_hundred ≝ one_hundred + one_hundred.
     702ndefinition two_hundred_and_two ≝ two_hundred + two.
     703ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
     704ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
     705ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
     706ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
     707ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
     708ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
     709ndefinition two_hundred_and_fifty_six ≝
     710  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
Note: See TracChangeset for help on using the changeset viewer.