Changes between Version 8 and Version 9 of TypeNats/Interact1

Timestamp:

12/18/10 21:01:51 (2 years ago)

Author:

diatchki

Comment:

--

TypeNats/Interact1

@@ -44 +44 @@
 (a * 1 ~ b) <=> a ~ b
 (a * b ~ 1) <=> (a ~ 1, b ~ 1)
-(a + a ~ b) <=> a ^ 2 ~ b
+(a * a ~ b) <=> a ^ 2 ~ b
+(m * a ~ a) <=> a ~ 0            -- 2 <= m
 }}}
 
@@ -54 +55 @@
 (a ^ 0 ~ b) <=> b ~ 1
 (1 ^ a ~ b) <=> b ~ 1 
+(m ^ a ~ a) <=> False           -- m /= 1
 }}}