Changeset 357 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Dec 1, 2010, 11:27:04 PM (11 years ago)
 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".5 1 include "Exponential.ma". 6 include "Bool.ma".7 2 include "BitVector.ma". 8 include "List.ma".9 3 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 61 4 ndefinition nat_of_bool ≝ 62 5 λb: Bool.
Note: See TracChangeset
for help on using the changeset viewer.