Changes between Version 2 and Version 3 of TypeNats/Rules


Ignore:
Timestamp:
Dec 15, 2010 6:04:42 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Rules

    v2 v3  
    1 Notation: 
    2 {{{ 
    3 m,n,k:  natural numbers 
    4 a,b,c:  types of kind Nat 
    5 }}} 
    6  
    7 Top-level interactions for {{{TypeNat}}}: 
    8 {{{ 
    9 TypeNat m 
    10 }}} 
    11  
    12 Top-level interactions for <= 
    13 {{{ 
    14 m <= n   <=> {m <= n} = True 
    15 0 <= a   <=> True 
    16 a <= 0   <=> a ~ 0 
    17 }}} 
    18  
    19 Top-level interactions for +. 
    20 {{{ 
    21 (m + n ~ k) <=> {m + n} = k 
    22 (m + a ~ n) <=> a ~ {n - m}    -- n >= m 
    23 (a + m ~ n) <=> a ~ {n - m}    -- n >= m 
    24 (0 + a ~ b) <=> a ~ b 
    25 (a + 0 ~ b) <=> a ~ b 
    26 (a + b ~ 0) <=> (a ~ 0, b ~ 0) 
    27 (a + b ~ a) <=> (b ~ 0) 
    28 (a + b ~ b) <=> (a ~ 0) 
    29 (a + a ~ b) <=> (2 * a ~ b) 
    30 }}} 
    31  
    32 Top-level interactions for *. 
    33 {{{ 
    34 (m * n ~ k) <=> {m * n} = k 
    35 (m * a ~ n) <=> a ~ {n / m}     -- m `divides` n 
    36 (a * m ~ n) <=> a ~ {n / m}     -- m `divides` n 
    37 (0 * a ~ b) <=> b ~ 0 
    38 (a * 0 ~ b) <=> b ~ 0 
    39 (1 * a ~ b) <=> a ~ b 
    40 (a * 1 ~ b) <=> a ~ b 
    41 (a * b ~ 1) <=> (a ~ 1, b ~ 1) 
    42 (a + a ~ b) <=> 2 ^ a ~ b 
    43 }}} 
    44  
    45 Top-level interactions for ^ 
    46 {{{ 
    47 (m ^ n ~ k) <=> {m ^ n} = k 
    48 (m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists 
    49 (a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists 
    50 (a ^ 0 ~ b) <=> b ~ 1 
    51 (1 ^ a ~ b) <=> b ~ 1  
    52 }}}