Ignore:
Timestamp:
Nov 23, 2010, 11:43:14 AM (9 years ago)
Author:
mulligan
Message:

Added exponential functions for nats. Working on operational semantics of processor.

File:
1 edited

Legend:

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

    r248 r257  
    77include "BitVector.ma".
    88include "List.ma".
    9    
    10 ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))).
     9
     10ndefinition one ≝ S Z.
     11ndefinition two ≝ (S(S(Z))).
     12ndefinition three ≝ two + one.
     13ndefinition four ≝ two + two.
     14ndefinition five ≝ three + two.
     15ndefinition six ≝ three + three.
     16ndefinition seven ≝ three + four.
     17ndefinition eight ≝ four + four.
     18ndefinition nine ≝ five + four.
     19ndefinition ten ≝ five + five.
     20ndefinition eleven ≝ six + five.
     21ndefinition twelve ≝ six + six.
     22ndefinition thirteen ≝ seven + six.
     23ndefinition fourteen ≝ seven + seven.
     24ndefinition fifteen ≝ eight + seven.
    1125ndefinition sixteen ≝ eight + eight.
     26ndefinition seventeen ≝ nine + eight.
     27ndefinition eighteen ≝ nine + nine.
     28ndefinition nineteen ≝ ten + nine.
    1229ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
    1330ndefinition two_hundred_and_fifty_six ≝
Note: See TracChangeset for help on using the changeset viewer.