Changes between Version 2 and Version 3 of TypeNats/Axioms


Ignore:
Timestamp:
Nov 27, 2010 9:09:00 PM (4 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)