| symbol | specification | entry |
|---|
| # | encoding-index-node | function,
index-node-list → nat |
| # | nat-list-set | function,
nat-set → nat |
| # | nat-list-set | function,
nat-list → nat |
| # | encoding-group-node | function,
group-node-list → nat |
| # | set-basic | function,
set → nat |
| # | store | function,
store → nat |
| # | list-data | function,
list → nat |
| # | avolume | function,
avolume → nat |
| # | buffer | function,
buffer → nat |
| # | array | function,
array → nat |
| # | lp-array | function,
lp-array → nat |
| # | nat-set | function,
nat-set → nat |
| # | address-list-set | function,
address-set → nat |
| # | address-list-set | function,
address-list → nat |
| # | laddress-list | function,
laddress-list → nat |
| # | key-index-array | function,
key-array → nat |
| # | gc-heap-base | function,
lp-array → nat |
| # | gc-heap-rename | function,
gc-heap-set → nat |
| # | branch-array | function,
branch-array → nat |
| # | nat-store | function,
nat-set → nat |
| # | group-store | function,
group-address-store → nat |
| # | group-store | function,
group-store → nat |
| # | group-store | function,
group-node-list → nat |
| # | index-store | function,
index-address-store → nat |
| # | index-store | function,
index-store → nat |
| # | index-store | function,
index-node-list → nat |
| # | address-store | function,
address-set → nat |
| # | address-store | function,
address-store → nat |
| # | string | function,
string → nat |
| % | nat-div | partial function,
nat × nat → nat |
| ' | encoding-index-node | function,
index-node → index-node-list |
| ' | nat-list-set | function,
nat → nat-list |
| ' | encoding-group-node | function,
group-node → group-node-list |
| ' | list | function,
elem → list |
| ' | address-list-set | function,
address → address-list |
| ' | laddress-list | function,
laddress → laddress-list |
| ' | group-store | function,
group-node → group-node-list |
| ' | index-store | function,
index-node → index-node-list |
| ' | string | function,
char → string |
| * | nat-mult | function,
nat × nat → nat |
| + | encoding-index-node | function,
index-node-list × index-node → index-node-list |
| + | encoding-index-node | function,
index-node-list × index-node-list → index-node-list |
| + | encoding-index-node | function,
index-node × index-node-list → index-node-list |
| + | nat-list-set | function,
nat-list × nat → nat-list |
| + | nat-list-set | function,
nat-list × nat-list → nat-list |
| + | nat-list-set | function,
nat × nat-list → nat-list |
| + | encoding-group-node | function,
group-node-list × group-node → group-node-list |
| + | encoding-group-node | function,
group-node-list × group-node-list → group-node-list |
| + | encoding-group-node | function,
group-node × group-node-list → group-node-list |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → list |
| + | list-data | function,
elem × list → list |
| + | avolume | function,
avolume × avolume → avolume |
| + | buffer | function,
buffer × buffer → buffer |
| + | array-splice | function,
array × array → array |
| + | address-list-set | function,
address-list × address → address-list |
| + | address-list-set | function,
address-list × address-list → address-list |
| + | address-list-set | function,
address × address-list → address-list |
| + | laddress-list | function,
laddress-list × laddress → laddress-list |
| + | laddress-list | function,
laddress-list × laddress-list → laddress-list |
| + | laddress-list | function,
laddress × laddress-list → laddress-list |
| + | group-store | function,
group-node-list × group-node → group-node-list |
| + | group-store | function,
group-node-list × group-node-list → group-node-list |
| + | group-store | function,
group-node × group-node-list → group-node-list |
| + | index-store | function,
index-node-list × index-node → index-node-list |
| + | index-store | function,
index-node-list × index-node-list → index-node-list |
| + | index-store | function,
index-node × index-node-list → index-node-list |
| + | nat-basic | function,
nat × nat → nat |
| + | string | function,
string × char → string |
| + | string | function,
string × string → string |
| + | string | function,
char × string → string |
| ++ | encoding-index-node | function,
index-node-list × index-node → index-node-list |
| ++ | nat-list-set | function,
nat-set × nat → nat-set |
| ++ | nat-list-set | function,
nat-list × nat → nat-list |
| ++ | encoding-group-node | function,
group-node-list × group-node → group-node-list |
| ++ | set-basic | function,
set × elem → set |
| ++ | list-dup | function,
list × elem → list |
| ++ | nat-set | function,
nat-set × nat → nat-set |
| ++ | address-list-set | function,
address-set × address → address-set |
| ++ | address-list-set | function,
address-list × address → address-list |
| ++ | laddress-list | function,
laddress-list × laddress → laddress-list |
| ++ | keyindex-set | function,
set × keyindex → set |
| ++ | gc-heap-rename | function,
gc-heap-set × keyindex → gc-heap-set |
| ++ | nat-store | function,
nat-set × nat → nat-set |
| ++ | group-store | function,
group-node-list × group-node → group-node-list |
| ++ | index-store | function,
index-node-list × index-node → index-node-list |
| ++ | address-store | function,
address-set × address → address-set |
| ++ | string | function,
string × char → string |
| +1 | nat-basic | function,
nat → nat |
| +2 | encoding-index-node | function,
index-node × index-node → index-node-list |
| +2 | nat-list-set | function,
nat × nat → nat-list |
| +2 | encoding-group-node | function,
group-node × group-node → group-node-list |
| +2 | list | function,
elem × elem → list |
| +2 | address-list-set | function,
address × address → address-list |
| +2 | laddress-list | function,
laddress × laddress → laddress-list |
| +2 | group-store | function,
group-node × group-node → group-node-list |
| +2 | index-store | function,
index-node × index-node → index-node-list |
| +2 | string | function,
char × char → string |
| - | nat | partial function,
nat × nat → nat |
| -- | nat-list-set | function,
nat-set × nat → nat-set |
| -- | set-union | function,
set × elem → set |
| -- | store | function,
store × elem → store |
| -- | nat-set | function,
nat-set × nat → nat-set |
| -- | address-list-set | function,
address-set × address → address-set |
| -- | keyindex-set | function,
set × keyindex → set |
| -- | gc-heap-rename | function,
gc-heap-set × keyindex → gc-heap-set |
| -- | nat-store | function,
nat-set × nat → nat-set |
| -- | nat-store | function,
store × nat → store |
| -- | group-store | function,
group-address-store × address → group-address-store |
| -- | group-store | function,
group-store × nat → group-store |
| -- | index-store | function,
index-address-store × address → index-address-store |
| -- | index-store | function,
index-store × nat → index-store |
| -- | address-store | function,
address-set × address → address-set |
| -- | address-store | function,
address-store × address → address-store |
| -1 | nat-basic | partial function,
nat → nat |
| -1l | encoding-index-node | function,
index-node-list × index-node → index-node-list |
| -1l | nat-list-set | function,
nat-list × nat → nat-list |
| -1l | list-del | function,
list × elem → list |
| -1l | encoding-group-node | function,
group-node-list × group-node → group-node-list |
| -1l | address-list-set | function,
address-list × address → address-list |
| -1l | laddress-list | function,
laddress-list × laddress → laddress-list |
| -1l | group-store | function,
group-node-list × group-node → group-node-list |
| -1l | index-store | function,
index-node-list × index-node → index-node-list |
| -1l | string | function,
string × char → string |
| -l | encoding-index-node | function,
index-node-list × index-node → index-node-list |
| -l | nat-list-set | function,
nat-list × nat → nat-list |
| -l | list-del | function,
list × elem → list |
| -l | encoding-group-node | function,
group-node-list × group-node → group-node-list |
| -l | address-list-set | function,
address-list × address → address-list |
| -l | laddress-list | function,
laddress-list × laddress → laddress-list |
| -l | group-store | function,
group-node-list × group-node → group-node-list |
| -l | index-store | function,
index-node-list × index-node → index-node-list |
| -l | string | function,
string × char → string |
| -p | encoding-index-node | function,
index-node-list × nat → index-node-list |
| -p | nat-list-set | function,
nat-list × nat → nat-list |
| -p | list-del | function,
list × nat → list |
| -p | encoding-group-node | function,
group-node-list × nat → group-node-list |
| -p | address-list-set | function,
address-list × nat → address-list |
| -p | laddress-list | function,
laddress-list × nat → laddress-list |
| -p | group-store | function,
group-node-list × nat → group-node-list |
| -p | index-store | function,
index-node-list × nat → index-node-list |
| -p | string | function,
string × nat → string |
| .adr | branch | function,
branch → address |
| .adr:= | branch | function,
branch × address → branch |
| .alignedsize | encoding-index-node | function,
index-node → nat |
| .alignedsize | encoding-group-node | function,
group-node → nat |
| .alignedsize | encoding-node-base | function,
elem → nat |
| .align↓ | awbuf-inv | function,
avolume → avolume |
| .align↓ | awbuf-inv | function,
buffer → buffer |
| .ar | bin-min-heap | function,
binheap → key-array |
| .ar:= | bin-min-heap | function,
binheap × key-array → binheap |
| .branch? | branch | predicate,
branch |
| .branches | indexnode | function,
index-node → branch-array |
| .branches:= | indexnode | function,
index-node × branch-array → index-node |
| .butlast | encoding-index-node | partial function,
index-node-list → index-node-list |
| .butlast | nat-list-set | partial function,
nat-list → nat-list |
| .butlast | encoding-group-node | partial function,
group-node-list → group-node-list |
| .butlast | list-last | partial function,
list → list |
| .butlast | address-list-set | partial function,
address-list → address-list |
| .butlast | laddress-list | partial function,
laddress-list → laddress-list |
| .butlast | group-store | partial function,
group-node-list → group-node-list |
| .butlast | index-store | partial function,
index-node-list → index-node-list |
| .butlast | string | partial function,
string → string |
| .butmax | oset | partial function,
set → set |
| .butmax | nat-set | partial function,
nat-set → nat-set |
| .butmin | oset | partial function,
set → set |
| .butmin | nat-set | partial function,
nat-set → nat-set |
| .char1 | string | partial function,
string → char |
| .data | aleb | partial function,
aleb → buffer |
| .data | node | partial function,
node → buffer |
| .data:= | aleb | partial function,
aleb × buffer → aleb |
| .data:= | node | partial function,
node × buffer → node |
| .data? | key | predicate,
key |
| .data? | node | predicate,
node |
| .dentry? | key | predicate,
key |
| .dentry? | node | predicate,
node |
| .directory | node | partial predicate,
node |
| .directory:= | node | partial function,
node × bool → node |
| .elem | elem-index | function,
elem-index → elem |
| .elem:= | elem-index | function,
elem-index × elem → elem-index |
| .end | groupnode | predicate,
group-node |
| .end:= | groupnode | function,
group-node × bool → group-node |
| .entry? | branch | predicate,
branch |
| .filter | array-indices | function,
nat-set × nat → bool → nat-set |
| .flags | lprops | function,
lprops → lpropflags |
| .flags:= | lprops | function,
lprops × lpropflags → lprops |
| .flashsize | encoding-index-node | function,
index-node-list → nat |
| .flashsize | encoding-index-node | function,
index-node → nat |
| .flashsize | encoding-group-node | function,
group-node-list → nat |
| .flashsize | encoding-group-node | function,
group-node → nat |
| .flashsize | encoding-node-base | function,
elem → nat |
| .flashsize | abs-list | function,
list → nat |
| .flashsize | ablock-store-inv | function,
list → nat |
| .flashsize | ablock-store-inv | function,
elem → nat |
| .flashsize | group-store | function,
group-node-list → nat |
| .flashsize | group-store | function,
group-node → nat |
| .flashsize | index-store | function,
index-node-list → nat |
| .flashsize | index-store | function,
index-node → nat |
| .gcheapidx | lprops | function,
lprops → nat |
| .gcheapidx:= | lprops | function,
lprops × nat → lprops |
| .gndlist | encoding-group-node | function,
group-block → group-node-list |
| .gndlist | group-store | function,
group-block → group-node-list |
| .gndlist:= | encoding-group-node | function,
group-block × group-node-list → group-block |
| .gndlist:= | group-store | function,
group-block × group-node-list → group-block |
| .head | encoding-index-node | partial function,
index-node-list → index-node |
| .head | nat-list-set | partial function,
nat-list → nat |
| .head | encoding-group-node | partial function,
group-node-list → group-node |
| .head | list-data | partial function,
list → elem |
| .head | address-list-set | partial function,
address-list → address |
| .head | laddress-list | partial function,
laddress-list → laddress |
| .head | group-store | partial function,
group-node-list → group-node |
| .head | index-store | partial function,
index-node-list → index-node |
| .idx | key-index | function,
keyindex → nat |
| .idx | elem-index | function,
elem-index → nat |
| .idx:= | key-index | function,
keyindex × nat → keyindex |
| .idx:= | elem-index | function,
elem-index × nat → elem-index |
| .index? | persistence-state | predicate,
persistence-state |
| .indicesWhere | lp-array | function,
lp-array × lprops → bool × nat → nat-list |
| .indicesWhere | lp-array | function,
lp-array × lprops → bool → nat-list |
| .indicesWhere | array-indices | function,
array × elem → bool × nat → nat-list |
| .indicesWhere | array-indices | function,
array × elem → bool → nat-list |
| .indlist | encoding-index-node | function,
index-block → index-node-list |
| .indlist | index-store | function,
index-block → index-node-list |
| .indlist:= | encoding-index-node | function,
index-block × index-node-list → index-block |
| .indlist:= | index-store | function,
index-block × index-node-list → index-block |
| .ino | key | function,
key → nat |
| .ino | node | partial function,
node → nat |
| .ino:= | key | function,
key × nat → key |
| .ino:= | node | partial function,
node × nat → node |
| .inode? | key | predicate,
key |
| .inode? | node | predicate,
node |
| .isbuf? | bufleb | predicate,
bufleb |
| .ispadding | node-header | predicate,
node-header |
| .ispadding:= | node-header | function,
node-header × bool → node-header |
| .journal? | persistence-state | predicate,
persistence-state |
| .key | key-index | function,
keyindex → key |
| .key | gc-heap-base | function,
keyindex → nat |
| .key | branch | function,
branch → key |
| .key | node | function,
node → key |
| .key:= | key-index | function,
keyindex × key → keyindex |
| .key:= | gc-heap-base | function,
keyindex × nat → keyindex |
| .key:= | branch | function,
branch × key → branch |
| .key:= | node | function,
node × key → node |
| .ladrlist | encoding-index-node | function,
index-block → laddress-list |
| .ladrlist | encoding-group-node | function,
group-block → laddress-list |
| .ladrlist | ablock | function,
ablock → laddress-list |
| .ladrlist | group-store | function,
group-block → laddress-list |
| .ladrlist | index-store | function,
index-block → laddress-list |
| .ladrlist:= | encoding-index-node | function,
index-block × laddress-list → index-block |
| .ladrlist:= | encoding-group-node | function,
group-block × laddress-list → group-block |
| .ladrlist:= | ablock | function,
ablock × laddress-list → ablock |
| .ladrlist:= | group-store | function,
group-block × laddress-list → group-block |
| .ladrlist:= | index-store | function,
index-block × laddress-list → index-block |
| .last | encoding-index-node | partial function,
index-node-list → index-node |
| .last | nat-list-set | partial function,
nat-list → nat |
| .last | encoding-group-node | partial function,
group-node-list → group-node |
| .last | list-last | partial function,
list → elem |
| .last | address-list-set | partial function,
address-list → address |
| .last | laddress-list | partial function,
laddress-list → laddress |
| .last | group-store | partial function,
group-node-list → group-node |
| .last | index-store | partial function,
index-node-list → index-node |
| .last | string | partial function,
string → char |
| .leaf | indexnode | predicate,
index-node |
| .leaf:= | indexnode | function,
index-node × bool → index-node |
| .leb | bufleb | partial function,
bufleb → nat |
| .list | ablock | function,
ablock → list |
| .list:= | ablock | function,
ablock × list → ablock |
| .lnum | address-data | function,
address → nat |
| .lnum | persistence-state | partial function,
persistence-state → nat |
| .lnum:= | address-data | function,
address × nat → address |
| .map | lp-array | function,
lp-array × lprops → lprops → lp-array |
| .map | array-indices | function,
array × elem → elem → array |
| .map | array-indices | function,
nat-set × nat → nat → nat-set |
| .map | store-map | function,
store × elem × data → data → store |
| .map | store-map | function,
store × data → data → store |
| .map | nat-store | function,
store × nat × data → data → store |
| .map | ablock-store | function,
store × nat × ablock → ablock → store |
| .map | ablock-store | function,
store × ablock → ablock → store |
| .map | group-store | function,
group-address-store × address × group-node → group-node → group-address-store |
| .map | group-store | function,
group-address-store × group-node → group-node → group-address-store |
| .map | group-store | function,
group-store × nat × group-block → group-block → group-store |
| .map | group-store | function,
group-store × group-block → group-block → group-store |
| .map | index-store | function,
index-address-store × address × index-node → index-node → index-address-store |
| .map | index-store | function,
index-address-store × index-node → index-node → index-address-store |
| .map | index-store | function,
index-store × nat × index-block → index-block → index-store |
| .map | index-store | function,
index-store × index-block → index-block → index-store |
| .map | address-store | function,
address-store × address × elem → elem → address-store |
| .map | address-store | function,
address-store × elem → elem → address-store |
| .mapIf | lp-array | function,
lp-array × lprops → bool × lprops → lprops × nat → lp-array |
| .mapIf | lp-array | function,
lp-array × lprops → bool × lprops → lprops → lp-array |
| .mapIf | array-indices | function,
array × elem → bool × elem → elem × nat → array |
| .mapIf | array-indices | function,
array × elem → bool × elem → elem → array |
| .mapIndices | lp-array | function,
lp-array × nat-set × lprops → lprops → lp-array |
| .mapIndices | lp-array | function,
lp-array × nat-list × lprops → lprops → lp-array |
| .mapIndices | array-indices | function,
array × nat-set × elem → elem → array |
| .mapIndices | array-indices | function,
array × nat-list × elem → elem → array |
| .mapped? | aleb | predicate,
aleb |
| .max | oset | partial function,
set → elem |
| .max | nat-set | partial function,
nat-set → nat |
| .meta | node | partial function,
node → metadata |
| .meta:= | node | partial function,
node × metadata → node |
| .min | oset | partial function,
set → elem |
| .min | nat-set | partial function,
nat-set → nat |
| .name | key | partial function,
key → string |
| .name:= | key | partial function,
key × string → key |
| .nd | groupnode | function,
group-node → node |
| .nd:= | groupnode | function,
group-node × node → group-node |
| .nlink | node | partial function,
node → nat |
| .nlink:= | node | partial function,
node × nat → node |
| .nsubdirs | node | partial function,
node → nat |
| .nsubdirs:= | node | partial function,
node × nat → node |
| .off | laddress | function,
laddress → nat |
| .off:= | laddress | function,
laddress × nat → laddress |
| .part | key | partial function,
key → nat |
| .part:= | key | partial function,
key × nat → key |
| .pos | address-data | function,
address → nat |
| .pos:= | address-data | function,
address × nat → address |
| .ref-size | encoding-index-node | function,
index-block → nat |
| .ref-size | encoding-group-node | function,
group-block → nat |
| .ref-size | lprops | function,
lprops → nat |
| .ref-size | ablock | function,
ablock → nat |
| .ref-size | group-store | function,
group-block → nat |
| .ref-size | index-store | function,
index-block → nat |
| .ref-size:= | encoding-index-node | function,
index-block × nat → index-block |
| .ref-size:= | encoding-group-node | function,
group-block × nat → group-block |
| .ref-size:= | lprops | function,
lprops × nat → lprops |
| .ref-size:= | ablock | function,
ablock × nat → ablock |
| .ref-size:= | group-store | function,
group-block × nat → group-block |
| .ref-size:= | index-store | function,
index-block × nat → index-block |
| .rstring | string | partial function,
string → string |
| .size | lprops | function,
lprops → nat |
| .size | node-header | function,
node-header → nat |
| .size | address-data | function,
address → nat |
| .size | laddress | function,
laddress → nat |
| .size | bin-min-heap | function,
binheap → nat |
| .size | node | partial function,
node → nat |
| .size | ablock-store-refsize-cons | function,
address-set → nat |
| .size:= | lprops | function,
lprops × nat → lprops |
| .size:= | node-header | function,
node-header × nat → node-header |
| .size:= | address-data | function,
address × nat → address |
| .size:= | laddress | function,
laddress × nat → laddress |
| .size:= | bin-min-heap | function,
binheap × nat → binheap |
| .size:= | node | partial function,
node × nat → node |
| .sqnum | groupnode | function,
group-node → nat |
| .sqnum:= | groupnode | function,
group-node × nat → group-node |
| .start | groupnode | predicate,
group-node |
| .start:= | groupnode | function,
group-node × bool → group-node |
| .tail | encoding-index-node | partial function,
index-node-list → index-node-list |
| .tail | nat-list-set | partial function,
nat-list → nat-list |
| .tail | encoding-group-node | partial function,
group-node-list → group-node-list |
| .tail | list-data | partial function,
list → list |
| .tail | address-list-set | partial function,
address-list → address-list |
| .tail | laddress-list | partial function,
laddress-list → laddress-list |
| .tail | group-store | partial function,
group-node-list → group-node-list |
| .tail | index-store | partial function,
index-node-list → index-node-list |
| .to-adr | ablock-store-inv | function,
laddress-list × nat → address-list |
| .toSet | nat-list-set | function,
nat-list → nat-set |
| .toSet | address-list-set | function,
address-list → address-set |
| .toSet | list+set | function,
list → set |
| .toString | debug | function,
nat → string |
| .trunc? | node | predicate,
node |
| .usedsize | indexnode | function,
index-node → nat |
| .usedsize:= | indexnode | function,
index-node × nat → index-node |
| / | nat-div | partial function,
nat × nat → nat |
| 2^ | nat-pot | function,
nat → nat |
| 2exp-size | bin-min-heap-inv | predicate,
nat |
| < | encoding-index-node | predicate,
index-node-list × index-node-list |
| < | nat-list-set | predicate,
nat-list × nat-list |
| < | encoding-group-node | predicate,
group-node-list × group-node-list |
| < | list-data | predicate,
list × list |
| < | oelem | predicate,
elem × elem |
| < | oset | predicate,
set × elem |
| < | oset | predicate,
elem × set |
| < | nat-set | predicate,
nat-set × nat |
| < | nat-set | predicate,
nat × nat-set |
| < | address-list-set | predicate,
address-list × address-list |
| < | nat-list-less | predicate,
nat-list × nat |
| < | laddress-list | predicate,
laddress-list × laddress-list |
| < | binheap-key | predicate,
key × key |
| < | group-store | predicate,
group-node-list × group-node-list |
| < | index-store | predicate,
index-node-list × index-node-list |
| < | nat-basic | predicate,
nat × nat |
| =○refsize | ablock-store-inv | predicate,
store × store |
| =○refsize | group-store | predicate,
group-store × group-store |
| =○refsize | index-store | predicate,
index-store × index-store |
| > | nat | predicate,
nat × nat |
| @ | address-data | function,
nat × nat × nat → address |
| @ | laddress | function,
nat × nat → laddress |
| ADR | persistence-asm | variable,
address,flexible |
| ADR | apersistence-asm | variable,
address,flexible |
| ADRLIST | persistence-asm | variable,
address-list,flexible |
| ADRLIST | apersistence-asm | variable,
address-list,flexible |
| ADR_DUMMY | constants | constant,
address |
| ALIGNEDSIZE | encoding-node-base | variable,
nat,flexible |
| AROFS | awbuf-asm | variable,
bool,flexible |
| AROFS0 | awbuf-asm | variable,
bool,flexible |
| BRANCH_SIZE | constants | constant,
nat |
| BUF | encoding-node-base | variable,
buffer,flexible |
| BUF | awbuf-asm | variable,
buffer,flexible |
| BUF0 | awbuf-asm | variable,
buffer,flexible |
| Boolvar | encoding-node-header | variable,
bool,flexible |
| Boolvar | gc-heap-base | variable,
bool,flexible |
| COMMIT? | awbuf-asm | variable,
bool,flexible |
| COMMIT? | apersistence-asm | variable,
bool,flexible |
| EACCESS | error | constant,
error |
| EBADFD | error | constant,
error |
| EB_PAGE_SIZE | eraseblock | constant,
nat |
| ECOMMIT | error | constant,
error |
| EEXISTS | error | constant,
error |
| EFAIL | error | constant,
error |
| EINVAL | error | constant,
error |
| EIO | error | constant,
error |
| EISDIR | error | constant,
error |
| EMPTY? | persistence-asm | variable,
bool,flexible |
| EMPTY? | apersistence-asm | variable,
bool,flexible |
| ENCODED_ELEM_SIZE | encoding-elem-size | constant,
nat |
| ENOENT | error | constant,
error |
| ENOMEM | error | constant,
error |
| ENOSPC | error | constant,
error |
| ENOTDIR | error | constant,
error |
| ENOTEMPTY | error | constant,
error |
| EROFS | error | constant,
error |
| ERR | error-class | variable,
error,flexible |
| ERR0 | error-class | variable,
error,flexible |
| ESUCCESS | error | constant,
error |
| EUCLEAN | error | constant,
error |
| FLASHSIZE | persistence-asm | variable,
nat,flexible |
| FREELIST | persistence-asm | variable,
nat-list,flexible |
| GCHEAP | persistence-asm | variable,
binheap,flexible |
| GINVAL | apersistence-asm | variable,
nat-set,flexible |
| GND | encoding-group-node | variable,
group-node,flexible |
| GND | apersistence-asm | variable,
group-node,flexible |
| GNDLIST | apersistence-asm | variable,
group-node-list,flexible |
| GSTORE | apersistence-asm | variable,
group-store,flexible |
| GSTORE0 | apersistence-asm | variable,
group-store,flexible |
| IDX | persistence-asm | variable,
nat,flexible |
| IND | encoding-index-node | variable,
index-node,flexible |
| IND | apersistence-asm | variable,
index-node,flexible |
| ISBUF | awbuf-asm | variable,
bool,flexible |
| ISGBLOCK | apersistence-asm | variable,
bool,flexible |
| ISPAD | encoding-node-base | variable,
bool,flexible |
| ISTORE | apersistence-asm | variable,
index-store,flexible |
| ISTORE0 | apersistence-asm | variable,
index-store,flexible |
| KI | persistence-asm | variable,
keyindex,flexible |
| LADR | apersistence-asm | variable,
laddress,flexible |
| LADRLIST | apersistence-asm | variable,
laddress-list,flexible |
| LEBSIZE | persistence-asm | variable,
nat,flexible |
| LEB_SIZE | eraseblock | constant,
nat |
| LNUM | awbuf-asm | variable,
nat,flexible |
| LNUM | apersistence-asm | variable,
nat,flexible |
| LOG | awbuf-asm | variable,
nat-list,flexible |
| LOG0 | persistence-asm | variable,
nat-list,flexible |
| LPT | awbuf-asm | variable,
lp-array,flexible |
| LPT0 | persistence-asm | variable,
lp-array,flexible |
| LP_FREE | lprops | constant,
lpropflags |
| LP_GROUP_NODES | lprops | constant,
lpropflags |
| LP_INDEX_NODES | lprops | constant,
lpropflags |
| MAXINO | apersistence-asm | variable,
nat,flexible |
| MAXINO0 | apersistence-asm | variable,
nat,flexible |
| MIN_SIZE | constants | constant,
nat |
| N | awbuf-asm | variable,
nat,flexible |
| N | apersistence-asm | variable,
nat,flexible |
| N0 | awbuf-asm | variable,
nat,flexible |
| N0 | apersistence-asm | variable,
nat,flexible |
| N1 | awbuf-asm | variable,
nat,flexible |
| ND | encoding-node-base | variable,
elem,flexible |
| NDHD | encoding-node-base | variable,
node-header,flexible |
| NDSIZE | encoding-node-base | variable,
nat,flexible |
| NL | apersistence-asm | variable,
nat-list,flexible |
| NL0 | apersistence-asm | variable,
nat-list,flexible |
| NODELIST | persistence-asm | variable,
group-node-list,flexible |
| NODE_HEADER_SIZE | node-header-size | constant,
nat |
| NS | apersistence-asm | variable,
nat-set,flexible |
| NS0 | apersistence-asm | variable,
nat-set,flexible |
| NS1 | apersistence-asm | variable,
nat-set,flexible |
| OFFSET | encoding-node-base | variable,
nat,flexible |
| OFFSET | awbuf-asm | variable,
nat,flexible |
| OFFSET | apersistence-asm | variable,
nat,flexible |
| ORPHANS | awbuf-asm | variable,
nat-set,flexible |
| ORPHANS0 | persistence-asm | variable,
nat-set,flexible |
| OS | apersistence-asm | variable,
nat-set,flexible |
| OS0 | apersistence-asm | variable,
nat-set,flexible |
| PAGESIZE | persistence-asm | variable,
nat,flexible |
| PAGES_PER_LEB | eraseblock | constant,
nat |
| PAGES_PER_PEB | eraseblock | constant,
nat |
| PEB_SIZE | eraseblock | constant,
nat |
| PSTATE | apersistence-asm | variable,
persistence-state,flexible |
| PSYNCED | apersistence-asm | variable,
bool,flexible |
| Plprops | gc-heap-base | variable,
lprops → bool |
| ROFS | persistence-asm | variable,
bool,flexible |
| ROFS | apersistence-asm | variable,
bool,flexible |
| ROOTADR | apersistence-asm | variable,
address,flexible |
| ROOTADR0 | apersistence-asm | variable,
address,flexible |
| SIZE | encoding-node-base | variable,
nat,flexible |
| SIZE | awbuf-asm | variable,
nat,flexible |
| SIZE | apersistence-asm | variable,
nat,flexible |
| SIZE0 | encoding-node-base | variable,
nat,flexible |
| TRAILER | encoding-node-base | variable,
buffer,flexible |
| VFS_PAGE_SIZE | page | constant,
nat |
| VOLSIZE | awbuf-asm | variable,
nat,flexible |
| VOLSIZE | apersistence-asm | variable,
nat,flexible |
| WBUFLEB | awbuf-asm | variable,
bufleb,flexible |
| WBUFLEB0 | awbuf-asm | variable,
bufleb,flexible |
| WLOG | awbuf-asm | variable,
nat-list,flexible |
| WLPT | awbuf-asm | variable,
lp-array,flexible |
| WMAXINO | awbuf-asm | variable,
nat,flexible |
| WMAXINO0 | awbuf-asm | variable,
nat,flexible |
| WORPHANS | awbuf-asm | variable,
nat-set,flexible |
| WROOTADR | awbuf-asm | variable,
address,flexible |
| WROOTADR0 | awbuf-asm | variable,
address,flexible |
| WVOL | awbuf-asm | variable,
avolume,flexible |
| [] | encoding-index-node | constant,
index-node-list |
| [] | nat-list-set | constant,
nat-list |
| [] | encoding-group-node | constant,
group-node-list |
| [] | list-data | constant,
list |
| [] | address-list-set | constant,
address-list |
| [] | laddress-list | constant,
laddress-list |
| [] | group-store | constant,
group-node-list |
| [] | index-store | constant,
index-node-list |
| \ | nat-list-set | function,
nat-set × nat-set → nat-set |
| \ | store+set | function,
store × set → store |
| \ | set-union | function,
set × set → set |
| \ | nat-set | function,
nat-set × nat-set → nat-set |
| \ | address-list-set | function,
address-set × address-set → address-set |
| \ | gc-heap-rename | function,
gc-heap-set × gc-heap-set → gc-heap-set |
| \ | nat-store | function,
store × nat-set → store |
| \ | nat-store | function,
nat-set × nat-set → nat-set |
| \ | group-store | function,
group-address-store × address-set → group-address-store |
| \ | group-store | function,
group-store × nat-set → group-store |
| \ | index-store | function,
index-address-store × address-set → index-address-store |
| \ | index-store | function,
index-store × nat-set → index-store |
| \ | address-store | function,
address-store × address-set → address-store |
| \ | address-store | function,
address-set × address-set → address-set |
| ] | encoding-index-node | partial function,
index-node-list × nat × index-node → index-node-list |
| ] | encoding-index-node | partial function,
index-node-list × nat → index-node |
| ] | nat-list-set | partial function,
nat-list × nat × nat → nat-list |
| ] | nat-list-set | partial function,
nat-list × nat → nat |
| ] | list-del | partial function,
list × nat × elem → list |
| ] | list-del | partial function,
list × nat → elem |
| ] | encoding-group-node | partial function,
group-node-list × nat × group-node → group-node-list |
| ] | encoding-group-node | partial function,
group-node-list × nat → group-node |
| ] | store | partial function,
store × elem → data |
| ] | store | function,
store × elem × data → store |
| ] | avolume | partial function,
avolume × nat × aleb → avolume |
| ] | avolume | partial function,
avolume × nat → aleb |
| ] | buffer | partial function,
buffer × nat × data → buffer |
| ] | buffer | partial function,
buffer × nat → data |
| ] | array | partial function,
array × nat × elem → array |
| ] | array | partial function,
array × nat → elem |
| ] | lp-array | partial function,
lp-array × nat × lprops → lp-array |
| ] | lp-array | partial function,
lp-array × nat → lprops |
| ] | address-list-set | partial function,
address-list × nat × address → address-list |
| ] | address-list-set | partial function,
address-list × nat → address |
| ] | laddress-list | partial function,
laddress-list × nat × laddress → laddress-list |
| ] | laddress-list | partial function,
laddress-list × nat → laddress |
| ] | key-index-array | partial function,
key-array × nat × keyindex → key-array |
| ] | key-index-array | partial function,
key-array × nat → keyindex |
| ] | index-array-base | partial function,
array × nat × elem-index → array |
| ] | index-array-base | partial function,
array × nat → elem-index |
| ] | gc-heap-base | partial function,
lp-array × nat × lprops → lp-array |
| ] | gc-heap-base | partial function,
lp-array × nat → lprops |
| ] | branch-array | partial function,
branch-array × nat × branch → branch-array |
| ] | branch-array | partial function,
branch-array × nat → branch |
| ] | nat-store | partial function,
store × nat → data |
| ] | nat-store | function,
store × nat × data → store |
| ] | ablock-store | partial function,
store × nat → ablock |
| ] | ablock-store | function,
store × nat × ablock → store |
| ] | ablock-store-inv | function,
store × address → elem |
| ] | group-store | partial function,
group-address-store × address → group-node |
| ] | group-store | partial function,
group-store × nat → group-block |
| ] | group-store | partial function,
group-node-list × nat × group-node → group-node-list |
| ] | group-store | partial function,
group-node-list × nat → group-node |
| ] | group-store | function,
group-address-store × address × group-node → group-address-store |
| ] | group-store | function,
group-store × address → group-node |
| ] | group-store | function,
group-store × nat × group-block → group-store |
| ] | index-store | partial function,
index-address-store × address → index-node |
| ] | index-store | partial function,
index-store × nat → index-block |
| ] | index-store | partial function,
index-node-list × nat × index-node → index-node-list |
| ] | index-store | partial function,
index-node-list × nat → index-node |
| ] | index-store | function,
index-address-store × address × index-node → index-address-store |
| ] | index-store | function,
index-store × address → index-node |
| ] | index-store | function,
index-store × nat × index-block → index-store |
| ] | address-store | partial function,
address-store × address → elem |
| ] | address-store | function,
address-store × address × elem → address-store |
| ] | string | partial function,
string × nat × char → string |
| ] | string | partial function,
string × nat → char |
| ^ | nat-pot | function,
nat × nat → nat |
| a | elem | variable,
elem |
| a0 | list-data | variable,
elem |
| a0 | elem-index | variable,
elem |
| a0 | address-store | variable,
elem |
| ablock | ablock | variable,
ablock |
| ablock | ablock | sort,
|
| ablock0 | ablock-store | variable,
ablock |
| ablock1 | ablock-store | variable,
ablock |
| ablock2 | ablock-store | variable,
ablock |
| abs-failed | abs-node | predicate,
buffer |
| abs-gstore | persistence-base | predicate,
avolume × lp-array × group-store × nat-set |
| abs-istore | persistence-base | predicate,
avolume × lp-array × index-store |
| abs-leb | encoding-index-node | predicate,
aleb × index-block × lprops |
| abs-leb | encoding-group-node | predicate,
aleb × group-block × lprops |
| abs-leb | abs-leb | predicate,
aleb × ablock × lprops |
| abs-node | encoding-index-node | predicate,
buffer × index-node |
| abs-node | encoding-group-node | predicate,
buffer × group-node |
| abs-node | abs-node | predicate,
buffer × elem |
| abs-nodes | encoding-index-node | predicate,
buffer × nat × index-node-list × laddress-list × bool |
| abs-nodes | encoding-index-node | predicate,
buffer × index-node-list × laddress-list × bool |
| abs-nodes | encoding-group-node | predicate,
buffer × nat × group-node-list × laddress-list × bool |
| abs-nodes | encoding-group-node | predicate,
buffer × group-node-list × laddress-list × bool |
| abs-nodes | abs-list | predicate,
buffer × nat × list × laddress-list × bool |
| abs-nodes | abs-list | predicate,
buffer × list × laddress-list × bool |
| abs-padding | abs-node | predicate,
buffer |
| address | address-data | sort,
|
| address | address | sort,
|
| address-list | address-list-set | sort,
|
| address-set | address-list-set | sort,
|
| address-set | address-store | sort,
|
| address-store | address-store | sort,
|
| addresselemf | address-store | variable,
address × elem → elem |
| addressgf | group-store | variable,
address × group-node → group-node |
| addressif | index-store | variable,
address × index-node → index-node |
| adr | address-data | variable,
address |
| adr | address | variable,
address |
| adr0 | address | variable,
address |
| adr1 | address | variable,
address |
| adr1 | address-store | variable,
address |
| adr2 | address | variable,
address |
| adr2 | address-store | variable,
address |
| adr3 | address | variable,
address |
| adr4 | address | variable,
address |
| adr5 | address | variable,
address |
| aleb | aleb | variable,
aleb |
| aleb | aleb | sort,
|
| aleb0 | avolume | variable,
aleb |
| aleb1 | avolume | variable,
aleb |
| align↑ | align | function,
nat × nat → nat |
| align↓ | align | function,
nat × nat → nat |
| apersistence_add_gnds# | apersistence-asm | procedure,
group-node-list × address × index-store × index-store × nat-set ×
group-store × nat-list × nat × nat-set
: address-list × group-store × persistence-state × bool
: error |
| apersistence_add_ind# | apersistence-asm | procedure,
index-node × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set
: address × index-store × persistence-state × bool
: error |
| apersistence_allocate_gnd# | apersistence-asm | procedure,
address × index-store × index-store × group-store × nat × nat-set ×
bool
: nat-set × group-store × nat-list × persistence-state
: error |
| apersistence_allocate_ind# | apersistence-asm | procedure,
address × index-store × nat-set × group-store × group-store × nat-list ×
nat × nat-set × bool
: index-store × persistence-state
: error |
| apersistence_commit# | apersistence-asm | procedure,
address × nat × bool
: nat-set × index-store × nat-set × group-store × address ×
index-store × group-store × nat-list × nat × nat-set
: persistence-state × error |
| apersistence_deallocate_gnd# | apersistence-asm | procedure,
nat × address × index-store × index-store × group-store × nat-list ×
nat × nat-set × persistence-state × bool
: nat-set × group-store
: error |
| apersistence_format# | apersistence-asm | procedure,
nat × nat × nat
:
: address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool ×
error |
| apersistence_get_block_free_size# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| apersistence_get_gblock_refsize# | apersistence-asm | procedure,
nat × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| apersistence_get_gc_block# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: nat
: error |
| apersistence_get_iblock_refsize# | apersistence-asm | procedure,
nat × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| apersistence_get_leb_size# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| apersistence_is_log_empty# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool |
| apersistence_is_readonly# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool |
| apersistence_read_gblock_nodes# | apersistence-asm | procedure,
nat × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: address-list × group-node-list
: error |
| apersistence_read_gnd# | apersistence-asm | procedure,
address × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: group-node
: error |
| apersistence_read_ind# | apersistence-asm | procedure,
address × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: index-node
: error |
| apersistence_recover# | apersistence-asm | procedure,
: address × nat × nat-list × nat-set × address × nat-list × nat ×
nat-set × index-store × index-store × nat-set × group-store ×
group-store
: persistence-state × bool × error |
| apersistence_requires_commit# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool |
| apersistence_set_gblock_refsize# | apersistence-asm | procedure,
nat × nat × address × index-store × index-store × nat-set ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: group-store |
| apersistence_set_iblock_refsize# | apersistence-asm | procedure,
nat × nat × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: index-store |
| apersistence_sync# | apersistence-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set
: persistence-state × bool
: error |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| as | address-list-set | variable,
address-set |
| as | address-store | variable,
address-set |
| as0 | address-list-set | variable,
address-set |
| as0 | address-store | variable,
address-set |
| as1 | address-list-set | variable,
address-set |
| as1 | address-store | variable,
address-set |
| as2 | address-list-set | variable,
address-set |
| as2 | address-store | variable,
address-set |
| ast | address-store | variable,
address-store |
| ast0 | address-store | variable,
address-store |
| ast1 | address-store | variable,
address-store |
| ast2 | address-store | variable,
address-store |
| avol | avolume | variable,
avolume |
| avol-cleanup-lpt-unchanged | persistence-base | predicate,
avolume × avolume × lp-array |
| avol-replay-lpt-unchanged | persistence-base | predicate,
avolume × avolume × lp-array × nat-list |
| avol0 | avolume | variable,
avolume |
| avol1 | avolume | variable,
avolume |
| avol2 | avolume | variable,
avolume |
| avolume | avolume | sort,
|
| awbuf-inv | awbuf-inv | predicate,
avolume × bufleb |
| awbuf_add_log_leb# | awbuf-asm | procedure,
nat × nat × address × nat × avolume × lp-array × nat-set × bool
: nat-list × bufleb
: error |
| awbuf_commit# | awbuf-asm | procedure,
lp-array × address × nat × avolume × bufleb
: nat-set × address × nat × nat-list × lp-array × nat-set × bool
: error |
| awbuf_destroy_buf# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bool
: bufleb
: error |
| awbuf_enter_readonly# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb
:
: bool |
| awbuf_format# | awbuf-asm | procedure,
nat × nat × lp-array × address × nat
:
: address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool × error |
| awbuf_get_buf# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bufleb |
| awbuf_get_leb_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_page_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_volume_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_is_readonly# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| awbuf_move_buf# | awbuf-asm | procedure,
nat × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bool
: bufleb
: error |
| awbuf_read_buf# | awbuf-asm | procedure,
nat × nat × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
: buffer
: error |
| awbuf_recover# | awbuf-asm | procedure,
: address × nat × nat-set × nat-list × lp-array × address × nat ×
nat-list × lp-array × nat-set × avolume
: bufleb × bool × error |
| awbuf_remap# | awbuf-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume
: error |
| awbuf_requires_commit# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| awbuf_unmap# | awbuf-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume |
| awbuf_write_buf# | awbuf-asm | procedure,
nat × buffer × address × nat × nat-list × lp-array × nat-set × bufleb
: avolume × bool
: error |
| ax | address-list-set | variable,
address-list |
| ax0 | address-list-set | variable,
address-list |
| ax1 | address-list-set | variable,
address-list |
| ay | address-list-set | variable,
address-list |
| az | address-list-set | variable,
address-list |
| b | elem | variable,
elem |
| bh | bin-min-heap | variable,
binheap |
| bh0 | bin-min-heap | variable,
binheap |
| bin-heap | bin-min-heap | function,
key-array × nat → binheap |
| bin-heap-inv | bin-min-heap-prepost | predicate,
binheap × array |
| bin-heap-inv | gc-heap-base | predicate,
binheap × lp-array |
| bin_min_heap_bubble_down# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_bubble_down# | gc-heap-base | procedure,
nat : binheap × lp-array |
| bin_min_heap_bubble_up# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_bubble_up# | gc-heap-base | procedure,
nat : binheap × lp-array |
| bin_min_heap_empty# | bin-min-heap-ops | procedure,
: binheap |
| bin_min_heap_extract_min# | bin-min-heap-ops | procedure,
: binheap × array × nat |
| bin_min_heap_extract_min# | gc-heap-base | procedure,
: binheap × lp-array × nat |
| bin_min_heap_get_min# | bin-min-heap-ops | procedure,
binheap : nat |
| bin_min_heap_insert# | bin-min-heap-ops | procedure,
keyindex : binheap × array |
| bin_min_heap_insert# | gc-heap-base | procedure,
keyindex : binheap × lp-array |
| bin_min_heap_is_empty# | bin-min-heap-ops | procedure,
binheap : bool |
| bin_min_heap_next_2pot | bin-min-heap-ops | procedure,
nat : nat |
| bin_min_heap_remove# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_remove# | gc-heap-base | procedure,
nat : binheap × lp-array |
| bin_min_heap_resize# | bin-min-heap-ops | procedure,
nat : binheap |
| bin_min_heap_update# | bin-min-heap-ops | procedure,
nat × key : binheap × array |
| bin_min_heap_update# | gc-heap-base | procedure,
nat × nat : binheap × lp-array |
| binheap | bin-min-heap | sort,
|
| bleb | bufleb | variable,
bufleb |
| boolvar | node-header | variable,
bool |
| boolvar | gc-heap-base | variable,
bool |
| boolvar | indexnode | variable,
bool |
| boolvar | node | variable,
bool |
| boolvar0 | node-header | variable,
bool |
| boolvar0 | gc-heap-base | variable,
bool |
| boolvar0 | indexnode | variable,
bool |
| boolvar0 | node | variable,
bool |
| boolvar1 | encoding-node-header | variable,
bool |
| boolvar1 | gc-heap-base | variable,
bool |
| boolvar1 | groupnode | variable,
bool |
| boolvar2 | groupnode | variable,
bool |
| br | branch | variable,
branch |
| br0 | branch-array | variable,
branch |
| br1 | branch-array | variable,
branch |
| branch | branch | sort,
|
| branch-array | branch-array | sort,
|
| brar | branch-array | variable,
branch-array |
| brar0 | branch-array | variable,
branch-array |
| brar1 | branch-array | variable,
branch-array |
| brar2 | branch-array | variable,
branch-array |
| bubble-down-inv | bin-min-heap-prepost | predicate,
nat × binheap × array × binheap × array |
| bubble-down-inv | gc-heap-base | predicate,
nat × binheap × lp-array × binheap × lp-array |
| bubble-up-inv | bin-min-heap-prepost | predicate,
nat × binheap × array × binheap × array |
| bubble-up-inv | gc-heap-base | predicate,
nat × binheap × lp-array × binheap × lp-array |
| buf | buffer | variable,
buffer |
| buf-ro-rw-mode | persistence-base | predicate,
bool × bufleb × lp-array × avolume |
| buf0 | buffer | variable,
buffer |
| buf1 | buffer | variable,
buffer |
| buf2 | buffer | variable,
buffer |
| buffer | buffer | sort,
|
| buffered | bufleb | function,
nat → bufleb |
| bufleb | bufleb | sort,
|
| bufs-log-only | persistence-base | predicate,
bufleb × nat-list × lp-array |
| butlastn | encoding-index-node | partial function,
nat × index-node-list → index-node-list |
| butlastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| butlastn | encoding-group-node | partial function,
nat × group-node-list → group-node-list |
| butlastn | list-last | partial function,
nat × list → list |
| butlastn | address-list-set | partial function,
nat × address-list → address-list |
| butlastn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| butlastn | group-store | partial function,
nat × group-node-list → group-node-list |
| butlastn | index-store | partial function,
nat × index-node-list → index-node-list |
| butlastn | string | partial function,
nat × string → string |
| c | elem | variable,
elem |
| char | char | variable,
char |
| char | char | sort,
|
| char0 | char | variable,
char |
| char1 | char | variable,
char |
| char2 | char | variable,
char |
| cleanup-lpt | persistence-base | function,
lp-array × nat → lp-array |
| cleanup-lpt | persistence-base | function,
lp-array → lp-array |
| cmp | avolume | partial predicate,
avolume × aleb × nat × nat |
| cmp | avolume | partial predicate,
avolume × nat × avolume × nat × nat |
| cmp | buffer | partial predicate,
buffer × data × nat × nat |
| cmp | buffer | partial predicate,
buffer × nat × buffer × nat × nat |
| cmp | array-copy | partial predicate,
array × elem × nat × nat |
| cmp | array-copy | partial predicate,
array × nat × array × nat × nat |
| cmp | lp-array | partial predicate,
lp-array × lprops × nat × nat |
| cmp | lp-array | partial predicate,
lp-array × nat × lp-array × nat × nat |
| cmp | key-index-array | partial predicate,
key-array × keyindex × nat × nat |
| cmp | key-index-array | partial predicate,
key-array × nat × key-array × nat × nat |
| cmp | index-array-base | partial predicate,
array × elem-index × nat × nat |
| cmp | gc-heap-base | partial predicate,
lp-array × lprops × nat × nat |
| cmp | gc-heap-base | partial predicate,
lp-array × nat × lp-array × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × branch × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × nat × branch-array × nat × nat |
| copy | avolume | partial function,
avolume × nat × avolume × nat × nat → avolume |
| copy | buffer | partial function,
buffer × nat × buffer × nat × nat → buffer |
| copy | array-copy | partial function,
array × nat × array × nat × nat → array |
| copy | lp-array | partial function,
lp-array × nat × lp-array × nat × nat → lp-array |
| copy | key-index-array | partial function,
key-array × nat × key-array × nat × nat → key-array |
| copy | gc-heap-base | partial function,
lp-array × nat × lp-array × nat × nat → lp-array |
| copy | branch-array | partial function,
branch-array × nat × branch-array × nat × nat → branch-array |
| crash | apersistence-base | function,
group-store × group-store × nat-set × nat-list → group-store |
| crash | apersistence-base | function,
index-store × index-store → index-store |
| crash-logblock | apersistence-base | function,
group-block × nat → group-block |
| d | data | variable,
data |
| d0 | data | variable,
data |
| d1 | data | variable,
data |
| d2 | data | variable,
data |
| data | data | sort,
|
| dataf | store-map | variable,
data → data |
| dataf | ablock-store | variable,
ablock → ablock |
| datakey | key | function,
nat × nat → key |
| datanode | node | function,
key × buffer → node |
| debug# | debug | procedure,
string : |
| decode# | encoding | procedure,
nat × buffer : elem × nat : error |
| decode_group_node# | encoding-group-node | procedure,
nat × nat × buffer : group-node : error |
| decode_group_node_headerless# | encoding-group-node | procedure,
nat × buffer : group-node × nat : error |
| decode_header# | encoding-node-header | procedure,
nat × buffer : node-header : error |
| decode_header_empty# | encoding-node-header | procedure,
nat × buffer : node-header × nat : error |
| decode_index_node# | encoding-index-node | procedure,
nat × nat × buffer : index-node : error |
| decode_index_node_headerless# | encoding-index-node | procedure,
nat × buffer : index-node × nat : error |
| decode_node# | encoding-node-base | procedure,
nat × nat × buffer : elem : error |
| decode_node_headerless# | encoding-node-headerless | procedure,
nat × buffer : elem × nat : error |
| decode_nonempty# | encoding-fixed-size-nonempty | procedure,
nat × buffer : elem : error |
| dentrykey | key | function,
nat × string → key |
| dentrynode | node | function,
key × nat → node |
| disj | encoding-index-node | predicate,
index-node-list × index-node-list |
| disj | nat-list-set | predicate,
nat-list × nat-list |
| disj | encoding-group-node | predicate,
group-node-list × group-node-list |
| disj | list-dup | predicate,
list × list |
| disj | address-list-set | predicate,
address-list × address-list |
| disj | laddress-list | predicate,
laddress-list × laddress-list |
| disj | group-store | predicate,
group-node-list × group-node-list |
| disj | index-store | predicate,
index-node-list × index-node-list |
| disj | string | predicate,
string × string |
| dom | store+set | function,
store → set |
| dom | nat-store | function,
store → nat-set |
| dom | group-store | function,
group-address-store → address-set |
| dom | group-store | function,
group-store → nat-set |
| dom | index-store | function,
index-address-store → address-set |
| dom | index-store | function,
index-store → nat-set |
| dom | address-store | function,
address-store → address-set |
| dropn | encoding-index-node | function,
nat × index-node-list → index-node-list |
| dropn | nat-list-set | function,
nat × nat-list → nat-list |
| dropn | encoding-group-node | function,
nat × group-node-list → group-node-list |
| dropn | address-list-set | function,
nat × address-list → address-list |
| dropn | laddress-list | function,
nat × laddress-list → laddress-list |
| dropn | list-prefixn | function,
nat × list → list |
| dropn | group-store | function,
nat × group-node-list → group-node-list |
| dropn | index-store | function,
nat × index-node-list → index-node-list |
| dups | encoding-index-node | predicate,
index-node-list |
| dups | nat-list-set | predicate,
nat-list |
| dups | encoding-group-node | predicate,
group-node-list |
| dups | list-dup | predicate,
list |
| dups | address-list-set | predicate,
address-list |
| dups | laddress-list | predicate,
laddress-list |
| dups | group-store | predicate,
group-node-list |
| dups | index-store | predicate,
index-node-list |
| dups | string | predicate,
string |
| ebm-vol-inv | ebm-vol-inv | predicate,
avolume |
| ei | elem-index | variable,
elem-index |
| ei0 | index-array-base | variable,
elem-index |
| ei1 | index-array-base | variable,
elem-index |
| elem | elem | sort,
|
| elem-index | elem-index | sort,
|
| elemdataf | store-map | variable,
elem × data → data |
| elemdataf | nat-store | variable,
nat × data → data |
| elemdataf | ablock-store | variable,
nat × ablock → ablock |
| elemf | address-store | variable,
elem → elem |
| elemindex | elem-index | function,
elem × nat → elem-index |
| elems | apersistence-base | function,
nat-list → nat-set |
| empty | avolume | constant,
aleb |
| empty | buffer | constant,
data |
| empty | array-splice | constant,
elem |
| empty? | gc-heap-rename | variable,
bool |
| emptyleb | eraseblock | constant,
buffer |
| emptypage | eraseblock | constant,
buffer |
| emptypeb | eraseblock | constant,
buffer |
| encode# | encoding | procedure,
elem × nat : buffer × nat : error |
| encode_group_node# | encoding-group-node | procedure,
group-node × nat : nat × buffer : error |
| encode_group_node_headerless# | encoding-group-node | procedure,
group-node × nat : buffer × nat : error |
| encode_header# | encoding-node-header | procedure,
node-header × nat : buffer : error |
| encode_header_empty# | encoding-node-header | procedure,
node-header × nat : buffer × nat : error |
| encode_index_node# | encoding-index-node | procedure,
index-node × nat : nat × buffer : error |
| encode_index_node_headerless# | encoding-index-node | procedure,
index-node × nat : buffer × nat : error |
| encode_node# | encoding-node-base | procedure,
elem × nat : nat × buffer : error |
| encode_node_headerless# | encoding-node-headerless | procedure,
elem × nat : buffer × nat : error |
| encode_nonempty# | encoding-fixed-size-nonempty | procedure,
elem × nat : buffer : error |
| encoding-size | encoding-node-header | function,
node-header → nat |
| encoding-size | encoding | function,
elem → nat |
| err | error | variable,
error |
| err0 | error | variable,
error |
| err1 | error | variable,
error |
| error | error | sort,
|
| f | array-indices | variable,
elem → elem |
| fail# | error-class | procedure,
: : error |
| fail_or_success# | error-class | procedure,
: : error |
| fill | avolume | partial function,
avolume × aleb × nat × nat → avolume |
| fill | avolume | function,
avolume × aleb → avolume |
| fill | buffer | partial function,
buffer × data × nat × nat → buffer |
| fill | buffer | function,
buffer × data → buffer |
| fill | array-copy | partial function,
array × elem × nat × nat → array |
| fill | array-copy | function,
array × elem → array |
| fill | lp-array | partial function,
lp-array × lprops × nat × nat → lp-array |
| fill | lp-array | function,
lp-array × lprops → lp-array |
| fill | key-index-array | partial function,
key-array × keyindex × nat × nat → key-array |
| fill | key-index-array | function,
key-array × keyindex → key-array |
| fill | index-array-base | partial function,
array × elem-index × nat × nat → array |
| fill | index-array-base | function,
array × elem-index → array |
| fill | gc-heap-base | partial function,
lp-array × lprops × nat × nat → lp-array |
| fill | gc-heap-base | function,
lp-array × lprops → lp-array |
| fill | branch-array | partial function,
branch-array × branch × nat × nat → branch-array |
| fill | branch-array | function,
branch-array × branch → branch-array |
| fillfirst | encoding-index-node | function,
nat × index-node × index-node-list → index-node-list |
| fillfirst | nat-list-set | function,
nat × nat × nat-list → nat-list |
| fillfirst | encoding-group-node | function,
nat × group-node × group-node-list → group-node-list |
| fillfirst | list-last | function,
nat × elem × list → list |
| fillfirst | address-list-set | function,
nat × address × address-list → address-list |
| fillfirst | laddress-list | function,
nat × laddress × laddress-list → laddress-list |
| fillfirst | group-store | function,
nat × group-node × group-node-list → group-node-list |
| fillfirst | index-store | function,
nat × index-node × index-node-list → index-node-list |
| fillfirst | string | function,
nat × char × string → string |
| firstn | encoding-index-node | partial function,
nat × index-node-list → index-node-list |
| firstn | nat-list-set | partial function,
nat × nat-list → nat-list |
| firstn | list-del | partial function,
nat × list → list |
| firstn | encoding-group-node | partial function,
nat × group-node-list → group-node-list |
| firstn | address-list-set | partial function,
nat × address-list → address-list |
| firstn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| firstn | group-store | partial function,
nat × group-node-list → group-node-list |
| firstn | index-store | partial function,
nat × index-node-list → index-node-list |
| firstn | string | partial function,
nat × string → string |
| flash-lpt-cons | persistence-base | predicate,
lp-array × index-store × group-store |
| fn | array-indices | variable,
nat → nat |
| freelist | persistence-base | variable,
nat-list |
| freelist-cons | persistence-base | predicate,
lp-array × nat-list |
| frome | encoding-index-node | function,
index-node-list × index-node → index-node-list |
| frome | nat-list-set | function,
nat-list × nat → nat-list |
| frome | list-del | function,
list × elem → list |
| frome | encoding-group-node | function,
group-node-list × group-node → group-node-list |
| frome | address-list-set | function,
address-list × address → address-list |
| frome | laddress-list | function,
laddress-list × laddress → laddress-list |
| frome | group-store | function,
group-node-list × group-node → group-node-list |
| frome | index-store | function,
index-node-list × index-node → index-node-list |
| frome | string | function,
string × char → string |
| gast | group-store | variable,
group-address-store |
| gast0 | group-store | variable,
group-address-store |
| gast1 | group-store | variable,
group-address-store |
| gast2 | group-store | variable,
group-address-store |
| gblock | encoding-group-node | variable,
group-block |
| gblock | group-store | variable,
group-block |
| gblock0 | group-store | variable,
group-block |
| gblock1 | group-store | variable,
group-block |
| gblock2 | group-store | variable,
group-block |
| gc-heap | persistence-base | function,
lp-array × nat-list → gc-heap-set |
| gc-heap | persistence-base | function,
lp-array × nat-list × nat → gc-heap-set |
| gc-heap-set | gc-heap-rename | sort,
|
| gc_heap_empty# | gc-heap-rename | procedure,
: binheap |
| gc_heap_extract_min# | gc-heap-rename | procedure,
: binheap × lp-array × nat |
| gc_heap_get_min# | gc-heap-rename | procedure,
binheap : nat |
| gc_heap_insert# | gc-heap-rename | procedure,
keyindex : binheap × lp-array |
| gc_heap_is_empty# | gc-heap-rename | procedure,
binheap : bool |
| gc_heap_remove# | gc-heap-rename | procedure,
nat : binheap × lp-array |
| gc_heap_update# | gc-heap-rename | procedure,
nat × nat : binheap × lp-array |
| gch | persistence-base | variable,
binheap |
| gchs | gc-heap-rename | variable,
gc-heap-set |
| gchs0 | gc-heap-rename | variable,
gc-heap-set |
| gchs1 | gc-heap-rename | variable,
gc-heap-set |
| gchs2 | gc-heap-rename | variable,
gc-heap-set |
| gdataf | group-store | variable,
group-block → group-block |
| gelemdataf | group-store | variable,
nat × group-block → group-block |
| gelemf | group-store | variable,
group-node → group-node |
| ginval | apersistence-base | variable,
nat-set |
| gnd | groupnode | variable,
group-node |
| gnd0 | encoding-group-node | variable,
group-node |
| gnd0 | group-store | variable,
group-node |
| gnd1 | encoding-group-node | variable,
group-node |
| gnd1 | group-store | variable,
group-node |
| gnd2 | encoding-group-node | variable,
group-node |
| gnd2 | group-store | variable,
group-node |
| gnd3 | encoding-group-node | variable,
group-node |
| gnd4 | encoding-group-node | variable,
group-node |
| gnd5 | encoding-group-node | variable,
group-node |
| gndx | encoding-group-node | variable,
group-node-list |
| gndx | group-store | variable,
group-node-list |
| gndx0 | encoding-group-node | variable,
group-node-list |
| gndx0 | group-store | variable,
group-node-list |
| gndx1 | encoding-group-node | variable,
group-node-list |
| gndx1 | group-store | variable,
group-node-list |
| gndx2 | group-store | variable,
group-node-list |
| gndx3 | encoding-group-node | variable,
group-node-list |
| gndx3 | group-store | variable,
group-node-list |
| gndx7 | encoding-group-node | variable,
group-node-list |
| group-address-store | group-store | sort,
|
| group-block | encoding-group-node | sort,
|
| group-block | group-store | sort,
|
| group-node | groupnode | sort,
|
| group-node-list | encoding-group-node | sort,
|
| group-node-list | group-store | sort,
|
| group-node-size-headerless | encoding-group-node | function,
group-node → nat |
| group-store | group-store | sort,
|
| groupblock | encoding-group-node | function,
group-node-list × laddress-list × nat → group-block |
| groupblock | group-store | function,
group-node-list × laddress-list × nat → group-block |
| gstore | group-store | variable,
group-store |
| gstore0 | group-store | variable,
group-store |
| gstore1 | group-store | variable,
group-store |
| gstore2 | group-store | variable,
group-store |
| heap-order | bin-min-heap-inv | predicate,
key-array × nat |
| iast | index-store | variable,
index-address-store |
| iast0 | index-store | variable,
index-address-store |
| iast1 | index-store | variable,
index-address-store |
| iast2 | index-store | variable,
index-address-store |
| iblock | encoding-index-node | variable,
index-block |
| iblock | index-store | variable,
index-block |
| iblock0 | index-store | variable,
index-block |
| iblock1 | index-store | variable,
index-block |
| iblock2 | index-store | variable,
index-block |
| id-idx | index-array | predicate,
array × array |
| id-idx | gc-heap-base | predicate,
lp-array × lp-array |
| idataf | index-store | variable,
index-block → index-block |
| idrange | avolume | partial predicate,
avolume × nat × nat |
| idrange | buffer | partial predicate,
buffer × nat × nat |
| idrange | array-copy | partial predicate,
array × nat × nat |
| idrange | lp-array | partial predicate,
lp-array × nat × nat |
| idrange | key-index-array | partial predicate,
key-array × nat × nat |
| idrange | gc-heap-base | partial predicate,
lp-array × nat × nat |
| idrange | branch-array | partial predicate,
branch-array × nat × nat |
| id○ | avolume | predicate,
avolume × avolume × nat |
| id○ | buffer | predicate,
buffer × buffer × nat |
| id○ | array-copy | predicate,
array × array × nat |
| id○ | lp-array | predicate,
lp-array × lp-array × nat |
| id○ | key-index-array | predicate,
key-array × key-array × nat |
| id○ | gc-heap-base | predicate,
lp-array × lp-array × nat |
| id○ | branch-array | predicate,
branch-array × branch-array × nat |
| ielemdataf | index-store | variable,
nat × index-block → index-block |
| ielemf | index-store | variable,
index-node → index-node |
| ind | indexnode | variable,
index-node |
| ind0 | encoding-index-node | variable,
index-node |
| ind0 | index-store | variable,
index-node |
| ind1 | encoding-index-node | variable,
index-node |
| ind1 | index-store | variable,
index-node |
| ind2 | encoding-index-node | variable,
index-node |
| ind2 | index-store | variable,
index-node |
| ind3 | encoding-index-node | variable,
index-node |
| ind4 | encoding-index-node | variable,
index-node |
| ind5 | encoding-index-node | variable,
index-node |
| index | persistence-state | function,
nat → persistence-state |
| index-address-store | index-store | sort,
|
| index-block | encoding-index-node | sort,
|
| index-block | index-store | sort,
|
| index-node | indexnode | sort,
|
| index-node-list | encoding-index-node | sort,
|
| index-node-list | index-store | sort,
|
| index-node-size-headerless | encoding-index-node | function,
index-node → nat |
| index-store | index-store | sort,
|
| indexblock | encoding-index-node | function,
index-node-list × laddress-list × nat → index-block |
| indexblock | index-store | function,
index-node-list × laddress-list × nat → index-block |
| indexnode | indexnode | function,
branch-array × bool × nat → index-node |
| indx | encoding-index-node | variable,
index-node-list |
| indx | index-store | variable,
index-node-list |
| indx0 | encoding-index-node | variable,
index-node-list |
| indx0 | index-store | variable,
index-node-list |
| indx1 | encoding-index-node | variable,
index-node-list |
| indx1 | index-store | variable,
index-node-list |
| indx2 | index-store | variable,
index-node-list |
| indx3 | encoding-index-node | variable,
index-node-list |
| indx3 | index-store | variable,
index-node-list |
| indx7 | encoding-index-node | variable,
index-node-list |
| inodekey | key | function,
nat → key |
| inodenode | node | function,
key × metadata × bool × nat × nat × nat → node |
| inv | ablock-store-inv | predicate,
store |
| inv | ablock-store-inv | predicate,
ablock |
| inv | group-store | predicate,
group-store |
| inv | group-store | predicate,
group-block |
| inv | index-store | predicate,
index-store |
| inv | index-store | predicate,
index-block |
| inv | apersistence-base | predicate,
nat-list × group-store × group-store × nat-set × index-store × index-store |
| inv-flashsize | ablock-store-inv | predicate,
list × laddress-list |
| inv-flashsize | group-store | predicate,
group-node-list × laddress-list |
| inv-flashsize | index-store | predicate,
index-node-list × laddress-list |
| inv-index | apersistence-base | predicate,
index-store × index-store |
| inv-journal | apersistence-base | predicate,
nat-list × group-store × group-store × nat-set |
| inv-state | apersistence-base | predicate,
persistence-state × nat-list × group-store × index-store × bool |
| is-aligned | align | predicate,
nat × nat |
| is-encoded | encoding-index-node | predicate,
index-node × buffer |
| is-encoded | encoding-group-node | predicate,
group-node × buffer |
| is-encoded | encoding-node-header | predicate,
node-header × buffer |
| is-encoded | encoding | predicate,
elem × buffer |
| is-encoded-empty | encoding-node-header | predicate,
node-header × buffer |
| is-encoded-nonempty | encoding-fixed-size-nonempty | predicate,
elem × buffer |
| is-garbage | encoding | predicate,
buffer |
| is-garbage-header | encoding-node-header | predicate,
buffer |
| is-garbage-nonempty | encoding-fixed-size-nonempty | predicate,
buffer |
| is-garbage-rnode-empty | encoding-node-header | predicate,
buffer |
| isbuf | awbuf-asm | variable,
bool |
| isempty | eraseblock | predicate,
buffer × nat × nat |
| isempty | eraseblock | predicate,
buffer |
| isempty | bin-min-heap-ops | variable,
bool |
| ispad | encoding-node-base | variable,
bool |
| istore | index-store | variable,
index-store |
| istore0 | index-store | variable,
index-store |
| istore1 | index-store | variable,
index-store |
| istore2 | index-store | variable,
index-store |
| isvalidtrailer | node-header-size | predicate,
buffer |
| journal | persistence-state | function,
nat → persistence-state |
| kar | key-index-array | variable,
key-array |
| kar0 | key-index-array | variable,
key-array |
| kar1 | key-index-array | variable,
key-array |
| kar2 | key-index-array | variable,
key-array |
| key | binheap-key | variable,
key |
| key | binheap-key | sort,
|
| key | gc-heap-base | variable,
nat |
| key | key | variable,
key |
| key | key | sort,
|
| key-array | key-index-array | sort,
|
| key-index | key-index | function,
key × nat → keyindex |
| key-index | gc-heap-base | function,
nat × nat → keyindex |
| key0 | binheap-key | variable,
key |
| key0 | gc-heap-base | variable,
nat |
| key0 | branch | variable,
key |
| key0 | node | variable,
key |
| key1 | binheap-key | variable,
key |
| key1 | gc-heap-base | variable,
nat |
| keyindex | key-index | sort,
|
| keyset | bin-min-heap-inv | function,
key-array × nat → set |
| keyset | bin-min-heap-prepost | function,
binheap → set |
| keyset | gc-heap-rename | function,
binheap → gc-heap-set |
| keyset | gc-heap-rename | function,
key-array × nat → gc-heap-set |
| ki | key-index | variable,
keyindex |
| ki0 | key-index-array | variable,
keyindex |
| ki0 | keyindex-set | variable,
keyindex |
| ki1 | key-index-array | variable,
keyindex |
| ki1 | keyindex-set | variable,
keyindex |
| laddress | laddress | sort,
|
| laddress-list | laddress-list | sort,
|
| ladr | laddress | variable,
laddress |
| ladr0 | laddress-list | variable,
laddress |
| ladr1 | laddress-list | variable,
laddress |
| ladr2 | laddress-list | variable,
laddress |
| lastn | encoding-index-node | partial function,
nat × index-node-list → index-node-list |
| lastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| lastn | list-del | partial function,
nat × list → list |
| lastn | encoding-group-node | partial function,
nat × group-node-list → group-node-list |
| lastn | address-list-set | partial function,
nat × address-list → address-list |
| lastn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| lastn | group-store | partial function,
nat × group-node-list → group-node-list |
| lastn | index-store | partial function,
nat × index-node-list → index-node-list |
| lastn | string | partial function,
nat × string → string |
| lax | laddress-list | variable,
laddress-list |
| lax0 | laddress-list | variable,
laddress-list |
| lax1 | laddress-list | variable,
laddress-list |
| lax2 | laddress-list | variable,
laddress-list |
| lax3 | laddress-list | variable,
laddress-list |
| list | list-data | sort,
|
| log | persistence-asm | variable,
nat-list |
| log | nat-pot | partial function,
nat × nat → nat |
| log-group-block | persistence-base | predicate,
nat-list × lp-array |
| log2 | nat-pot | partial function,
nat → nat |
| logarithm | gc-heap-rename | partial function,
nat × nat → nat |
| logarithm2 | gc-heap-rename | partial function,
nat → nat |
| lp | lprops | variable,
lprops |
| lp-array | lp-array | sort,
|
| lp-array | gc-heap-base | sort,
|
| lp0 | lprops | variable,
lprops |
| lp1 | lp-array | variable,
lprops |
| lp2 | gc-heap-base | variable,
lprops |
| lp3 | gc-heap-base | variable,
lprops |
| lpf | lprops | variable,
lpropflags |
| lpf0 | lprops | variable,
lpropflags |
| lpf1 | gc-heap-base | variable,
lpropflags |
| lpf2 | gc-heap-base | variable,
lpropflags |
| lpropflags | lprops | sort,
|
| lprops | lprops | sort,
|
| lpt | lp-array | variable,
lp-array |
| lpt | gc-heap-base | variable,
lp-array |
| lpt-free-unref | persistence-base | predicate,
lp-array |
| lpt-leb-size | persistence-base | predicate,
lp-array |
| lpt-ram-flash | persistence-base | predicate,
lp-array × lp-array × nat-list |
| lpt0 | lp-array | variable,
lp-array |
| lpt0 | gc-heap-base | variable,
lp-array |
| lpt1 | lp-array | variable,
lp-array |
| lpt1 | gc-heap-base | variable,
lp-array |
| lpt2 | lp-array | variable,
lp-array |
| lpt2 | gc-heap-base | variable,
lp-array |
| lptfun | lp-array | variable,
lprops → lprops |
| m | nat-basic | variable,
nat |
| m0 | array-copy | variable,
nat |
| m0 | lprops | variable,
nat |
| m0 | node-header | variable,
nat |
| m0 | address-data | variable,
nat |
| m0 | laddress | variable,
nat |
| m0 | nat-pot | variable,
nat |
| m0 | key-index | variable,
nat |
| m0 | elem-index | variable,
nat |
| m0 | key | variable,
nat |
| m0 | bufleb | variable,
nat |
| m0 | persistence-state | variable,
nat |
| m1 | lprops | variable,
nat |
| m1 | address-data | variable,
nat |
| m1 | laddress | variable,
nat |
| m1 | bin-min-heap-inv | variable,
nat |
| m1 | key | variable,
nat |
| m2 | lprops | variable,
nat |
| m2 | address-data | variable,
nat |
| m2 | laddress | variable,
nat |
| m2 | key | variable,
nat |
| m3 | lprops | variable,
nat |
| m3 | address-data | variable,
nat |
| m3 | node | variable,
nat |
| m4 | lprops | variable,
nat |
| m4 | address-data | variable,
nat |
| m4 | node | variable,
nat |
| mapped | aleb | function,
buffer → aleb |
| max | min-max | function,
nat × nat → nat |
| maxino | apersistence-base | variable,
nat |
| md | metadata | variable,
metadata |
| md0 | node | variable,
metadata |
| metadata | metadata | sort,
|
| min | min-max | function,
nat × nat → nat |
| minsize | bin-min-heap-ops | variable,
nat |
| mkarray | array | function,
nat → array |
| mkavolume | avolume | function,
nat → avolume |
| mkblock | ablock | function,
list × laddress-list × nat → ablock |
| mkbranch | branch | function,
key × address → branch |
| mkbrarray | branch-array | function,
nat → branch-array |
| mkbuf | buffer | function,
nat → buffer |
| mkemparray | avolume | function,
nat → avolume |
| mkemparray | array-splice | function,
nat → array |
| mkempbuf | buffer | function,
nat → buffer |
| mkentry | branch | function,
key × address → branch |
| mkgnode | groupnode | function,
node × nat × bool × bool → group-node |
| mkkeyarray | key-index-array | function,
nat → key-array |
| mklist | encoding-index-node | function,
index-node × nat → index-node-list |
| mklist | nat-list-set | function,
nat × nat → nat-list |
| mklist | encoding-group-node | function,
group-node × nat → group-node-list |
| mklist | list-last | function,
elem × nat → list |
| mklist | address-list-set | function,
address × nat → address-list |
| mklist | laddress-list | function,
laddress × nat → laddress-list |
| mklist | group-store | function,
group-node × nat → group-node-list |
| mklist | index-store | function,
index-node × nat → index-node-list |
| mklist | string | function,
char × nat → string |
| mklp | lprops | function,
nat × nat × lpropflags × nat → lprops |
| mklparray | lp-array | function,
nat → lp-array |
| mklparray | gc-heap-base | function,
nat → lp-array |
| mkzarray | avolume | function,
nat → avolume |
| mkzarray | array-splice | function,
nat → array |
| mkzbuf | buffer | function,
nat → buffer |
| n | nat-basic | variable,
nat |
| n0 | nat-basic | variable,
nat |
| n1 | nat-basic | variable,
nat |
| n2 | nat-list-set | variable,
nat |
| n2 | nat-set | variable,
nat |
| n2 | gc-heap-base | variable,
nat |
| n2 | nat-store | variable,
nat |
| n3 | nat-list-set | variable,
nat |
| n3 | nat-set | variable,
nat |
| n3 | gc-heap-base | variable,
nat |
| n3 | nat-store | variable,
nat |
| n4 | nat-list-set | variable,
nat |
| n4 | nat-set | variable,
nat |
| n4 | gc-heap-base | variable,
nat |
| n4 | nat-store | variable,
nat |
| n5 | nat-list-set | variable,
nat |
| n5 | gc-heap-base | variable,
nat |
| n6 | gc-heap-base | variable,
nat |
| n7 | gc-heap-base | variable,
nat |
| n8 | gc-heap-base | variable,
nat |
| n9 | gc-heap-base | variable,
nat |
| nat | nat-basic | sort,
|
| nat-list | nat-list-set | sort,
|
| nat-set | nat-list-set | sort,
|
| nat-set | nat-set | sort,
|
| nat-set | nat-store | sort,
|
| natkey | gc-heap-rename | variable,
nat |
| natkey0 | gc-heap-rename | variable,
nat |
| natkey1 | gc-heap-rename | variable,
nat |
| nd | encoding-node-headerless | variable,
elem |
| nd | node | variable,
node |
| nd0 | encoding-node-headerless | variable,
elem |
| nd0 | node | variable,
node |
| nd1 | encoding-node-headerless | variable,
elem |
| nd1 | node | variable,
node |
| nd2 | node | variable,
node |
| nd3 | node | variable,
node |
| ndhd | node-header | variable,
node-header |
| ndhd0 | encoding-node-header | variable,
node-header |
| ndhd1 | encoding-node-header | variable,
node-header |
| no-dups | bin-min-heap-inv | predicate,
key-array × nat |
| no-dups-idx | bin-min-heap-inv | predicate,
key-array × nat |
| nobuffer | bufleb | constant,
bufleb |
| node | node | sort,
|
| node-header | node-header | sort,
|
| node-size-headerless | encoding-node-headerless | function,
elem → nat |
| nodeheader | node-header | function,
nat × bool → node-header |
| nodes | group-store | function,
group-store → group-address-store |
| nodes | index-store | function,
index-store → index-address-store |
| nodes | ablock-nodes | function,
store → address-store |
| ns | nat-list-set | variable,
nat-set |
| ns | nat-set | variable,
nat-set |
| ns | nat-store | variable,
nat-set |
| ns0 | nat-list-set | variable,
nat-set |
| ns0 | nat-set | variable,
nat-set |
| ns0 | nat-store | variable,
nat-set |
| ns1 | nat-list-set | variable,
nat-set |
| ns1 | nat-set | variable,
nat-set |
| ns1 | nat-store | variable,
nat-set |
| ns2 | nat-list-set | variable,
nat-set |
| ns2 | nat-set | variable,
nat-set |
| ns2 | nat-store | variable,
nat-set |
| nx | nat-list-set | variable,
nat-list |
| nx0 | nat-list-set | variable,
nat-list |
| nx1 | nat-list-set | variable,
nat-list |
| ny | nat-list-set | variable,
nat-list |
| nz | nat-list-set | variable,
nat-list |
| persistence-state | persistence-state | sort,
|
| persistence_add_gnds# | persistence-asm | procedure,
group-node-list × nat-list × nat × address × nat × nat-list × lp-array ×
nat-set × bufleb
: address-list × lp-array × avolume × bool
: error |
| persistence_add_ind# | persistence-asm | procedure,
index-node × nat × address × nat × nat-list × lp-array × nat-set ×
bufleb
: address × lp-array × avolume × bool
: error |
| persistence_allocate_gnd# | persistence-asm | procedure,
address × nat × lp-array × nat-set × bool
: nat-list × lp-array × nat-list × nat-list × avolume × bufleb
: error |
| persistence_allocate_ind# | persistence-asm | procedure,
address × nat × nat-list × lp-array × nat-set × bool
: lp-array × nat-list × avolume × bufleb
: error |
| persistence_allocate_leb# | persistence-asm | procedure,
address × nat × nat-list × lp-array × nat-set × bufleb × bool
: nat × lp-array × nat-list × avolume
: error |
| persistence_cleanup_lpt# | persistence-asm | procedure,
address × nat × nat-list × lp-array × nat-set × bufleb × bool
: lp-array × nat-list × binheap × avolume |
| persistence_commit# | persistence-asm | procedure,
address × nat
: nat-set × nat-list × lp-array × nat-list × binheap × address × nat ×
nat-list × avolume × lp-array × nat-set × bufleb × bool
: error |
| persistence_create_freelist# | persistence-asm | procedure,
lp-array : nat-list |
| persistence_create_gcheap# | persistence-asm | procedure,
nat-list : lp-array × binheap |
| persistence_deallocate_gnd# | persistence-asm | procedure,
nat × nat-list × address × nat × nat-list × lp-array × nat-set ×
bufleb × bool
: lp-array × nat-list × binheap × avolume
: error |
| persistence_encode_group_nodes# | persistence-asm | procedure,
group-node-list × nat × nat : : buffer × address-list × error |
| persistence_encode_padding_node# | persistence-asm | procedure,
: buffer : error |
| persistence_format# | persistence-asm | procedure,
nat × nat × nat
: lp-array × nat-list × binheap × address × nat × nat-list × avolume ×
lp-array × nat-set × bufleb × bool × nat-list × nat
: error |
| persistence_gc_heap_add_log# | persistence-asm | procedure,
: nat-list × lp-array × binheap |
| persistence_get_block_free_size# | persistence-asm | procedure,
lp-array × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
:
: nat |
| persistence_get_gblock_refsize# | persistence-asm | procedure,
nat × lp-array : : nat |
| persistence_get_gc_block# | persistence-asm | procedure,
binheap : nat : error |
| persistence_get_iblock_refsize# | persistence-asm | procedure,
nat × lp-array : : nat |
| persistence_get_leb_size# | persistence-asm | procedure,
nat : : nat |
| persistence_is_log_empty# | persistence-asm | procedure,
nat-list : : bool |
| persistence_is_readonly# | persistence-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| persistence_read_gblock_nodes# | persistence-asm | procedure,
nat × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bufleb × bool
: address-list × group-node-list
: error |
| persistence_read_gnd# | persistence-asm | procedure,
address × address × nat × nat-list × avolume × lp-array × nat-set ×
bufleb × bool
: group-node
: error |
| persistence_read_ind# | persistence-asm | procedure,
address × address × nat × nat-list × avolume × lp-array × nat-set ×
bufleb × bool
: index-node
: error |
| persistence_recover# | persistence-asm | procedure,
: address × nat × nat-list × nat-set × nat-list × lp-array × nat-list ×
binheap × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
: error |
| persistence_replay_log# | persistence-asm | procedure,
nat : nat-list × lp-array |
| persistence_replay_lpt# | persistence-asm | procedure,
nat-list × nat × address × nat × nat-list × lp-array × nat-set ×
bufleb × bool
: lp-array × avolume |
| persistence_requires_commit# | persistence-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| persistence_set_gblock_refsize# | persistence-asm | procedure,
nat × nat × nat-list : lp-array × binheap |
| persistence_set_iblock_refsize# | persistence-asm | procedure,
nat × nat : lp-array |
| persistence_sync# | persistence-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set × bufleb
: lp-array × avolume × bool
: error |
| pos | encoding-index-node | function,
index-node × index-node-list → nat |
| pos | nat-list-set | function,
nat × nat-list → nat |
| pos | list-del | function,
elem × list → nat |
| pos | encoding-group-node | function,
group-node × group-node-list → nat |
| pos | address-list-set | function,
address × address-list → nat |
| pos | laddress-list | function,
laddress × laddress-list → nat |
| pos | group-store | function,
group-node × group-node-list → nat |
| pos | index-store | function,
index-node × index-node-list → nat |
| pos | string | function,
char × string → nat |
| prefixn | encoding-index-node | function,
nat × index-node-list → index-node-list |
| prefixn | nat-list-set | function,
nat × nat-list → nat-list |
| prefixn | encoding-group-node | function,
nat × group-node-list → group-node-list |
| prefixn | address-list-set | function,
nat × address-list → address-list |
| prefixn | laddress-list | function,
nat × laddress-list → laddress-list |
| prefixn | list-prefixn | function,
nat × list → list |
| prefixn | group-store | function,
nat × group-node-list → group-node-list |
| prefixn | index-store | function,
nat × index-node-list → index-node-list |
| pstate | persistence-state | variable,
persistence-state |
| range= | avolume | predicate,
avolume × nat × avolume × nat × nat |
| range= | buffer | predicate,
buffer × nat × buffer × nat × nat |
| range= | array-splice | predicate,
array × nat × array × nat × nat |
| read-gblock-inv | persistence-base | predicate,
nat × nat × address-list × group-node-list × address-list × group-node-list × buffer × bool |
| readonly | persistence-state | constant,
persistence-state |
| refsize-cons | ablock-store-refsize-cons | predicate,
store × address-set |
| refsize-cons | group-store | predicate,
group-store × address-set |
| refsize-cons | index-store | predicate,
index-store × address-set |
| remove-refsize0 | ablock-store-inv | function,
store → store |
| remove-refsize0 | group-store | function,
group-store → group-store |
| remove-refsize0 | index-store | function,
index-store → index-store |
| remove-wbufs | persistence-base | function,
nat-set × lp-array → lp-array |
| replay-log | persistence-base | function,
lp-array × nat-list → lp-array |
| replay-lpt | persistence-base | function,
lp-array × nat-list × nat → lp-array |
| resize | avolume | function,
avolume × nat → avolume |
| resize | buffer | function,
buffer × nat → buffer |
| resize | array-splice | function,
array × nat → array |
| restn | encoding-index-node | partial function,
nat × index-node-list → index-node-list |
| restn | nat-list-set | partial function,
nat × nat-list → nat-list |
| restn | list-del | partial function,
nat × list → list |
| restn | encoding-group-node | partial function,
nat × group-node-list → group-node-list |
| restn | address-list-set | partial function,
nat × address-list → address-list |
| restn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| restn | group-store | partial function,
nat × group-node-list → group-node-list |
| restn | index-store | partial function,
nat × index-node-list → index-node-list |
| restn | string | partial function,
nat × string → string |
| rev | encoding-index-node | function,
index-node-list → index-node-list |
| rev | nat-list-set | function,
nat-list → nat-list |
| rev | encoding-group-node | function,
group-node-list → group-node-list |
| rev | list-last | function,
list → list |
| rev | avolume | partial function,
avolume × nat → avolume |
| rev | avolume | function,
avolume → avolume |
| rev | buffer | partial function,
buffer × nat → buffer |
| rev | buffer | function,
buffer → buffer |
| rev | array-copy | partial function,
array × nat → array |
| rev | array-copy | function,
array → array |
| rev | lp-array | partial function,
lp-array × nat → lp-array |
| rev | lp-array | function,
lp-array → lp-array |
| rev | address-list-set | function,
address-list → address-list |
| rev | laddress-list | function,
laddress-list → laddress-list |
| rev | key-index-array | partial function,
key-array × nat → key-array |
| rev | key-index-array | function,
key-array → key-array |
| rev | gc-heap-base | partial function,
lp-array × nat → lp-array |
| rev | gc-heap-base | function,
lp-array → lp-array |
| rev | branch-array | partial function,
branch-array × nat → branch-array |
| rev | branch-array | function,
branch-array → branch-array |
| rev | group-store | function,
group-node-list → group-node-list |
| rev | index-store | function,
index-node-list → index-node-list |
| rev | string | function,
string → string |
| rmdup | encoding-index-node | function,
index-node-list → index-node-list |
| rmdup | nat-list-set | function,
nat-list → nat-list |
| rmdup | encoding-group-node | function,
group-node-list → group-node-list |
| rmdup | list-dup | function,
list → list |
| rmdup | address-list-set | function,
address-list → address-list |
| rmdup | laddress-list | function,
laddress-list → laddress-list |
| rmdup | group-store | function,
group-node-list → group-node-list |
| rmdup | index-store | function,
index-node-list → index-node-list |
| rmdup | string | function,
string → string |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| set | set-basic | sort,
|
| slice | encoding-index-node | function,
nat × nat × index-node-list → index-node-list |
| slice | nat-list-set | function,
nat × nat × nat-list → nat-list |
| slice | encoding-group-node | function,
nat × nat × group-node-list → group-node-list |
| slice | address-list-set | function,
nat × nat × address-list → address-list |
| slice | laddress-list | function,
nat × nat × laddress-list → laddress-list |
| slice | list-prefixn | function,
nat × nat × list → list |
| slice | group-store | function,
nat × nat × group-node-list → group-node-list |
| slice | index-store | function,
nat × nat × index-node-list → index-node-list |
| splice | avolume | function,
avolume × nat × avolume × nat × nat → avolume |
| splice | buffer | function,
buffer × nat × buffer × nat × nat → buffer |
| splice | array-splice | function,
array × nat × array × nat × nat → array |
| st | store | variable,
store |
| st0 | store | variable,
store |
| st1 | store | variable,
store |
| st2 | store | variable,
store |
| store | store | sort,
|
| str | string | variable,
string |
| str0 | string | variable,
string |
| str1 | string | variable,
string |
| str2 | string | variable,
string |
| str3 | string | variable,
string |
| string | string | sort,
|
| subarray | avolume | partial function,
avolume × nat × nat → avolume |
| subarray | buffer | partial function,
buffer × nat × nat → buffer |
| subarray | array-copy | partial function,
array × nat × nat → array |
| subarray | lp-array | partial function,
lp-array × nat × nat → lp-array |
| subarray | key-index-array | partial function,
key-array × nat × nat → key-array |
| subarray | gc-heap-base | partial function,
lp-array × nat × nat → lp-array |
| subarray | branch-array | partial function,
branch-array × nat × nat → branch-array |
| sublist | encoding-index-node | partial function,
nat × nat × index-node-list → index-node-list |
| sublist | nat-list-set | partial function,
nat × nat × nat-list → nat-list |
| sublist | list-del | partial function,
nat × nat × list → list |
| sublist | encoding-group-node | partial function,
nat × nat × group-node-list → group-node-list |
| sublist | address-list-set | partial function,
nat × nat × address-list → address-list |
| sublist | laddress-list | partial function,
nat × nat × laddress-list → laddress-list |
| sublist | group-store | partial function,
nat × nat × group-node-list → group-node-list |
| sublist | index-store | partial function,
nat × nat × index-node-list → index-node-list |
| sublist | string | partial function,
nat × nat × string → string |
| syn | apersistence-base | variable,
bool |
| synced | awbuf-inv | predicate,
avolume |
| truncnode | node | function,
key × nat → node |
| unbuffered | persistence-state | constant,
persistence-state |
| unmapped | aleb | constant,
aleb |
| valid-adrs | ablock-store-refsize-cons | predicate,
address-set |
| valid-idx | bin-min-heap-inv | predicate,
key-array × array × nat |
| valid-idx | gc-heap-base | predicate,
key-array × lp-array × nat |
| valid-indices | lp-array | predicate,
lp-array × nat-list |
| valid-indices | array-indices | predicate,
array × nat-list |
| validtrailer | node-header-size | constant,
buffer |
| weak | abs-list | variable,
bool |
| x | list-data | variable,
list |
| x0 | list-data | variable,
list |
| x1 | list-data | variable,
list |
| y | list-data | variable,
list |
| z | list-data | variable,
list |
| zero | avolume | constant,
aleb |
| zero | buffer | constant,
data |
| zero | array-splice | constant,
elem |
| zeropage | page | constant,
buffer |
| | | store+set | function,
store × set → store |
| | | nat-store | function,
store × nat-set → store |
| | | ablock-store-refsize-cons | function,
address-set × nat → address-set |
| | | group-store | function,
group-address-store × address-set → group-address-store |
| | | group-store | function,
group-store × nat-set → group-store |
| | | index-store | function,
index-address-store × address-set → index-address-store |
| | | index-store | function,
index-store × nat-set → index-store |
| | | address-store | function,
address-store × address-set → address-store |
| } | nat-list-set | function,
nat → nat-set |
| } | set-union | function,
elem → set |
| } | nat-set | function,
nat → nat-set |
| } | address-list-set | function,
address → address-set |
| } | keyindex-set | function,
keyindex → set |
| } | gc-heap-rename | function,
keyindex → gc-heap-set |
| } | nat-store | function,
nat → nat-set |
| } | address-store | function,
address → address-set |
| φ | lp-array | variable,
lprops → bool |
| φ | array-indices | variable,
elem → bool |
| φn | array-indices | variable,
nat → bool |
| ↓ | awbuf-inv | predicate,
aleb × aleb |
| ↓ | awbuf-inv | predicate,
avolume × avolume |
| ∅ | nat-list-set | constant,
nat-set |
| ∅ | set-basic | constant,
set |
| ∅ | store | constant,
store |
| ∅ | nat-set | constant,
nat-set |
| ∅ | address-list-set | constant,
address-set |
| ∅ | gc-heap-rename | constant,
gc-heap-set |
| ∅ | nat-store | constant,
nat-set |
| ∅ | group-store | constant,
group-address-store |
| ∅ | group-store | constant,
group-store |
| ∅ | index-store | constant,
index-address-store |
| ∅ | index-store | constant,
index-store |
| ∅ | address-store | constant,
address-set |
| ∅ | address-store | constant,
address-store |
| ∈ | encoding-index-node | predicate,
index-node × index-node-list |
| ∈ | nat-list-set | predicate,
nat × nat-set |
| ∈ | nat-list-set | predicate,
nat × nat-list |
| ∈ | encoding-group-node | predicate,
group-node × group-node-list |
| ∈ | store+set | predicate,
data × store |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | store | predicate,
elem × store |
| ∈ | list | predicate,
elem × list |
| ∈ | avolume | predicate,
aleb × avolume |
| ∈ | buffer | predicate,
data × buffer |
| ∈ | array-copy | predicate,
elem × array |
| ∈ | lp-array | predicate,
lprops × lp-array |
| ∈ | nat-set | predicate,
nat × nat-set |
| ∈ | address-list-set | predicate,
address × address-set |
| ∈ | address-list-set | predicate,
address × address-list |
| ∈ | laddress-list | predicate,
laddress × laddress-list |
| ∈ | key-index-array | predicate,
keyindex × key-array |
| ∈ | index-array-base | predicate,
elem-index × array |
| ∈ | keyindex-set | predicate,
keyindex × set |
| ∈ | gc-heap-base | predicate,
lprops × lp-array |
| ∈ | gc-heap-rename | predicate,
keyindex × gc-heap-set |
| ∈ | branch-array | predicate,
branch × branch-array |
| ∈ | nat-store | predicate,
nat × nat-set |
| ∈ | nat-store | predicate,
nat × store |
| ∈ | ablock-store | predicate,
ablock × store |
| ∈ | ablock-store-inv | predicate,
address × store |
| ∈ | group-store | predicate,
group-node × group-address-store |
| ∈ | group-store | predicate,
address × group-address-store |
| ∈ | group-store | predicate,
address × group-store |
| ∈ | group-store | predicate,
group-block × group-store |
| ∈ | group-store | predicate,
nat × group-store |
| ∈ | group-store | predicate,
group-node × group-node-list |
| ∈ | index-store | predicate,
index-node × index-address-store |
| ∈ | index-store | predicate,
address × index-address-store |
| ∈ | index-store | predicate,
address × index-store |
| ∈ | index-store | predicate,
index-block × index-store |
| ∈ | index-store | predicate,
nat × index-store |
| ∈ | index-store | predicate,
index-node × index-node-list |
| ∈ | address-store | predicate,
elem × address-store |
| ∈ | address-store | predicate,
address × address-set |
| ∈ | address-store | predicate,
address × address-store |
| ∈ | string | predicate,
char × string |
| ∩ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∩ | set-union | function,
set × set → set |
| ∩ | nat-set | function,
nat-set × nat-set → nat-set |
| ∩ | address-list-set | function,
address-set × address-set → address-set |
| ∩ | gc-heap-rename | function,
gc-heap-set × gc-heap-set → gc-heap-set |
| ∩ | nat-store | function,
nat-set × nat-set → nat-set |
| ∩ | address-store | function,
address-set × address-set → address-set |
| ∪ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∪ | set-union | function,
set × set → set |
| ∪ | nat-set | function,
nat-set × nat-set → nat-set |
| ∪ | address-list-set | function,
address-set × address-set → address-set |
| ∪ | gc-heap-rename | function,
gc-heap-set × gc-heap-set → gc-heap-set |
| ∪ | nat-store | function,
nat-set × nat-set → nat-set |
| ∪ | address-store | function,
address-set × address-set → address-set |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | nat-list-set | predicate,
nat-set × nat-set |
| ⊆ | set-basic | predicate,
set × set |
| ⊆ | store | predicate,
store × store |
| ⊆ | nat-set | predicate,
nat-set × nat-set |
| ⊆ | address-list-set | predicate,
address-set × address-set |
| ⊆ | gc-heap-rename | predicate,
gc-heap-set × gc-heap-set |
| ⊆ | ebm-vol-inv | predicate,
avolume × avolume |
| ⊆ | nat-store | predicate,
nat-set × nat-set |
| ⊆ | group-store | predicate,
group-address-store × group-address-store |
| ⊆ | group-store | predicate,
group-store × group-store |
| ⊆ | index-store | predicate,
index-address-store × index-address-store |
| ⊆ | index-store | predicate,
index-store × index-store |
| ⊆ | address-store | predicate,
address-set × address-set |
| ⊆ | address-store | predicate,
address-store × address-store |
| ⊏ | string | predicate,
string × string |
| ⊑ | encoding-index-node | predicate,
index-node-list × index-node-list |
| ⊑ | nat-list-set | predicate,
nat-list × nat-list |
| ⊑ | encoding-group-node | predicate,
group-node-list × group-node-list |
| ⊑ | list-last | predicate,
list × list |
| ⊑ | address-list-set | predicate,
address-list × address-list |
| ⊑ | laddress-list | predicate,
laddress-list × laddress-list |
| ⊑ | ablock-store-inv | predicate,
store × store |
| ⊑ | group-store | predicate,
group-store × group-store |
| ⊑ | group-store | predicate,
group-node-list × group-node-list |
| ⊑ | index-store | predicate,
index-store × index-store |
| ⊑ | index-store | predicate,
index-node-list × index-node-list |
| ⊑ | string | predicate,
string × string |
| ⊒ | encoding-index-node | predicate,
index-node-list × index-node-list |
| ⊒ | nat-list-set | predicate,
nat-list × nat-list |
| ⊒ | encoding-group-node | predicate,
group-node-list × group-node-list |
| ⊒ | list-last | predicate,
list × list |
| ⊒ | address-list-set | predicate,
address-list × address-list |
| ⊒ | laddress-list | predicate,
laddress-list × laddress-list |
| ⊒ | group-store | predicate,
group-node-list × group-node-list |
| ⊒ | index-store | predicate,
index-node-list × index-node-list |
| ⊒ | string | predicate,
string × string |
| ⊕ | store+set | function,
store × store → store |
| ⊕ | group-store | function,
group-address-store × group-address-store → group-address-store |
| ⊕ | group-store | function,
group-store × group-store → group-store |
| ⊕ | index-store | function,
index-address-store × index-address-store → index-address-store |
| ⊕ | index-store | function,
index-store × index-store → index-store |
| ⊕ | address-store | function,
address-store × address-store → address-store |
| ⌋ | error-class | predicate,
error |