| symbol | specification | entry |
|---|
| # | list-data | function,
list → nat |
| # | stackseq | function,
llist → nat |
| # | indexseq | function,
illist → nat |
| # | indexseq | function,
ilist → nat |
| #oc | list-perm | function,
elem × list → nat |
| #oc | indexseq | function,
nat × ilist → nat |
| ' | list | function,
elem → list |
| ' | stackseq | function,
list → llist |
| ' | indexseq | function,
ilist → illist |
| ' | indexseq | function,
nat → ilist |
| + | nat-basic2 | function,
nat × nat → nat |
| + | list-data | function,
elem × list → list |
| + | list | function,
elem × elem → list |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → list |
| + | stackseq | function,
llist × list → llist |
| + | stackseq | function,
llist × llist → llist |
| + | stackseq | function,
list × llist → llist |
| + | indexseq | function,
illist × ilist → illist |
| + | indexseq | function,
illist × illist → illist |
| + | indexseq | function,
ilist × illist → illist |
| + | indexseq | function,
ilist × nat → ilist |
| + | indexseq | function,
ilist × ilist → ilist |
| + | indexseq | function,
nat × ilist → ilist |
| ++ | list-dup | function,
list × elem → list |
| ++ | stackseq | function,
llist × list → llist |
| ++ | indexseq | function,
illist × ilist → illist |
| ++ | indexseq | function,
ilist × nat → ilist |
| +1 | nat-basic1 | function,
nat → nat |
| - | nat | function,
nat × nat → nat |
| -1 | nat-basic1 | function,
nat → nat |
| -1l | list-del | function,
list × nat → list |
| -1l | list-del | function,
list × elem → list |
| -1l | stackseq | function,
llist × nat → llist |
| -1l | stackseq | function,
llist × list → llist |
| -1l | indexseq | function,
illist × nat → illist |
| -1l | indexseq | function,
illist × ilist → illist |
| -1l | indexseq | function,
ilist × nat → ilist |
| -1p | indexseq | function,
ilist × nat → ilist |
| -l | list-del | function,
list × elem → list |
| -l | stackseq | function,
llist × list → llist |
| -l | indexseq | function,
illist × ilist → illist |
| -l | indexseq | function,
ilist × nat → ilist |
| .butlast | list-last | function,
list → list |
| .butlast | stackseq | function,
llist → llist |
| .butlast | indexseq | function,
illist → illist |
| .butlast | indexseq | function,
ilist → ilist |
| .first | list-data | function,
list → elem |
| .first | stackseq | function,
llist → list |
| .first | indexseq | function,
illist → ilist |
| .first | indexseq | function,
ilist → nat |
| .last | list-last | function,
list → elem |
| .last | stackseq | function,
llist → list |
| .last | indexseq | function,
illist → ilist |
| .last | indexseq | function,
ilist → nat |
| .rest | list-data | function,
list → list |
| .rest | stackseq | function,
llist → llist |
| .rest | indexseq | function,
illist → illist |
| .rest | indexseq | function,
ilist → ilist |
| .tolist | solitaire | function,
ilist × list → list |
| .tolist | solitaire | function,
illist × list → llist |
| < | nat-basic1 | predicate,
nat × nat |
| < | list-data | predicate,
list × list |
| < | oelem | predicate,
elem × elem |
| < | stackseq | predicate,
llist × llist |
| < | indexseq | predicate,
illist × illist |
| < | indexseq | predicate,
ilist × ilist |
| > | nat | predicate,
nat × nat |
| [] | list-data | constant,
list |
| [] | stackseq | constant,
llist |
| [] | indexseq | constant,
illist |
| [] | indexseq | constant,
ilist |
| \ | list-set | function,
list × list → list |
| \ | indexseq | function,
ilist × ilist → ilist |
| ] | list-del | function,
list × nat × elem → list |
| ] | list-del | function,
list × nat → elem |
| ] | stackseq | function,
llist × nat × list → llist |
| ] | stackseq | function,
llist × nat → list |
| ] | indexseq | function,
illist × nat × ilist → illist |
| ] | indexseq | function,
illist × nat → ilist |
| ] | indexseq | function,
ilist × nat × nat → ilist |
| ] | indexseq | function,
ilist × nat → nat |
| a | elem | variable,
elem |
| a0 | list-data | variable,
elem |
| all< | solitaire | predicate,
ilist × nat |
| ascsubseq | solitaire | predicate,
ilist × list |
| b | elem | variable,
elem |
| butlastn | list-last | function,
nat × list → list |
| butlastn | stackseq | function,
nat × llist → llist |
| butlastn | indexseq | function,
nat × illist → illist |
| butlastn | indexseq | function,
nat × ilist → ilist |
| c | elem | variable,
elem |
| covers | solitaire | predicate,
illist × ilist |
| covers | solitaire | predicate,
illist × nat |
| disj | list-dup | predicate,
list × list |
| disj | stackseq | predicate,
llist × llist |
| disj | indexseq | predicate,
illist × illist |
| disj | indexseq | predicate,
ilist × ilist |
| dups | list-dup | predicate,
list |
| dups | stackseq | predicate,
llist |
| dups | indexseq | predicate,
illist |
| dups | indexseq | predicate,
ilist |
| elem | elem | sort,
|
| fillfirst | list-last | function,
nat × elem × list → list |
| fillfirst | stackseq | function,
nat × list × llist → llist |
| fillfirst | indexseq | function,
nat × ilist × illist → illist |
| fillfirst | indexseq | function,
nat × nat × ilist → ilist |
| filter | list-set | function,
list × list → list |
| filter | indexseq | function,
ilist × ilist → ilist |
| firstn | list-del | function,
nat × list → list |
| firstn | stackseq | function,
nat × llist → llist |
| firstn | indexseq | function,
nat × illist → illist |
| firstn | indexseq | function,
nat × ilist → ilist |
| frome | list-del | function,
list × elem → list |
| frome | stackseq | function,
llist × list → llist |
| frome | indexseq | function,
illist × ilist → illist |
| frome | indexseq | function,
ilist × nat → ilist |
| ilist | indexseq | sort,
|
| illist | indexseq | sort,
|
| ins≤ | olist | function,
elem × list → list |
| ins≤ | indexseq | function,
nat × ilist → ilist |
| inv | solitaire | predicate,
illist × nat |
| ix | indexseq | variable,
ilist |
| ix0 | indexseq | variable,
ilist |
| ix1 | indexseq | variable,
ilist |
| ix10 | indexseq | variable,
ilist |
| ix2 | indexseq | variable,
ilist |
| ix3 | indexseq | variable,
ilist |
| ix4 | indexseq | variable,
ilist |
| ix5 | indexseq | variable,
ilist |
| ix6 | indexseq | variable,
ilist |
| ix7 | indexseq | variable,
ilist |
| ix8 | indexseq | variable,
ilist |
| ix9 | indexseq | variable,
ilist |
| ixs | indexseq | variable,
illist |
| ixs0 | indexseq | variable,
illist |
| ixs1 | indexseq | variable,
illist |
| ixs10 | indexseq | variable,
illist |
| ixs2 | indexseq | variable,
illist |
| ixs3 | indexseq | variable,
illist |
| ixs4 | indexseq | variable,
illist |
| ixs5 | indexseq | variable,
illist |
| ixs6 | indexseq | variable,
illist |
| ixs7 | indexseq | variable,
illist |
| ixs8 | indexseq | variable,
illist |
| ixs9 | indexseq | variable,
illist |
| lastn | list-del | function,
nat × list → list |
| lastn | stackseq | function,
nat × llist → llist |
| lastn | indexseq | function,
nat × illist → illist |
| lastn | indexseq | function,
nat × ilist → ilist |
| list | list-data | sort,
|
| llist | stackseq | sort,
|
| m | nat-basic2 | variable,
nat |
| maxincseq# | solitaire | function,
list → nat |
| merge | olist | function,
list × list → list |
| merge | indexseq | function,
ilist × ilist → ilist |
| mklist | list-last | function,
elem × nat → list |
| mklist | stackseq | function,
list × nat → llist |
| mklist | indexseq | function,
ilist × nat → illist |
| mklist | indexseq | function,
nat × nat → ilist |
| n | nat-basic1 | variable,
nat |
| n0 | nat-basic1 | variable,
nat |
| n1 | nat-basic1 | variable,
nat |
| n3 | indexseq | variable,
nat |
| n4 | indexseq | variable,
nat |
| n5 | indexseq | variable,
nat |
| n6 | indexseq | variable,
nat |
| nat | nat-basic1 | sort,
|
| ordered | solitaire | predicate,
illist × list |
| ordered | solitaire | predicate,
ilist × list |
| ordered< | olist | predicate,
list |
| ordered< | indexseq | predicate,
ilist |
| ordered≤ | olist | predicate,
list |
| ordered≤ | indexseq | predicate,
ilist |
| perm | list-perm | predicate,
list × list |
| perm | indexseq | predicate,
ilist × ilist |
| plus | stackseq | function,
list × list → llist |
| plus | indexseq | function,
ilist × ilist → illist |
| plus | indexseq | function,
nat × nat → ilist |
| pos | list-del | function,
elem × list → nat |
| pos | stackseq | function,
list × llist → nat |
| pos | indexseq | function,
ilist × illist → nat |
| pos | indexseq | function,
nat × ilist → nat |
| precedes | solitaire | predicate,
nat × nat × list |
| precedes∃ | solitaire | predicate,
illist × list |
| push | solitaire | function,
elem × llist → llist |
| pushx | solitaire | function,
nat × illist × list → illist |
| restn | list-del | function,
nat × list → list |
| restn | stackseq | function,
nat × llist → llist |
| restn | indexseq | function,
nat × illist → illist |
| restn | indexseq | function,
nat × ilist → ilist |
| rev | list-last | function,
list → list |
| rev | stackseq | function,
llist → llist |
| rev | indexseq | function,
illist → illist |
| rev | indexseq | function,
ilist → ilist |
| rmdup | list-dup | function,
list → list |
| rmdup | stackseq | function,
llist → llist |
| rmdup | indexseq | function,
illist → illist |
| rmdup | indexseq | function,
ilist → ilist |
| solitaire | solitaire | function,
list → llist |
| solitaireh | solitaire | function,
list × llist → llist |
| solix | solitaire | function,
list → illist |
| solixh | solitaire | function,
list × nat × illist → illist |
| sublist | list-del | function,
nat × nat × list → list |
| sublist | stackseq | function,
nat × nat × llist → llist |
| sublist | indexseq | function,
nat × nat × illist → illist |
| sublist | indexseq | function,
nat × nat × ilist → ilist |
| x | list-data | variable,
list |
| x0 | list-data | variable,
list |
| x1 | list-data | variable,
list |
| x2 | list-data | variable,
list |
| xs | stackseq | variable,
llist |
| xs0 | stackseq | variable,
llist |
| xs1 | stackseq | variable,
llist |
| xs10 | stackseq | variable,
llist |
| xs2 | stackseq | variable,
llist |
| xs3 | stackseq | variable,
llist |
| xs4 | stackseq | variable,
llist |
| xs5 | stackseq | variable,
llist |
| xs6 | stackseq | variable,
llist |
| xs7 | stackseq | variable,
llist |
| xs8 | stackseq | variable,
llist |
| xs9 | stackseq | variable,
llist |
| y | list-data | variable,
list |
| y0 | list-data | variable,
list |
| y1 | list-data | variable,
list |
| y2 | list-data | variable,
list |
| z | list-data | variable,
list |
| z0 | list-data | variable,
list |
| z1 | list-data | variable,
list |
| z2 | list-data | variable,
list |
| ∈ | list | predicate,
elem × list |
| ∈ | stackseq | predicate,
list × llist |
| ∈ | indexseq | predicate,
ilist × illist |
| ∈ | indexseq | predicate,
nat × ilist |
| ∪ | list-set | function,
list × list → list |
| ∪ | indexseq | function,
ilist × ilist → ilist |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | list-set | predicate,
list × list |
| ⊆ | indexseq | predicate,
ilist × ilist |
| ⊆m | list-perm | predicate,
list × list |
| ⊆m | indexseq | predicate,
ilist × ilist |
| ⊑ | list-last | predicate,
list × list |
| ⊑ | stackseq | predicate,
llist × llist |
| ⊑ | indexseq | predicate,
illist × illist |
| ⊑ | indexseq | predicate,
ilist × ilist |
| ⊒ | list-last | predicate,
list × list |
| ⊒ | stackseq | predicate,
llist × llist |
| ⊒ | indexseq | predicate,
illist × illist |
| ⊒ | indexseq | predicate,
ilist × ilist |