Changes between Version 2 and Version 3 of TypeNats/Axioms


Ignore:
Timestamp:
Nov 27, 2010 9:09:00 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Axioms

    v2 v3  
    55The actual algorithm for constructing the evidence is described as set of rules (interactions) which are described separately.
    66
     7The "*Def" axioms bellow look a bit odd but all they are saying is that the predicates which are being defined behave like their corresponding mathematical operations.
    78
    89
    910Notation:
    1011{{{
    11 m,n:    literals of kind Nat
     12k,m,n:  literals of kind Nat
    1213r,s,t:  arbitrary terms of kind Nat
    13 {expr}:
    1414}}}
    1515
     
    2424Addition:
    2525{{{
    26 addDef:      m + n ~ {m + n}
     26addDef:      m + n ~ k     -- if "m + n == k"
    2727addUnit:     0 + t ~ t
    2828addAssoc:    (r + s) + t ~ r + (s + t)
     
    3333Multiplication:
    3434{{{
    35 mulDef:      m * n ~ {m * n}
     35mulDef:      m * n ~ k   -- if "m * n == k"
    3636mulUnit:     1 * t ~ t
    3737mulAssoc:    (r * s) * t ~ r * (s * t)