Changes between Version 2 and Version 3 of TypeNats/Rules


Ignore:
Timestamp:
Dec 15, 2010 6:04:42 PM (5 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 }}}