| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | address-store | f | address-set → nat |
| # . | address-store | f | address-store → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . ++ . | address-store | f | address-set × address → address-set |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | address-store | f | address-store × address → address-store |
| . -- . | address-store | f | address-set × address → address-set |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . .lnum | address-data | f | address → nat |
| . .lnum:= . | address-data | f | address × nat → address |
| . .map ( . ) | address-store | f | address-store × (address × elem → elem) → address-store |
| . .map ( . ) | address-store | f | address-store × (elem → elem) → address-store |
| . .pos | address-data | f | address → nat |
| . .pos:= . | address-data | f | address × nat → address |
| . .size | address-data | f | address → nat |
| . .size:= . | address-data | f | address × nat → address |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | address-store | pf | address-store × address → elem with λ ast, adr. adr ∈ ast |
| . [ . ] | address-store | f | address-store × address × elem → address-store |
| . \ . | address-store | f | address-set × address-set → address-set |
| . \ . | address-store | f | address-store × address-set → address-store |
| . | . | address-store | f | address-store × address-set → address-store |
| . ∈ . | address-store | p | elem × address-store |
| . ∈ . | address-store | p | address × address-set |
| . ∈ . | address-store | p | address × address-store |
| . ∩ . | address-store | f | address-set × address-set → address-set |
| . ∪ . | address-store | f | address-set × address-set → address-set |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | address-store | p | address-set × address-set |
| . ⊆ . | address-store | p | address-store × address-store |
| . ⊕ . | address-store | f | address-store × address-store → address-store |
| @ | address-data | f | nat × nat × nat → address |
| { . } | address-store | f | address → address-set |
| ∅ | address-store | c | address-store |
| ∅ | address-store | c | address-set |
| a | elem | v | elem |
| a0 | address-store | v | elem |
| address | address-data | s | |
| address-set | address-store | s | |
| address-store | address-store | s | |
| addresselemf | address-store | v | address × elem → elem |
| adr | address-data | v | address |
| adr1 | address-store | v | address |
| adr2 | address-store | v | address |
| as | address-store | v | address-set |
| as0 | address-store | v | address-set |
| as1 | address-store | v | address-set |
| as2 | address-store | v | address-set |
| ast | address-store | v | address-store |
| ast0 | address-store | v | address-store |
| ast1 | address-store | v | address-store |
| ast2 | address-store | v | address-store |
| b | elem | v | elem |
| c | elem | v | elem |
| dom . | address-store | f | address-store → address-set |
| elem | elem | s | |
| elemf | address-store | v | elem → elem |
| m | nat-basic | v | nat |
| m0 | address-data | v | nat |
| m1 | address-data | v | nat |
| m2 | address-data | v | nat |
| m3 | address-data | v | nat |
| m4 | address-data | v | nat |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s |