| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | map_nat_nat | f | mapnatnat → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -- . | map_nat_nat | f | mapnatnat × nat → mapnatnat |
| . -1 | nat-basic1 | f | nat → nat |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | map_nat_nat | f | mapnatnat × nat → nat |
| . [ . ] | map_nat_nat | f | mapnatnat × nat × nat → mapnatnat |
| . × . | map_nat_nat | f | nat × nat → natnat |
| . ∈ . | map_nat_nat | p | natnat × mapnatnat |
| . ∈ . | map_nat_nat | p | nat × mapnatnat |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | map_nat_nat | p | mapnatnat × mapnatnat |
| ∅ | map_nat_nat | c | mapnatnat |
| D | map_nat_nat | v | mapnatnat |
| D0 | map_nat_nat | v | mapnatnat |
| D1 | map_nat_nat | v | mapnatnat |
| D2 | map_nat_nat | v | mapnatnat |
| m | nat-basic2 | v | nat |
| mapnatnat | map_nat_nat | s | |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| n2 | map_nat_nat | v | nat |
| n3 | map_nat_nat | v | nat |
| n4 | map_nat_nat | v | nat |
| n5 | map_nat_nat | v | nat |
| n6 | map_nat_nat | v | nat |
| n7 | map_nat_nat | v | nat |
| n8 | map_nat_nat | v | nat |
| n9 | map_nat_nat | v | nat |
| nat | nat-basic1 | s | |
| natnat | map_nat_nat | s | |
| nn | map_nat_nat | v | natnat |