Changes between Version 9 and Version 10 of TypeNats/Interact1

Timestamp:

12/18/10 21:04:45 (2 years ago)

Author:

diatchki

Comment:

--

TypeNats/Interact1

@@ -54 +54 @@
 (a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists
 (a ^ 0 ~ b) <=> b ~ 1
-(1 ^ a ~ b) <=> b ~ 1 
+(a ^ 1 ~ b) <=> a ~ b
+(1 ^ a ~ b) <=> b ~ 1
 (m ^ a ~ a) <=> False           -- m /= 1
+(a ^ m ~ a) <=> (a <= 1)        -- 2 <= m
 }}}