|
|
|
|
|
Notation:
|
|
|
|
|
|
```wiki
|
|
|
m,n,k: natural numbers
|
|
|
a,b,c: types of kind Nat
|
|
|
```
|
|
|
|
|
|
|
|
|
Top-level interaction for +.
|
|
|
|
|
|
```wiki
|
|
|
(m + n ~ k) <=> {m + n} = k
|
|
|
(m + a ~ n) <=> a ~ {n - m} -- n >= m
|
|
|
(a + m ~ n) <=> a ~ {n - m} -- n >= m
|
|
|
(0 + a ~ b) <=> a ~ b
|
|
|
(a + 0 ~ b) <=> a ~ b
|
|
|
(a + b ~ 0) <=> (a ~ 0, b ~ 0)
|
|
|
(a + b ~ a) <=> (b ~ 0)
|
|
|
(a + b ~ b) <=> (a ~ 0)
|
|
|
(a + a ~ b) <=> (2 * a ~ b)
|
|
|
``` |
|
|
\ No newline at end of file |