Changes between Version 17 and Version 18 of TypeNats/Interact1
 Timestamp:
 Dec 19, 2010 6:10:09 PM (6 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Interact1
v17 v18 14 14 {{{ 15 15 (m + n ~ k) <=> {m + n == k} 16 16 17 (m + a ~ n) <=> a ~ {n  m}  n >= m 17 18 (0 + a ~ b) <=> a ~ b 18 (a + b ~ 0) <=> (a ~ 0, b ~ 0)  XXX: Drop this, follows from <= rules? 19 19 20 (a + b ~ a) <=> (b ~ 0) 20 21 (a + b ~ b) <=> (a ~ 0) 22 21 23 (a + a ~ b) <=> (2 * a ~ b) 24 (a + b ~ 0) <=> (a ~ 0, b ~ 0)  XXX: Drop this, follows from <= rules? 25 22 26 (a + m ~ b) <=> (m + a ~ b)  simple normalization cuts down on some rules 23 27 }}}