| symbol | specification | entry |
|---|
| # | array | function,
array → nat |
| # | bag-union | function,
bag → nat |
| + | nat-basic | function,
nat × nat → nat |
| ++ | bag-basic | function,
bag × elem → bag |
| +1 | nat-basic | function,
nat → nat |
| - | nat | partial function,
nat × nat → nat |
| -- | bag-union | function,
bag × elem → bag |
| -1 | nat-basic | partial function,
nat → nat |
| < | nat-basic | predicate,
nat × nat |
| < | oelem | predicate,
elem × elem |
| > | nat | predicate,
nat × nat |
| A | oarray-sorted | variable,
array |
| A0 | oarray-sorted | variable,
array |
| Inv-end | sort-invariants | predicate,
array × array × nat × nat × elem |
| Inv-first-inner | sort-invariants | predicate,
array × array × elem × elem × nat × nat |
| Inv-last-inner | sort-invariants | predicate,
array × array × elem × elem × nat × nat |
| Inv-main | sort-invariants | predicate,
array × array × nat |
| \ | bag-union | function,
bag × bag → bag |
| ] | array | partial function,
array × nat × elem → array |
| ] | array | partial function,
array × nat → elem |
| a | elem | variable,
elem |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| b | elem | variable,
elem |
| bag | bag-basic | variable,
bag |
| bag | bag-basic | sort,
|
| bag0 | bag-basic | variable,
bag |
| bag1 | bag-basic | variable,
bag |
| bag2 | bag-basic | variable,
bag |
| c | elem | variable,
elem |
| cmp | array-copy | partial predicate,
array × elem × nat × nat |
| cmp | array-copy | partial predicate,
array × nat × array × nat × nat |
| cmp | array-copy | predicate,
array × elem |
| copy | array-copy | partial function,
array × nat × array × nat × nat → array |
| count | bag-basic | function,
elem × bag → nat |
| elem | elem | sort,
|
| fill | array-copy | partial function,
array × elem × nat × nat → array |
| fill | array-copy | function,
array × elem → array |
| i | oarray-sorted | variable,
nat |
| i0 | oarray-sorted | variable,
nat |
| idrange | array-copy | partial predicate,
array × nat × nat |
| id○ | array-copy | predicate,
array × array × nat |
| j | oarray-sorted | variable,
nat |
| m | nat-basic | variable,
nat |
| m0 | array-copy | variable,
nat |
| mkarray | array | function,
nat → array |
| mkbag | oarray-perm | partial function,
array × nat → bag |
| n | nat-basic | variable,
nat |
| n0 | nat-basic | variable,
nat |
| n1 | nat-basic | variable,
nat |
| nat | nat-basic | sort,
|
| perm | oarray-perm | predicate,
array × array |
| rev | array-copy | partial function,
array × nat → array |
| rev | array-copy | function,
array → array |
| sort# | pair-insertion-sort | procedure,
: array |
| sorted | oarray-sorted | predicate,
array × nat × nat |
| subarray | array-copy | partial function,
array × nat × nat → array |
| x | oarray-sorted | variable,
elem |
| y | oarray-sorted | variable,
elem |
| } | bag-union | function,
elem → bag |
| ∅ | bag-basic | constant,
bag |
| ∈ | array-copy | predicate,
elem × array |
| ∈ | bag-union | predicate,
elem × bag |
| ∪ | bag-union | function,
bag × bag → bag |
| ≤ | nat | predicate,
nat × nat |
| ≤ | oarray-sorted | predicate,
elem × elem |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | bag-union | predicate,
bag × bag |