| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | set_of_nat | f | natset → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . ++ . | set_of_nat | f | natset × nat → natset |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -- . | set_of_nat | f | natset × nat → natset |
| . -1 | nat-basic1 | f | nat → nat |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . \ . | set_of_nat | f | natset × natset → natset |
| . ∈ . | set_of_nat | p | nat × natset |
| . ∩ . | set_of_nat | f | natset × natset → natset |
| . ∪ . | set_of_nat | f | natset × natset → natset |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | set_of_nat | p | natset × natset |
| { . } | set_of_nat | f | nat → natset |
| ∅ | set_of_nat | c | natset |
| S | set_of_nat | v | natset |
| S0 | set_of_nat | v | natset |
| S1 | set_of_nat | v | natset |
| S2 | set_of_nat | v | natset |
| m | nat-basic2 | v | nat |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| n2 | set_of_nat | v | nat |
| n3 | set_of_nat | v | nat |
| n4 | set_of_nat | v | nat |
| nat | nat-basic1 | s | |
| natset | set_of_nat | s |