... | ... | @@ -53,7 +53,8 @@ Top-level interactions for \*. |
|
|
(1 * a ~ b) <=> a ~ b
|
|
|
(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
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -64,5 +65,8 @@ Top-level interactions for `^` |
|
|
(m ^ a ~ n) <=> a ~ {log m n} -- log (base m) of n exists
|
|
|
(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
|
|
|
(a ^ m ~ a) <=> (a <= 1) -- 2 <= m
|
|
|
(1 ^ a ~ b) <=> b ~ 1
|
|
|
(m ^ a ~ a) <=> False -- m /= 1
|
|
|
``` |
|
|
\ No newline at end of file |