| symbol | specification | entry |
|---|
| # | zheap | function,
zheap → nat |
| # | zbranch-array | function,
zbranch-array → nat |
| # | heap | function,
heap → nat |
| # | refset | function,
refset → nat |
| # | set-basic | function,
set → nat |
| # | store | function,
store → nat |
| # | array | function,
array → nat |
| # | stringset | function,
stringset → nat |
| # | list-data | function,
list → nat |
| # | node-index | function,
key-set → nat |
| # | node-index | function,
node-index → nat |
| # | nat-store | function,
nat-set → nat |
| # | nat-set | function,
nat-set → nat |
| # | laddress-list | function,
laddress-list → nat |
| # | buffer | function,
buffer → 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 |
| # | node-store | function,
address-set → nat |
| # | node-store | function,
node-store → nat |
| # | branch-array | function,
branch-array → nat |
| # | node-list | function,
node-list → nat |
| # | nat-list-set | function,
nat-set → nat |
| # | nat-list-set | function,
nat-list → nat |
| # | address-list-set | function,
address-set → nat |
| # | address-list-set | function,
address-list → nat |
| # | key-list-set | function,
key-set → nat |
| # | key-list-set | function,
key-list → nat |
| # | address-set-array | function,
address-set-array → nat |
| # | address-store | function,
address-set → nat |
| # | address-store | function,
address-store → nat |
| # | string | function,
string → nat |
| % | nat-div | partial function,
nat × nat → nat |
| ' | list | function,
elem → list |
| ' | laddress-list | function,
laddress → laddress-list |
| ' | group-store | function,
group-node → group-node-list |
| ' | index-store | function,
index-node → index-node-list |
| ' | node-list | function,
node → node-list |
| ' | nat-list-set | function,
nat → nat-list |
| ' | address-list-set | function,
address → address-list |
| ' | key-list-set | function,
key → key-list |
| ' | string | function,
char → string |
| * | nat-mult | function,
nat × nat → nat |
| * | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| * | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| + | array-list | function,
elem × array → array |
| + | list-data | function,
elem × list → list |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → 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 |
| + | array-splice | function,
array × array → array |
| + | buffer | function,
buffer × buffer → buffer |
| + | 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 |
| + | node-list | function,
node-list × node → node-list |
| + | node-list | function,
node-list × node-list → node-list |
| + | node-list | function,
node × node-list → 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 |
| + | 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 |
| + | key-list-set | function,
key-list × key → key-list |
| + | key-list-set | function,
key-list × key-list → key-list |
| + | key-list-set | function,
key × key-list → key-list |
| + | nat-basic | function,
nat × nat → nat |
| + | string | function,
string × char → string |
| + | string | function,
string × string → string |
| + | string | function,
char × string → string |
| ++ | zheap | function,
zheap × ref → zheap |
| ++ | heap | function,
heap × ref → heap |
| ++ | refset | function,
refset × ref → refset |
| ++ | set-basic | function,
set × elem → set |
| ++ | stringset | function,
stringset × string → stringset |
| ++ | node-index | function,
key-set × key → key-set |
| ++ | list-dup | function,
list × elem → list |
| ++ | nat-store | function,
nat-set × nat → nat-set |
| ++ | nat-set | function,
nat-set × nat → nat-set |
| ++ | laddress-list | function,
laddress-list × laddress → laddress-list |
| ++ | group-store | function,
group-node-list × group-node → group-node-list |
| ++ | index-store | function,
index-node-list × index-node → index-node-list |
| ++ | node-store | function,
address-set × address → address-set |
| ++ | node-list | function,
node-list × node → node-list |
| ++ | nat-list-set | function,
nat-set × nat → nat-set |
| ++ | nat-list-set | function,
nat-list × nat → nat-list |
| ++ | address-list-set | function,
address-set × address → address-set |
| ++ | address-list-set | function,
address-list × address → address-list |
| ++ | key-list-set | function,
key-set × key → key-set |
| ++ | key-list-set | function,
key-list × key → key-list |
| ++ | address-store | function,
address-set × address → address-set |
| ++ | string | function,
string × char → string |
| +1 | nat-basic | function,
nat → nat |
| +2 | list | function,
elem × elem → 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 | node-list | function,
node × node → node-list |
| +2 | nat-list-set | function,
nat × nat → nat-list |
| +2 | address-list-set | function,
address × address → address-list |
| +2 | key-list-set | function,
key × key → key-list |
| +2 | string | function,
char × char → string |
| - | nat | partial function,
nat × nat → nat |
| -* | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| -* | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| -- | zheap | function,
zheap × ref → zheap |
| -- | heap | function,
heap × ref → heap |
| -- | refset | function,
refset × ref → refset |
| -- | set-union | function,
set × elem → set |
| -- | store | function,
store × elem → store |
| -- | stringset | function,
stringset × string → stringset |
| -- | node-index | function,
key-set × key → key-set |
| -- | node-index | function,
node-index × key → node-index |
| -- | nat-store | function,
nat-set × nat → nat-set |
| -- | nat-store | function,
store × nat → store |
| -- | nat-set | function,
nat-set × nat → nat-set |
| -- | 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 |
| -- | node-store | function,
address-set × address → address-set |
| -- | node-store | function,
node-store × address → node-store |
| -- | nat-list-set | function,
nat-set × nat → nat-set |
| -- | address-list-set | function,
address-set × address → address-set |
| -- | key-list-set | function,
key-set × key → key-set |
| -- | address-store | function,
address-set × address → address-set |
| -- | address-store | function,
address-store × address → address-store |
| -1 | nat-basic | partial function,
nat → nat |
| -1l | list-del | function,
list × elem → 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 | node-list | function,
node-list × node → node-list |
| -1l | nat-list-set | function,
nat-list × nat → nat-list |
| -1l | address-list-set | function,
address-list × address → address-list |
| -1l | key-list-set | function,
key-list × key → key-list |
| -1l | string | function,
string × char → string |
| -l | list-del | function,
list × elem → 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 | node-list | function,
node-list × node → node-list |
| -l | nat-list-set | function,
nat-list × nat → nat-list |
| -l | address-list-set | function,
address-list × address → address-list |
| -l | key-list-set | function,
key-list × key → key-list |
| -l | string | function,
string × char → string |
| -p | list-del | function,
list × nat → 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 | node-list | function,
node-list × nat → node-list |
| -p | nat-list-set | function,
nat-list × nat → nat-list |
| -p | address-list-set | function,
address-list × nat → address-list |
| -p | key-list-set | function,
key-list × nat → key-list |
| -p | string | function,
string × nat → string |
| -⊗ | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| -⊗ | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| .adr | zbranch | function,
zbranch → address |
| .adr | modification | partial function,
modification → address |
| .adr | branch | function,
branch → address |
| .adr:= | zbranch | function,
zbranch × address → zbranch |
| .adr:= | branch | function,
branch × address → branch |
| .branch? | zbranch | predicate,
zbranch |
| .branch? | branch | predicate,
branch |
| .branches | indexnode | function,
index-node → branch-array |
| .branches:= | indexnode | function,
index-node × branch-array → index-node |
| .butlast | list-last | partial function,
list → 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 | node-list | partial function,
node-list → node-list |
| .butlast | nat-list-set | partial function,
nat-list → nat-list |
| .butlast | address-list-set | partial function,
address-list → address-list |
| .butlast | key-list-set | partial function,
key-list → key-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 |
| .child | zbranch | partial function,
zbranch → ref |
| .child | restructure | partial function,
restructure → ref |
| .child:= | zbranch | partial function,
zbranch × ref → zbranch |
| .contains? | modification | predicate,
modification |
| .data | node | partial function,
node → buffer |
| .data:= | node | partial function,
node × buffer → node |
| .data? | key | predicate,
key |
| .data? | node | predicate,
node |
| .dentry? | key | predicate,
key |
| .dentry? | dentry | predicate,
dentry |
| .dentry? | node | predicate,
node |
| .directory | inode | predicate,
inode |
| .directory | node | partial predicate,
node |
| .directory:= | inode | function,
inode × bool → inode |
| .directory:= | node | partial function,
node × bool → node |
| .dirty | znode | predicate,
znode |
| .dirty:= | znode | function,
znode × bool → znode |
| .end | groupnode | predicate,
group-node |
| .end:= | groupnode | function,
group-node × bool → group-node |
| .entry? | zbranch | predicate,
zbranch |
| .entry? | branch | predicate,
branch |
| .first | array-list | partial function,
array → elem |
| .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 |
| .gndlist | group-store | function,
group-block → group-node-list |
| .gndlist:= | group-store | function,
group-block × group-node-list → group-block |
| .head | list-data | partial function,
list → elem |
| .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 |
| .head | node-list | partial function,
node-list → node |
| .head | nat-list-set | partial function,
nat-list → nat |
| .head | address-list-set | partial function,
address-list → address |
| .head | key-list-set | partial function,
key-list → key |
| .index? | persistence-state | predicate,
persistence-state |
| .indlist | index-store | function,
index-block → index-node-list |
| .indlist:= | index-store | function,
index-block × index-node-list → index-block |
| .ino | key | function,
key → nat |
| .ino | inode | function,
inode → nat |
| .ino | dentry | partial function,
dentry → nat |
| .ino | node | partial function,
node → nat |
| .ino:= | key | function,
key × nat → key |
| .ino:= | inode | function,
inode × nat → inode |
| .ino:= | dentry | partial function,
dentry × nat → dentry |
| .ino:= | node | partial function,
node × nat → node |
| .inode? | key | predicate,
key |
| .inode? | node | predicate,
node |
| .inodes? | aubifs-inv | predicate,
key-set |
| .journal? | persistence-state | predicate,
persistence-state |
| .key | zbranch | function,
zbranch → key |
| .key | restructure | partial function,
restructure → key |
| .key | modification | function,
modification → key |
| .key | node | function,
node → key |
| .key | branch | function,
branch → key |
| .key:= | zbranch | function,
zbranch × key → zbranch |
| .key:= | node | function,
node × key → node |
| .key:= | branch | function,
branch × key → branch |
| .ladrlist | ablock | function,
ablock → laddress-list |
| .ladrlist | group-store | function,
group-block → laddress-list |
| .ladrlist | index-store | function,
index-block → laddress-list |
| .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 | list-last | partial function,
list → elem |
| .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 | node-list | partial function,
node-list → node |
| .last | nat-list-set | partial function,
nat-list → nat |
| .last | address-list-set | partial function,
address-list → address |
| .last | key-list-set | partial function,
key-list → key |
| .last | string | partial function,
string → char |
| .leaf | znode | predicate,
znode |
| .leaf | indexnode | predicate,
index-node |
| .leaf:= | znode | function,
znode × bool → znode |
| .leaf:= | indexnode | function,
index-node × bool → index-node |
| .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 |
| .lookup? | modification | predicate,
modification |
| .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 |
| .max | oset | partial function,
set → elem |
| .max | nat-set | partial function,
nat-set → nat |
| .meta | inode | function,
inode → metadata |
| .meta | node | partial function,
node → metadata |
| .meta:= | inode | function,
inode × metadata → inode |
| .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 | dentry | function,
dentry → string |
| .name:= | key | partial function,
key × string → key |
| .name:= | dentry | function,
dentry × string → dentry |
| .nd | groupnode | function,
group-node → node |
| .nd:= | groupnode | function,
group-node × node → group-node |
| .negdentry? | dentry | predicate,
dentry |
| .nlink | inode | function,
inode → nat |
| .nlink | node | partial function,
node → nat |
| .nlink:= | inode | function,
inode × nat → inode |
| .nlink:= | node | partial function,
node × nat → node |
| .nsubdirs | inode | function,
inode → nat |
| .nsubdirs | node | partial function,
node → nat |
| .nsubdirs:= | inode | function,
inode × nat → inode |
| .nsubdirs:= | node | partial function,
node × nat → node |
| .off | laddress | function,
laddress → nat |
| .off:= | laddress | function,
laddress × nat → laddress |
| .parent | znode | function,
znode → ref |
| .parent:= | znode | function,
znode × ref → znode |
| .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 | ablock | function,
ablock → nat |
| .ref-size | group-store | function,
group-block → nat |
| .ref-size | index-store | function,
index-block → nat |
| .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 |
| .remove? | modification | predicate,
modification |
| .rest | array-list | partial function,
array → array |
| .rstring | string | partial function,
string → string |
| .size | laddress | function,
laddress → nat |
| .size | address-data | function,
address → nat |
| .size | inode | function,
inode → nat |
| .size | node | partial function,
node → nat |
| .size | ablock-store-refsize-cons | function,
address-set → nat |
| .size:= | laddress | function,
laddress × nat → laddress |
| .size:= | address-data | function,
address × nat → address |
| .size:= | inode | function,
inode × nat → inode |
| .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 |
| .store? | modification | predicate,
modification |
| .tail | list-data | partial function,
list → 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 |
| .tail | node-list | partial function,
node-list → node-list |
| .tail | nat-list-set | partial function,
nat-list → nat-list |
| .tail | address-list-set | partial function,
address-list → address-list |
| .tail | key-list-set | partial function,
key-list → key-list |
| .to-adr | ablock-store-inv | function,
laddress-list × nat → address-list |
| .toSet | list+set | function,
list → set |
| .toSet | nat-list-set | function,
nat-list → nat-set |
| .toSet | address-list-set | function,
address-list → address-set |
| .toSet | key-list-set | function,
key-list → key-set |
| .toString | debug | function,
nat → string |
| .trunc? | node | predicate,
node |
| .usedsize | znode | function,
znode → nat |
| .usedsize | indexnode | function,
index-node → nat |
| .usedsize:= | znode | function,
znode × nat → znode |
| .usedsize:= | indexnode | function,
index-node × nat → index-node |
| .zbranches | znode | function,
znode → zbranch-array |
| .zbranches:= | znode | function,
znode × zbranch-array → znode |
| / | nat-div | partial function,
nat × nat → nat |
| < | oelem | predicate,
elem × elem |
| < | array-list | predicate,
array × array |
| < | list-data | predicate,
list × list |
| < | oset | predicate,
set × elem |
| < | oset | predicate,
elem × set |
| < | nat-set | predicate,
nat-set × nat |
| < | nat-set | predicate,
nat × nat-set |
| < | 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 |
| < | key-order-def | predicate,
key × key |
| < | string-less | predicate,
char × char |
| < | string-less | predicate,
string × string |
| < | node-list | predicate,
node-list × node-list |
| < | nat-list-set | predicate,
nat-list × nat-list |
| < | address-list-set | predicate,
address-list × address-list |
| < | key-list-set | predicate,
key-list × key-list |
| < | nat-basic | predicate,
nat × nat |
| => | zheap | function,
ref × znode → zheap → bool |
| => | maplet | function,
ref × obj → heap → bool |
| =>? | zheap | function,
ref → zheap → bool |
| =>? | maplet | function,
ref → heap → bool |
| =>_ | zheap | function,
ref → zheap → bool |
| =>_ | maplet | function,
ref → heap → bool |
| =○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 |
| @ | laddress | function,
nat × nat → laddress |
| @ | address-data | function,
nat × nat × nat → address |
| ADR | apersistence-asm | variable,
address,flexible |
| ADR | index-asm | variable,
address,flexible |
| ADR0 | btree-asm | variable,
address,flexible |
| ADRC | btree-asm | variable,
address,flexible |
| ADRLIST | apersistence-asm | variable,
address-list,flexible |
| ADRLIST | index-asm | variable,
address-list,flexible |
| ADRP | btree-asm | variable,
address,flexible |
| ADRT | btree-asm | variable,
address,flexible |
| ADR_DUMMY | constants | constant,
address |
| AS | btree-asm | variable,
address-set,flexible |
| AS | index-asm | variable,
address-set,flexible |
| BRANCH_SIZE | constants | constant,
nat |
| Boolvar | key-order | variable,
bool,flexible |
| COMMIT? | apersistence-asm | variable,
bool,flexible |
| COMMIT? | index-asm | variable,
bool,flexible |
| DIRTY | btree-asm | variable,
bool,flexible |
| DONE | btree-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? | apersistence-asm | variable,
bool,flexible |
| EMPTY? | index-asm | variable,
bool,flexible |
| 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 |
| EXISTS | btree-asm | variable,
bool,flexible |
| EXISTS | index-asm | variable,
bool,flexible |
| FOUND | btree-asm | variable,
bool,flexible |
| GINVAL | apersistence-asm | variable,
nat-set,flexible |
| GINVAL0 | btree-asm | variable,
nat-set,flexible |
| GND | apersistence-asm | variable,
group-node,flexible |
| GND | index-asm | variable,
group-node,flexible |
| GNDLIST | apersistence-asm | variable,
group-node-list,flexible |
| GNDLIST | index-asm | variable,
group-node-list,flexible |
| GSTORE | apersistence-asm | variable,
group-store,flexible |
| GSTORE0 | apersistence-asm | variable,
group-store,flexible |
| H | heap | variable,
heap |
| H0 | heap | variable,
heap |
| H1 | heap | variable,
heap |
| H2 | heap | variable,
heap |
| IND | apersistence-asm | variable,
index-node,flexible |
| IND | index-asm | variable,
index-node,flexible |
| ISGBLOCK | apersistence-asm | variable,
bool,flexible |
| ISTORE | apersistence-asm | variable,
index-store,flexible |
| ISTORE0 | apersistence-asm | variable,
index-store,flexible |
| ISYNCED | index-asm | variable,
bool,flexible |
| KEY | btree-asm | variable,
key,flexible |
| KEY | index-asm | variable,
key,flexible |
| KS | index-asm | variable,
key-set,flexible |
| LADR | apersistence-asm | variable,
laddress,flexible |
| LADR | index-asm | variable,
laddress,flexible |
| LADRLIST | apersistence-asm | variable,
laddress-list,flexible |
| LADRLIST | index-asm | variable,
laddress-list,flexible |
| LEAF | btree-asm | variable,
bool,flexible |
| LEB_SIZE | eraseblock | constant,
nat |
| LEFT | btree-asm | variable,
nat,flexible |
| LNUM | apersistence-asm | variable,
nat,flexible |
| LNUM | index-asm | variable,
nat,flexible |
| M | btree-asm | variable,
nat,flexible |
| MAXINO | apersistence-asm | variable,
nat,flexible |
| MAXINO0 | apersistence-asm | variable,
nat,flexible |
| MIN_SIZE | constants | constant,
nat |
| MOD | btree-asm | variable,
modification,flexible |
| N | apersistence-asm | variable,
nat,flexible |
| N | index-asm | variable,
nat,flexible |
| N0 | apersistence-asm | variable,
nat,flexible |
| N0 | index-asm | variable,
nat,flexible |
| NAMES | btree-asm | variable,
stringset,flexible |
| NAMES | index-asm | variable,
stringset,flexible |
| ND | btree-asm | variable,
node,flexible |
| ND | index-asm | variable,
node,flexible |
| NL | apersistence-asm | variable,
nat-list,flexible |
| NL0 | apersistence-asm | variable,
nat-list,flexible |
| NS | apersistence-asm | variable,
nat-set,flexible |
| NS | index-asm | variable,
nat-set,flexible |
| NS0 | apersistence-asm | variable,
nat-set,flexible |
| NS0 | index-asm | variable,
nat-set,flexible |
| NS1 | apersistence-asm | variable,
nat-set,flexible |
| NS1 | index-asm | variable,
nat-set,flexible |
| NUSED | btree-asm | variable,
nat,flexible |
| OFFSET | apersistence-asm | variable,
nat,flexible |
| OLDADR | btree-asm | variable,
address,flexible |
| OLDADR | index-asm | variable,
address,flexible |
| OS | apersistence-asm | variable,
nat-set,flexible |
| OS0 | apersistence-asm | variable,
nat-set,flexible |
| P | zheap | variable,
zheap → bool |
| P | heap-sep | variable,
heap → bool |
| P0 | zheap | variable,
zheap → bool |
| P0 | heap-sep | variable,
heap → bool |
| P1 | zheap | variable,
zheap → bool |
| P1 | heap-sep | variable,
heap → bool |
| P2 | zheap | variable,
zheap → bool |
| P2 | heap-sep | variable,
heap → bool |
| PAGES_PER_LEB | eraseblock | constant,
nat |
| PAGES_PER_PEB | eraseblock | constant,
nat |
| PEB_SIZE | eraseblock | constant,
nat |
| PFI | index-asm | variable,
node-index,flexible |
| PINVAL | index-asm | variable,
nat-set,flexible |
| PMAXINO | index-asm | variable,
nat,flexible |
| PMAXINO0 | index-asm | variable,
nat,flexible |
| PNL | index-asm | variable,
nat-list,flexible |
| PNL0 | index-asm | variable,
nat-list,flexible |
| POSITION | btree-asm | variable,
nat,flexible |
| PPMAXINO | index-asm | variable,
nat,flexible |
| PPMAXINO0 | index-asm | variable,
nat,flexible |
| PRI | index-asm | variable,
node-index,flexible |
| PSTATE | apersistence-asm | variable,
persistence-state,flexible |
| PSTORE | index-asm | variable,
group-store,flexible |
| PSTORE0 | index-asm | variable,
group-store,flexible |
| PSYNCED | apersistence-asm | variable,
bool,flexible |
| P_OS | index-asm | variable,
nat-set,flexible |
| P_OS0 | index-asm | variable,
nat-set,flexible |
| Pa | zheap | variable,
address-set-array → zheap → bool |
| Pa | existential | variable,
elem → heap → bool |
| R | btree-asm | variable,
ref,flexible |
| R0 | btree-asm | variable,
ref,flexible |
| RC | btree-asm | variable,
ref,flexible |
| RIGHT | btree-asm | variable,
nat,flexible |
| RL | btree-asm | variable,
ref,flexible |
| RN | btree-asm | variable,
ref,flexible |
| ROFS | apersistence-asm | variable,
bool,flexible |
| ROOTADR | apersistence-asm | variable,
address,flexible |
| ROOTADR0 | apersistence-asm | variable,
address,flexible |
| ROOT_INO | root-ino | constant,
nat |
| RP | btree-asm | variable,
ref,flexible |
| RR | btree-asm | variable,
ref,flexible |
| RT | btree-asm | variable,
ref,flexible |
| SIZE | apersistence-asm | variable,
nat,flexible |
| SIZE | index-asm | variable,
nat,flexible |
| SKIP | btree-asm | variable,
nat,flexible |
| True | separation | predicate,
bool |
| VFS_PAGE_SIZE | page | constant,
nat |
| VOLSIZE | apersistence-asm | variable,
nat,flexible |
| VOLSIZE | index-asm | variable,
nat,flexible |
| ZH | btree-asm | variable,
zheap,flexible |
| ZND | btree-asm | variable,
znode,flexible |
| [] | array-list | constant,
array |
| [] | list-data | constant,
list |
| [] | laddress-list | constant,
laddress-list |
| [] | group-store | constant,
group-node-list |
| [] | index-store | constant,
index-node-list |
| [] | node-list | constant,
node-list |
| [] | nat-list-set | constant,
nat-list |
| [] | address-list-set | constant,
address-list |
| [] | key-list-set | constant,
key-list |
| \ | zheap | function,
zheap × zheap → zheap |
| \ | zheap | function,
zheap × refset → zheap |
| \ | heap | function,
heap × heap → heap |
| \ | heap | function,
heap × refset → heap |
| \ | refset | function,
refset × refset → refset |
| \ | store+set | function,
store × set → store |
| \ | set-union | function,
set × set → set |
| \ | stringset | function,
stringset × stringset → stringset |
| \ | node-index | function,
node-index × key-set → node-index |
| \ | node-index | function,
key-set × key-set → key-set |
| \ | nat-store | function,
store × nat-set → store |
| \ | nat-store | function,
nat-set × nat-set → nat-set |
| \ | nat-set | 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 |
| \ | node-store | function,
node-store × address-set → node-store |
| \ | node-store | function,
address-set × address-set → address-set |
| \ | nat-list-set | function,
nat-set × nat-set → nat-set |
| \ | address-list-set | function,
address-set × address-set → address-set |
| \ | key-list-set | function,
key-set × key-set → key-set |
| \ | address-store | function,
address-store × address-set → address-store |
| \ | address-store | function,
address-set × address-set → address-set |
| ] | zheap | function,
zheap × ref × znode → zheap |
| ] | zheap | function,
zheap × ref → znode |
| ] | zbranch-array | partial function,
zbranch-array × nat × zbranch → zbranch-array |
| ] | zbranch-array | partial function,
zbranch-array × nat → zbranch |
| ] | heap | function,
heap × ref × obj → heap |
| ] | heap | function,
heap × ref → obj |
| ] | store | partial function,
store × elem → data |
| ] | store | function,
store × elem × data → store |
| ] | array | partial function,
array × nat × elem → array |
| ] | array | partial function,
array × nat → elem |
| ] | node-index | partial function,
node-index × key → address |
| ] | node-index | function,
node-index × key × address → node-index |
| ] | list-del | partial function,
list × nat × elem → list |
| ] | list-del | partial function,
list × nat → elem |
| ] | nat-store | partial function,
store × nat → data |
| ] | nat-store | function,
store × nat × data → store |
| ] | laddress-list | partial function,
laddress-list × nat × laddress → laddress-list |
| ] | laddress-list | partial function,
laddress-list × nat → laddress |
| ] | ablock-store | partial function,
store × nat → ablock |
| ] | ablock-store | function,
store × nat × ablock → store |
| ] | buffer | partial function,
buffer × nat × data → buffer |
| ] | buffer | partial function,
buffer × nat → data |
| ] | 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 |
| ] | node-store | partial function,
node-store × address → node |
| ] | node-store | function,
node-store × address × node → node-store |
| ] | aubifs-base | function,
node-store × address-list → node-list |
| ] | aubifs-base | function,
node-store × address-list × node-list → node-store |
| ] | aubifs-base | function,
node-index × key-list → address-list |
| ] | aubifs-base | function,
node-index × key-list × address-list → node-index |
| ] | branch-array | partial function,
branch-array × nat × branch → branch-array |
| ] | branch-array | partial function,
branch-array × nat → branch |
| ] | index-base | function,
node-index × key-set → address-set |
| ] | node-list | partial function,
node-list × nat × node → node-list |
| ] | node-list | partial function,
node-list × nat → node |
| ] | nat-list-set | partial function,
nat-list × nat × nat → nat-list |
| ] | nat-list-set | partial function,
nat-list × nat → nat |
| ] | address-list-set | partial function,
address-list × nat × address → address-list |
| ] | address-list-set | partial function,
address-list × nat → address |
| ] | key-list-set | partial function,
key-list × nat × key → key-list |
| ] | key-list-set | partial function,
key-list × nat → key |
| ] | address-set-array | partial function,
address-set-array × nat × address-set → address-set-array |
| ] | address-set-array | partial function,
address-set-array × nat → address-set |
| ] | 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 |
| _∃ | zheap | function,
address-set-array → zheap → bool → zheap → bool |
| _∃ | zheap | function,
znode → zheap → bool → zheap → bool |
| _∃ | zheap | function,
ref × ref → zheap → bool → zheap → bool |
| _∃ | zheap | function,
ref → zheap → bool → zheap → bool |
| _∃ | maplet | function,
obj → heap → bool → heap → bool |
| _∃ | maplet | function,
ref × ref → heap → bool → heap → bool |
| _∃ | maplet | function,
ref → heap → bool → heap → bool |
| _∃ | existential | function,
elem → heap → bool → heap → bool |
| a | elem | variable,
elem |
| a | address-set-array | variable,
address-set |
| a0 | list-data | 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 |
| address | address | sort,
|
| address | address-data | sort,
|
| address-list | address-list-set | sort,
|
| address-set | node-store | sort,
|
| address-set | address-list-set | sort,
|
| address-set | address-store | sort,
|
| address-set-array | address-set-array | 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 | variable,
address |
| adr | address-data | 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 |
| align↑ | align | function,
nat × nat → nat |
| align↓ | align | function,
nat × nat → nat |
| alladrs | btree-inv | variable,
address-set |
| 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 |
| ar10 | array-list | variable,
array |
| ar2 | array | variable,
array |
| ar3 | array-list | variable,
array |
| ar4 | array-list | variable,
array |
| ar5 | array-list | variable,
array |
| ar6 | array-list | variable,
array |
| ar7 | array-list | variable,
array |
| ar8 | array-list | variable,
array |
| ar9 | array-list | variable,
array |
| array | array | sort,
|
| as | node-store | variable,
address-set |
| as | address-list-set | variable,
address-set |
| as | address-store | variable,
address-set |
| as0 | node-store | variable,
address-set |
| as0 | address-list-set | variable,
address-set |
| as0 | address-store | variable,
address-set |
| as1 | node-store | variable,
address-set |
| as1 | address-list-set | variable,
address-set |
| as1 | address-store | variable,
address-set |
| as2 | node-store | variable,
address-set |
| as2 | address-list-set | variable,
address-set |
| as2 | address-store | variable,
address-set |
| asar | address-set-array | variable,
address-set-array |
| asar0 | address-set-array | variable,
address-set-array |
| asar1 | address-set-array | variable,
address-set-array |
| asar2 | address-set-array | variable,
address-set-array |
| ast | address-store | variable,
address-store |
| ast0 | address-store | variable,
address-store |
| ast1 | address-store | variable,
address-store |
| ast2 | address-store | variable,
address-store |
| aubifs-crash | aubifs-base | predicate,
node-index × key-set × key-set × node-index × key-set × node-store × address-list × node-index × key-set × key-set × node-index × key-set × node-store × address-list |
| 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 |
| b | address-set-array | variable,
address-set |
| bnode | btree-inv | function,
ref × zbranch-array × nat × nat × nat × nat × bool × node-index × index-address-store × address-set × address-set → zheap → bool |
| boolvar | key-order | variable,
bool |
| boolvar | inode | variable,
bool |
| boolvar | node | variable,
bool |
| boolvar | indexnode | variable,
bool |
| boolvar0 | key-order | variable,
bool |
| boolvar0 | inode | variable,
bool |
| boolvar0 | node | variable,
bool |
| boolvar0 | indexnode | variable,
bool |
| boolvar1 | key-order | variable,
bool |
| boolvar1 | groupnode | variable,
bool |
| boolvar2 | znode | 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 |
| btree | btree-inv | function,
ref × ref × address × nat × bool × node-index × index-address-store × address-set × address-set × node-status → zheap → bool |
| btree-inv | btree-inv | predicate,
ref × address × index-store × index-store × zheap × node-index × node-index |
| btree-sub-clean | btree-inv | predicate,
ref × nat × zheap |
| btree_add_gnds# | btree-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 |
| btree_allocate_gnd# | btree-asm | procedure,
address × index-store × index-store × group-store × nat × nat-set ×
bool
: nat-set × group-store × nat-list × persistence-state
: error |
| btree_commit# | btree-asm | procedure,
nat × ref
: nat-set × address × zheap × address × index-store × index-store ×
nat-set × group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: error |
| btree_commit_rec# | btree-asm | procedure,
ref × address × index-store × nat-set × group-store × group-store ×
nat-list × nat × nat-set
: address × error × zheap × index-store × persistence-state × bool |
| btree_deallocate_gnd# | btree-asm | procedure,
nat × address × index-store × index-store × group-store × nat-list ×
nat × nat-set × persistence-state × bool
: nat-set × group-store
: error |
| btree_entries# | btree-asm | procedure,
key × ref × address × address × index-store × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × bool × stringset × zheap
: error |
| btree_format# | btree-asm | procedure,
nat × nat × nat
: address × address × index-store × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × error |
| btree_get_block_free_size# | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| btree_get_gblock_refsize# | btree-asm | procedure,
nat × address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| btree_get_gc_block# | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: nat
: error |
| btree_get_leb_size | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat |
| btree_index_contains# | btree-asm | procedure,
key × address × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: bool × ref × zheap × index-store
: error |
| btree_index_entries# | btree-asm | procedure,
key × address × address × index-store × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: stringset × ref × zheap
: error |
| btree_index_lookup# | btree-asm | procedure,
key × address × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: bool × address × ref × zheap × index-store
: error |
| btree_index_remove# | btree-asm | procedure,
key × address × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: address × bool × ref × zheap × index-store |
| btree_index_store# | btree-asm | procedure,
key × address × address × address × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: address × bool × ref × zheap × index-store |
| btree_index_truncate# | btree-asm | procedure,
key × nat × address × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: address-set × ref × zheap × index-store |
| btree_io_dirty# | btree-asm | procedure,
ref × address × bool × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: error × zheap × index-store |
| btree_io_load# | btree-asm | procedure,
ref × address × address × index-store × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × zheap
: error |
| btree_io_save# | btree-asm | procedure,
ref × address × index-store × nat-set × group-store × group-store ×
nat-list × nat × nat-set
: address × zheap × index-store × persistence-state × bool
: error |
| btree_io_scan# | btree-asm | procedure,
key × nat × ref × zheap : nat |
| btree_io_shift_left# | btree-asm | procedure,
nat × ref : zheap |
| btree_io_shift_n_left# | btree-asm | procedure,
nat × nat × ref : zheap |
| btree_io_shift_right# | btree-asm | procedure,
nat × ref : zheap |
| btree_io_split# | btree-asm | procedure,
nat × ref : ref × ref × error × zheap |
| btree_is_log_empty# | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool |
| btree_read_gblock_nodes# | btree-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 |
| btree_read_gnd# | btree-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 |
| btree_recover# | btree-asm | procedure,
: nat × nat-list × nat-set × address × address × index-store ×
index-store × nat-set × group-store × group-store × nat-list × nat ×
nat-set × persistence-state × bool
: ref × error |
| btree_requires_commit# | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool |
| btree_set_gblock_refsize# | btree-asm | procedure,
nat × nat × address × index-store × index-store × nat-set ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: group-store |
| btree_sync# | btree-asm | procedure,
address × index-store × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set
: persistence-state × bool
: error |
| btree_traverse# | btree-asm | procedure,
modification × ref × address × address × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × bool × bool × address × zheap × index-store
: error |
| btree_traverse_root# | btree-asm | procedure,
modification × ref × address × address × index-store × nat-set ×
group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: bool × bool × address × ref × zheap × index-store
: error |
| btree_truncate# | btree-asm | procedure,
key × ref × address × address × index-store × nat-set × group-store ×
group-store × nat-list × nat × nat-set × persistence-state × bool
: ref × bool × bool × address-set × zheap × index-store
: error |
| buf | buffer | variable,
buffer |
| buf0 | buffer | variable,
buffer |
| buf1 | buffer | variable,
buffer |
| buf2 | buffer | variable,
buffer |
| buffer | buffer | sort,
|
| butlastn | list-last | partial function,
nat × list → 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 | node-list | partial function,
nat × node-list → node-list |
| butlastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| butlastn | address-list-set | partial function,
nat × address-list → address-list |
| butlastn | key-list-set | partial function,
nat × key-list → key-list |
| butlastn | string | partial function,
nat × string → string |
| bv | heap-sep | variable,
bool |
| bv | znode-ops | variable,
bool |
| c | elem | variable,
elem |
| c | address-set-array | variable,
address-set |
| char | char | variable,
char |
| char | char | sort,
|
| char0 | char | variable,
char |
| char1 | char | variable,
char |
| char2 | char | variable,
char |
| char3 | string-less | variable,
char |
| cmp | zbranch-array | partial predicate,
zbranch-array × zbranch × nat × nat |
| cmp | zbranch-array | partial predicate,
zbranch-array × nat × zbranch-array × nat × nat |
| cmp | array-copy | partial predicate,
array × elem × nat × nat |
| cmp | array-copy | partial predicate,
array × nat × array × nat × nat |
| cmp | buffer | partial predicate,
buffer × data × nat × nat |
| cmp | buffer | partial predicate,
buffer × nat × buffer × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × branch × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × nat × branch-array × nat × nat |
| cmp | address-set-array | partial predicate,
address-set-array × address-set × nat × nat |
| cmp | address-set-array | partial predicate,
address-set-array × nat × address-set-array × nat × nat |
| commit-inv | btree-inv | predicate,
nat × persistence-state × index-store × index-store × nat-list × group-store × group-store × nat-set × bool × error × ref × ref × address × nat × bool × node-index × index-store × address-set × address-set × address-set × zheap → bool × zheap |
| compatible | zbranch-array-ops | predicate,
key-set × key-set × zbranch-array × nat × nat |
| compatible | zbranch-array-ops | predicate,
node-index × node-index × zbranch-array × nat × nat |
| contains | modification | function,
key → modification |
| copy | zbranch-array | partial function,
zbranch-array × nat × zbranch-array × nat × nat → zbranch-array |
| copy | array-copy | partial function,
array × nat × array × nat × nat → array |
| copy | buffer | partial function,
buffer × nat × buffer × nat × nat → buffer |
| copy | branch-array | partial function,
branch-array × nat × branch-array × nat × nat → branch-array |
| copy | address-set-array | partial function,
address-set-array × nat × address-set-array × nat × nat → address-set-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 |
| datakeys | aubifs-base | function,
key-set × node-index → key-set |
| datakeys | aubifs-base | function,
key × nat × node-index → key-set |
| datakeys | aubifs-base | function,
key × node-index → key-set |
| datanode | node | function,
key × buffer → node |
| debug# | debug | procedure,
string : |
| dent | dentry | variable,
dentry |
| dentries | aubifs-base | function,
key × node-index → stringset |
| dentry | dentry | sort,
|
| dentrykey | key | function,
nat × string → key |
| dentrykeys | aubifs-base | function,
key × node-index → key-set |
| dentrynode | node | function,
key × nat → node |
| dirty | zbranch-array-ops | variable,
bool |
| dirty0 | zbranch-array-ops | variable,
bool |
| disj | list-dup | predicate,
list × 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 | node-list | predicate,
node-list × node-list |
| disj | nat-list-set | predicate,
nat-list × nat-list |
| disj | address-list-set | predicate,
address-list × address-list |
| disj | key-list-set | predicate,
key-list × key-list |
| disj | address-set-array-ops | predicate,
address-set-array × nat × nat |
| disj | string | predicate,
string × string |
| dom | store+set | function,
store → set |
| dom | node-index | function,
node-index → key-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 | node-store | function,
node-store → address-set |
| dom | address-store | function,
address-store → address-set |
| dropn | list-prefixn | function,
nat × list → list |
| dropn | laddress-list | function,
nat × laddress-list → laddress-list |
| dropn | group-store | function,
nat × group-node-list → group-node-list |
| dropn | index-store | function,
nat × index-node-list → index-node-list |
| dropn | node-list | function,
nat × node-list → node-list |
| dropn | nat-list-set | function,
nat × nat-list → nat-list |
| dropn | address-list-set | function,
nat × address-list → address-list |
| dropn | key-list-set | function,
nat × key-list → key-list |
| dups | list-dup | predicate,
list |
| dups | laddress-list | predicate,
laddress-list |
| dups | group-store | predicate,
group-node-list |
| dups | index-store | predicate,
index-node-list |
| dups | node-list | predicate,
node-list |
| dups | nat-list-set | predicate,
nat-list |
| dups | address-list-set | predicate,
address-list |
| dups | key-list-set | predicate,
key-list |
| dups | string | predicate,
string |
| elem | elem | 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 |
| elems | apersistence-base | function,
nat-list → nat-set |
| emp | zheap | predicate,
zheap |
| emp | heap-sep | predicate,
heap |
| empty | array-splice | constant,
elem |
| empty | buffer | constant,
data |
| emptyleb | eraseblock | constant,
buffer |
| emptypage | eraseblock | constant,
buffer |
| emptypeb | eraseblock | constant,
buffer |
| err | error | variable,
error |
| err0 | error | variable,
error |
| err1 | error | variable,
error |
| error | error | sort,
|
| fail# | error-class | procedure,
: : error |
| fail_or_success# | error-class | procedure,
: : error |
| false | zheap | predicate,
zheap |
| false | heap-sep | predicate,
heap |
| fi | aubifs-base | variable,
node-index |
| fi | btree-inv | variable,
node-index |
| fi0 | aubifs-base | variable,
node-index |
| fi1 | aubifs-base | variable,
node-index |
| fi2 | aubifs-base | variable,
node-index |
| file-node-cons | aubifs-inv | predicate,
node-store × node-index |
| fill | zbranch-array | partial function,
zbranch-array × zbranch × nat × nat → zbranch-array |
| fill | zbranch-array | function,
zbranch-array × zbranch → zbranch-array |
| fill | array-copy | partial function,
array × elem × nat × nat → array |
| fill | array-copy | function,
array × elem → array |
| fill | buffer | partial function,
buffer × data × nat × nat → buffer |
| fill | buffer | function,
buffer × data → buffer |
| fill | branch-array | partial function,
branch-array × branch × nat × nat → branch-array |
| fill | branch-array | function,
branch-array × branch → branch-array |
| fill | address-set-array | partial function,
address-set-array × address-set × nat × nat → address-set-array |
| fill | address-set-array | function,
address-set-array × address-set → address-set-array |
| fillfirst | list-last | function,
nat × elem × list → 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 | node-list | function,
nat × node × node-list → node-list |
| fillfirst | nat-list-set | function,
nat × nat × nat-list → nat-list |
| fillfirst | address-list-set | function,
nat × address × address-list → address-list |
| fillfirst | key-list-set | function,
nat × key × key-list → key-list |
| fillfirst | string | function,
nat × char × string → string |
| firstn | list-del | partial function,
nat × list → 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 | node-list | partial function,
nat × node-list → node-list |
| firstn | nat-list-set | partial function,
nat × nat-list → nat-list |
| firstn | address-list-set | partial function,
nat × address-list → address-list |
| firstn | key-list-set | partial function,
nat × key-list → key-list |
| firstn | string | partial function,
nat × string → string |
| fo | aubifs-base | variable,
key-set |
| fo0 | aubifs-base | variable,
key-set |
| fo1 | aubifs-base | variable,
key-set |
| fo2 | aubifs-base | variable,
key-set |
| frome | list-del | function,
list × elem → 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 | node-list | function,
node-list × node → node-list |
| frome | nat-list-set | function,
nat-list × nat → nat-list |
| frome | address-list-set | function,
address-list × address → address-list |
| frome | key-list-set | function,
key-list × key → key-list |
| frome | string | function,
string × char → string |
| fs | node-store | variable,
node-store |
| fs0 | node-store | variable,
node-store |
| fs1 | node-store | variable,
node-store |
| fs2 | node-store | variable,
node-store |
| 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 | group-store | variable,
group-block |
| gblock0 | group-store | variable,
group-block |
| gblock1 | group-store | variable,
group-block |
| gblock2 | group-store | variable,
group-block |
| 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 | group-store | variable,
group-node |
| gnd1 | group-store | variable,
group-node |
| gnd2 | group-store | variable,
group-node |
| gndx | group-store | variable,
group-node-list |
| gndx0 | group-store | variable,
group-node-list |
| gndx1 | group-store | variable,
group-node-list |
| gndx2 | group-store | variable,
group-node-list |
| gndx3 | group-store | variable,
group-node-list |
| group-address-store | group-store | sort,
|
| group-block | group-store | sort,
|
| group-node | groupnode | sort,
|
| group-node-list | group-store | sort,
|
| group-store | group-store | sort,
|
| 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 | heap | sort,
|
| height | zbranch-array-ops | variable,
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 | index-store | variable,
index-block |
| iblock0 | index-store | variable,
index-block |
| iblock1 | index-store | variable,
index-block |
| iblock2 | index-store | variable,
index-block |
| idataf | index-store | variable,
index-block → index-block |
| idrange | zbranch-array | partial predicate,
zbranch-array × nat × nat |
| idrange | array-copy | partial predicate,
array × nat × nat |
| idrange | buffer | partial predicate,
buffer × nat × nat |
| idrange | branch-array | partial predicate,
branch-array × nat × nat |
| idrange | address-set-array | partial predicate,
address-set-array × nat × nat |
| id○ | zbranch-array | predicate,
zbranch-array × zbranch-array × nat |
| id○ | array-copy | predicate,
array × array × nat |
| id○ | buffer | predicate,
buffer × buffer × nat |
| id○ | branch-array | predicate,
branch-array × branch-array × nat |
| id○ | address-set-array | predicate,
address-set-array × address-set-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 | index-store | variable,
index-node |
| ind1 | index-store | variable,
index-node |
| ind2 | index-store | variable,
index-node |
| index | persistence-state | function,
nat → persistence-state |
| index-address-store | index-store | sort,
|
| index-block | index-store | sort,
|
| index-node | indexnode | sort,
|
| index-node-list | index-store | sort,
|
| index-store | index-store | sort,
|
| index_add_gnds# | index-asm | procedure,
group-node-list × node-index × node-index × nat-set × group-store ×
nat-list × nat × nat-set
: address-list × group-store
: bool × error |
| index_allocate_gnd# | index-asm | procedure,
node-index × node-index × group-store × nat × nat-set × bool
: nat-set × group-store × nat-list
: error |
| index_commit# | index-asm | procedure,
nat × node-index × bool
: nat-set × nat-set × group-store × node-index × group-store ×
nat-list × nat × nat-set
: error |
| index_deallocate_gnd# | index-asm | procedure,
nat × node-index × node-index × group-store × nat-list × nat × nat-set ×
bool
: nat-set × group-store
: error |
| index_format# | index-asm | procedure,
nat × nat × nat
:
: node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool × error |
| index_get_block_free_size# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_get_gblock_refsize# | index-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_get_gc_block# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: nat
: error |
| index_get_leb_size | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_index_contains# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool
: error |
| index_index_entries# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: stringset
: error |
| index_index_lookup# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool × address
: error |
| index_index_remove# | index-asm | procedure,
key × node-index × nat-set × group-store × group-store × nat-list ×
nat × nat-set × bool
: address × bool × node-index |
| index_index_store# | index-asm | procedure,
key × address × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address × bool × node-index |
| index_index_truncate# | index-asm | procedure,
key × nat × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-set × node-index |
| index_is_log_empty# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: bool |
| index_read_gblock_nodes# | index-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-list × group-node-list
: error |
| index_read_gnd# | index-asm | procedure,
address × node-index × node-index × nat-set × group-store ×
group-store × nat-list × nat × nat-set × bool
: group-node
: error |
| index_recover# | index-asm | procedure,
: nat × nat-list × nat-set × node-index × nat-list × nat × nat-set ×
nat-set × group-store × group-store
: node-index × bool × error |
| index_requires_commit# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: bool |
| index_set_gblock_refsize# | index-asm | procedure,
nat × nat × node-index × node-index × nat-set × group-store × nat-list ×
nat × nat-set × bool
: group-store |
| index_sync# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set
:
: bool × error |
| indexblock | index-store | function,
index-node-list × laddress-list × nat → index-block |
| indexnode | indexnode | function,
branch-array × bool × nat → index-node |
| indx | index-store | variable,
index-node-list |
| indx0 | index-store | variable,
index-node-list |
| indx1 | index-store | variable,
index-node-list |
| indx2 | index-store | variable,
index-node-list |
| indx3 | index-store | variable,
index-node-list |
| ino | key-order-def | variable,
nat |
| ino | aubifs-base | variable,
nat |
| ino0 | aubifs-base | variable,
nat |
| ino1 | aubifs-base | variable,
nat |
| ino2 | aubifs-base | variable,
nat |
| inode | inode | variable,
inode |
| inode | inode | sort,
|
| 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 |
| isempty | eraseblock | predicate,
buffer × nat × nat |
| isempty | eraseblock | predicate,
buffer |
| istore | index-store | variable,
index-store |
| istore0 | index-store | variable,
index-store |
| istore1 | index-store | variable,
index-store |
| istore2 | index-store | variable,
index-store |
| ite | zheap | function,
bool × zheap → bool × zheap → bool → zheap → bool |
| ite | heap-sep | function,
bool × heap → bool × heap → bool → heap → bool |
| journal | persistence-state | function,
nat → persistence-state |
| key | key | variable,
key |
| key | key | sort,
|
| key' | zbranch-array-ops | variable,
key |
| key-cons | aubifs-inv | predicate,
key × node |
| key-list | key-list-set | sort,
|
| key-range | zbranch-array-ops | function,
zbranch-array × nat × nat × node-index → node-index |
| key-set | node-index | sort,
|
| key-set | key-list-set | sort,
|
| key0 | zbranch | variable,
key |
| key0 | node-index | variable,
key |
| key0 | restructure | variable,
key |
| key0 | node | variable,
key |
| key0 | branch | variable,
key |
| key0 | key-list-set | variable,
key |
| key1 | key-order | variable,
key |
| key1 | node-index | variable,
key |
| key1 | key-list-set | variable,
key |
| key2 | key-list-set | variable,
key |
| keys | aubifs-base | function,
node-store × address-list → key-list |
| keys | zbranch-array-ops | function,
zbranch-array × nat × nat → key-set |
| ks | node-index | variable,
key-set |
| ks | key-list-set | variable,
key-set |
| ks0 | node-index | variable,
key-set |
| ks0 | key-list-set | variable,
key-set |
| ks1 | node-index | variable,
key-set |
| ks1 | key-list-set | variable,
key-set |
| ks2 | node-index | variable,
key-set |
| ks2 | key-list-set | variable,
key-set |
| kx | key-list-set | variable,
key-list |
| kx0 | key-list-set | variable,
key-list |
| kx1 | key-list-set | variable,
key-list |
| ky | key-list-set | variable,
key-list |
| kz | key-list-set | variable,
key-list |
| 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 | list-del | partial function,
nat × list → 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 | node-list | partial function,
nat × node-list → node-list |
| lastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| lastn | address-list-set | partial function,
nat × address-list → address-list |
| lastn | key-list-set | partial function,
nat × key-list → key-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 |
| ld | aubifs-base | variable,
key-set |
| ld | zbranch-array-ops | variable,
key-set |
| ld0 | aubifs-base | variable,
key-set |
| ld0 | zbranch-array-ops | variable,
key-set |
| ld1 | aubifs-base | variable,
key-set |
| ld1 | zbranch-array-ops | variable,
key-set |
| ld2 | aubifs-base | variable,
key-set |
| len | znode-ops | variable,
nat |
| links | aubifs-base | function,
nat × node-store × node-index → key-set |
| list | list-data | sort,
|
| load | znode-ops | function,
branch → zbranch |
| load | znode-ops | function,
branch-array × nat × nat → zbranch-array |
| load | znode-ops | function,
ref × index-node → znode |
| log | aubifs-base | variable,
address-list |
| log-cons | aubifs-inv | predicate,
address-list × node-store |
| log0 | aubifs-base | variable,
address-list |
| log1 | aubifs-base | variable,
address-list |
| log2 | aubifs-base | variable,
address-list |
| look | zbranch-array-ops | predicate,
bool × key × address × node-index |
| lookup | modification | function,
key → modification |
| m | nat-basic | variable,
nat |
| m0 | key | variable,
nat |
| m0 | array-copy | variable,
nat |
| m0 | laddress | variable,
nat |
| m0 | address-data | variable,
nat |
| m0 | inode | variable,
nat |
| m0 | dentry | variable,
nat |
| m0 | persistence-state | variable,
nat |
| m1 | key | variable,
nat |
| m1 | laddress | variable,
nat |
| m1 | address-data | variable,
nat |
| m1 | inode | variable,
nat |
| m2 | key | variable,
nat |
| m2 | laddress | variable,
nat |
| m2 | address-data | variable,
nat |
| m2 | inode | variable,
nat |
| m3 | address-data | variable,
nat |
| m3 | inode | variable,
nat |
| m3 | node | variable,
nat |
| m4 | address-data | variable,
nat |
| m4 | inode | variable,
nat |
| m4 | node | variable,
nat |
| m5 | inode | variable,
nat |
| m6 | inode | variable,
nat |
| max | min-max | function,
nat × nat → nat |
| maxino | apersistence-base | variable,
nat |
| md | metadata | variable,
metadata |
| md0 | inode | variable,
metadata |
| md0 | node | variable,
metadata |
| metadata | metadata | sort,
|
| min | min-max | function,
nat × nat → nat |
| mkarray | array | function,
nat → array |
| mkarray | address-set-array | function,
nat → address-set-array |
| 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 |
| mkdentry | dentry | function,
string × nat → dentry |
| 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 |
| mkinode | inode | function,
nat × metadata × bool × nat × nat × nat → inode |
| mklist | list-last | function,
elem × nat → 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 | node-list | function,
node × nat → node-list |
| mklist | nat-list-set | function,
nat × nat → nat-list |
| mklist | address-list-set | function,
address × nat → address-list |
| mklist | key-list-set | function,
key × nat → key-list |
| mklist | string | function,
char × nat → string |
| mkzarray | array-splice | function,
nat → array |
| mkzbranch | zbranch | function,
key × address × ref → zbranch |
| mkzbrarray | zbranch-array | function,
nat → zbranch-array |
| mkzbuf | buffer | function,
nat → buffer |
| mkzentry | zbranch | function,
key × address → zbranch |
| mkznode | znode | function,
ref × zbranch-array × bool × bool × nat → znode |
| mod | modification | variable,
modification |
| modification | modification | sort,
|
| n | nat-basic | variable,
nat |
| n0 | nat-basic | variable,
nat |
| n1 | nat-basic | variable,
nat |
| n2 | nat-store | variable,
nat |
| n2 | nat-set | variable,
nat |
| n2 | nat-list-set | variable,
nat |
| n3 | nat-store | variable,
nat |
| n3 | nat-set | variable,
nat |
| n3 | nat-list-set | variable,
nat |
| n4 | nat-store | variable,
nat |
| n4 | nat-set | variable,
nat |
| n4 | nat-list-set | variable,
nat |
| n5 | nat-list-set | variable,
nat |
| nP | zheap | variable,
nat → zheap → bool |
| nP | iter-n | variable,
nat → heap → bool |
| nat | nat-basic | sort,
|
| nat-list | nat-list-set | sort,
|
| nat-set | nat-store | sort,
|
| nat-set | nat-set | sort,
|
| nat-set | nat-list-set | sort,
|
| nd | node | variable,
node |
| nd0 | node | variable,
node |
| nd1 | node | variable,
node |
| nd2 | node | variable,
node |
| nd3 | node | variable,
node |
| ndx | node-list | variable,
node-list |
| ndx0 | node-list | variable,
node-list |
| ndx1 | node-list | variable,
node-list |
| ndy | node-list | variable,
node-list |
| ndz | node-list | variable,
node-list |
| negdentry | dentry | function,
string → dentry |
| new | aubifs-base | predicate,
address-list × node-store |
| node | node | sort,
|
| node-closed | aubifs-inv | predicate,
node × node-index × node-store × key-set |
| node-cons | aubifs-inv | predicate,
key × node |
| node-index | node-index | sort,
|
| node-list | node-list | sort,
|
| node-status | node-status | sort,
|
| node-store | node-store | sort,
|
| 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 |
| none | restructure | constant,
restructure |
| ns | nat-store | variable,
nat-set |
| ns | nat-set | variable,
nat-set |
| ns | nat-list-set | variable,
nat-set |
| ns0 | nat-store | variable,
nat-set |
| ns0 | nat-set | variable,
nat-set |
| ns0 | nat-list-set | variable,
nat-set |
| ns1 | nat-store | variable,
nat-set |
| ns1 | nat-set | variable,
nat-set |
| ns1 | nat-list-set | variable,
nat-set |
| ns2 | nat-store | variable,
nat-set |
| ns2 | nat-set | variable,
nat-set |
| ns2 | nat-list-set | variable,
nat-set |
| nsize | zbranch-array-ops | predicate,
nat × node-status |
| nstat | node-status | variable,
node-status |
| null | ref | constant,
ref |
| nused | znode-ops | variable,
nat |
| 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 |
| o | obj | variable,
obj |
| o0 | obj | variable,
obj |
| o1 | obj | variable,
obj |
| oP | zheap | variable,
znode → zheap → bool |
| oP | maplet | variable,
obj → heap → bool |
| obj | obj | sort,
|
| ok | node-status | constant,
node-status |
| orphans | aubifs-inv | function,
node-store × node-index → key-set |
| overflow | restructure | function,
key × ref → restructure |
| overfull? | node-status | constant,
node-status |
| payload | zbranch-array-ops | function,
zbranch-array × nat × nat → node-index |
| persistence-state | persistence-state | sort,
|
| pos | list-del | function,
elem × 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 | node-list | function,
node × node-list → nat |
| pos | nat-list-set | function,
nat × nat-list → nat |
| pos | address-list-set | function,
address × address-list → nat |
| pos | key-list-set | function,
key × key-list → nat |
| pos | string | function,
char × string → nat |
| precise | zheap | predicate,
zheap → bool |
| precise | heap-sep | predicate,
heap → bool |
| prefixn | list-prefixn | function,
nat × list → list |
| prefixn | laddress-list | function,
nat × laddress-list → laddress-list |
| prefixn | group-store | function,
nat × group-node-list → group-node-list |
| prefixn | index-store | function,
nat × index-node-list → index-node-list |
| prefixn | node-list | function,
nat × node-list → node-list |
| prefixn | nat-list-set | function,
nat × nat-list → nat-list |
| prefixn | address-list-set | function,
nat × address-list → address-list |
| prefixn | key-list-set | function,
nat × key-list → key-list |
| pstate | persistence-state | variable,
persistence-state |
| r | ref | variable,
ref |
| r0 | ref | variable,
ref |
| r1 | ref | variable,
ref |
| rP | zheap | variable,
ref → zheap → bool |
| rP | maplet | variable,
ref → heap → bool |
| range | aubifs-base | function,
node-index → address-set |
| range= | array-splice | predicate,
array × nat × array × nat × nat |
| range= | buffer | predicate,
buffer × nat × buffer × nat × nat |
| rc | zbranch-array-ops | variable,
ref |
| readonly | persistence-state | constant,
persistence-state |
| ref | ref | sort,
|
| refset | refset | sort,
|
| refsize-cons | group-store | predicate,
group-store × address-set |
| refsize-cons | index-store | predicate,
index-store × address-set |
| refsize-cons | ablock-store-refsize-cons | predicate,
store × address-set |
| remove | modification | function,
key → modification |
| 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 |
| resize | array-splice | function,
array × nat → array |
| resize | buffer | function,
buffer × nat → buffer |
| restn | list-del | partial function,
nat × list → 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 | node-list | partial function,
nat × node-list → node-list |
| restn | nat-list-set | partial function,
nat × nat-list → nat-list |
| restn | address-list-set | partial function,
nat × address-list → address-list |
| restn | key-list-set | partial function,
nat × key-list → key-list |
| restn | string | partial function,
nat × string → string |
| restructure | restructure | sort,
|
| rev | zbranch-array | partial function,
zbranch-array × nat → zbranch-array |
| rev | zbranch-array | function,
zbranch-array → zbranch-array |
| rev | array-copy | partial function,
array × nat → array |
| rev | array-copy | function,
array → array |
| rev | list-last | function,
list → list |
| rev | laddress-list | function,
laddress-list → laddress-list |
| rev | buffer | partial function,
buffer × nat → buffer |
| rev | buffer | function,
buffer → buffer |
| rev | group-store | function,
group-node-list → group-node-list |
| rev | index-store | function,
index-node-list → index-node-list |
| rev | branch-array | partial function,
branch-array × nat → branch-array |
| rev | branch-array | function,
branch-array → branch-array |
| rev | node-list | function,
node-list → node-list |
| rev | nat-list-set | function,
nat-list → nat-list |
| rev | address-list-set | function,
address-list → address-list |
| rev | key-list-set | function,
key-list → key-list |
| rev | address-set-array | partial function,
address-set-array × nat → address-set-array |
| rev | address-set-array | function,
address-set-array → address-set-array |
| rev | string | function,
string → string |
| ri | node-index | variable,
node-index |
| ri-closed | aubifs-inv | predicate,
node-index × node-store × key-set |
| ri-cons | aubifs-inv | predicate,
node-index × node-store |
| ri-inj | aubifs-inv | predicate,
node-index |
| ri0 | node-index | variable,
node-index |
| ri1 | node-index | variable,
node-index |
| ri2 | node-index | variable,
node-index |
| rmdup | list-dup | function,
list → 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 | node-list | function,
node-list → node-list |
| rmdup | nat-list-set | function,
nat-list → nat-list |
| rmdup | address-list-set | function,
address-list → address-list |
| rmdup | key-list-set | function,
key-list → key-list |
| rmdup | string | function,
string → string |
| ro | aubifs-base | variable,
key-set |
| ro0 | aubifs-base | variable,
key-set |
| ro1 | aubifs-base | variable,
key-set |
| ro2 | aubifs-base | variable,
key-set |
| rp | zbranch-array-ops | variable,
ref |
| rrP | zheap | variable,
ref × ref → zheap → bool |
| rrP | maplet | variable,
ref × ref → heap → bool |
| rs | refset | variable,
refset |
| rs0 | refset | variable,
refset |
| rs1 | refset | variable,
refset |
| rs2 | refset | variable,
refset |
| rst | restructure | variable,
restructure |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| save | znode-ops | function,
zbranch → branch |
| save | znode-ops | function,
zbranch-array × nat × nat → branch-array |
| save | znode-ops | function,
znode → index-node |
| scan | znode-ops | function,
key × zbranch-array × nat × nat → nat |
| set | set-basic | sort,
|
| shl | znode-ops | function,
zbranch-array × nat × nat → zbranch-array |
| shr | znode-ops | function,
zbranch-array × nat × nat → zbranch-array |
| slice | list-prefixn | function,
nat × nat × list → list |
| slice | laddress-list | function,
nat × nat × laddress-list → laddress-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 |
| slice | node-list | function,
nat × nat × node-list → node-list |
| slice | nat-list-set | function,
nat × nat × nat-list → nat-list |
| slice | address-list-set | function,
nat × nat × address-list → address-list |
| slice | key-list-set | function,
nat × nat × key-list → key-list |
| sorted | zbranch-array-sorted | predicate,
zbranch-array × nat × nat |
| sortedchars | string-less | constant,
string |
| splice | array-splice | function,
array × nat × array × nat × nat → array |
| splice | buffer | function,
buffer × nat × buffer × nat × nat → buffer |
| st | store | variable,
store |
| st0 | store | variable,
store |
| st1 | store | variable,
store |
| st2 | store | variable,
store |
| store | store | sort,
|
| store | modification | function,
key × address → modification |
| str | string | variable,
string |
| str0 | string | variable,
string |
| str1 | string | variable,
string |
| str2 | string | variable,
string |
| str3 | string | variable,
string |
| string | string | sort,
|
| strings | stringset | variable,
stringset |
| strings0 | stringset | variable,
stringset |
| strings1 | stringset | variable,
stringset |
| strings2 | stringset | variable,
stringset |
| stringset | stringset | sort,
|
| subarray | zbranch-array | partial function,
zbranch-array × nat × nat → zbranch-array |
| subarray | array-copy | partial function,
array × nat × nat → array |
| subarray | buffer | partial function,
buffer × nat × nat → buffer |
| subarray | branch-array | partial function,
branch-array × nat × nat → branch-array |
| subarray | address-set-array | partial function,
address-set-array × nat × nat → address-set-array |
| sublist | list-del | partial function,
nat × nat × list → 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 | node-list | partial function,
nat × nat × node-list → node-list |
| sublist | nat-list-set | partial function,
nat × nat × nat-list → nat-list |
| sublist | address-list-set | partial function,
nat × nat × address-list → address-list |
| sublist | key-list-set | partial function,
nat × nat × key-list → key-list |
| sublist | string | partial function,
nat × nat × string → string |
| syn | apersistence-base | variable,
bool |
| true | zheap | predicate,
zheap |
| true | heap-sep | predicate,
heap |
| truncnode | node | function,
key × nat → node |
| ubifs-cons | aubifs-inv | predicate,
node-store × node-index × key-set × node-index × key-set × address-list |
| unbuffered | persistence-state | constant,
persistence-state |
| underflow | restructure | constant,
restructure |
| underfull? | node-status | constant,
node-status |
| union | address-set-array-ops | function,
address-set-array × nat × nat → address-set |
| unmodified | zbranch-array-ops | predicate,
address × znode × index-address-store |
| valid-adrs | ablock-store-refsize-cons | predicate,
address-set |
| valid-dentry | aubifs-base | predicate,
nat × dentry × node-store × node-index × key-set |
| valid-dentry | aubifs-base | predicate,
dentry × node-store × node-index × key-set |
| valid-dir-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-file-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-negdentry | aubifs-base | predicate,
nat × dentry × node-store × node-index × key-set |
| valid-parent-ino | aubifs-base | predicate,
nat × node-store × node-index × key-set |
| 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 |
| zbr | zbranch | variable,
zbranch |
| zbr0 | zbranch-array | variable,
zbranch |
| zbr1 | zbranch-array | variable,
zbranch |
| zbranch | zbranch | sort,
|
| zbranch-array | zbranch-array | sort,
|
| zbrar | zbranch-array | variable,
zbranch-array |
| zbrar0 | zbranch-array | variable,
zbranch-array |
| zbrar1 | zbranch-array | variable,
zbranch-array |
| zbrar2 | zbranch-array | variable,
zbranch-array |
| zero | array-splice | constant,
elem |
| zero | buffer | constant,
data |
| zeropage | page | constant,
buffer |
| zh | zheap | variable,
zheap |
| zh0 | zheap | variable,
zheap |
| zh1 | zheap | variable,
zheap |
| zh2 | zheap | variable,
zheap |
| zheap | zheap | sort,
|
| znd | znode | variable,
znode |
| znd0 | zheap | variable,
znode |
| znd1 | zheap | variable,
znode |
| znode | znode | sort,
|
| | | store+set | function,
store × set → store |
| | | node-index | function,
node-index × key-set → node-index |
| | | nat-store | function,
store × nat-set → store |
| | | 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 |
| | | node-store | function,
node-store × address-set → node-store |
| | | ablock-store-refsize-cons | function,
address-set × nat → address-set |
| | | address-store | function,
address-store × address-set → address-store |
| |> | node-index-restrict | function,
node-index × key → node-index |
| |≤ | node-index-restrict | function,
node-index × key → node-index |
| } | zheap | function,
zheap → zheap → bool |
| } | refset | function,
ref → refset |
| } | set-union | function,
elem → set |
| } | heap-sep | function,
heap → heap → bool |
| } | stringset | function,
string → stringset |
| } | node-index | function,
key → key-set |
| } | nat-store | function,
nat → nat-set |
| } | nat-set | function,
nat → nat-set |
| } | node-store | function,
address → address-set |
| } | nat-list-set | function,
nat → nat-set |
| } | address-list-set | function,
address → address-set |
| } | key-list-set | function,
key → key-set |
| } | address-store | function,
address → address-set |
| ¬ | zheap | function,
zheap → bool → zheap → bool |
| ¬ | heap-sep | function,
heap → bool → heap → bool |
| → | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| → | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| ∅ | zheap | constant,
zheap |
| ∅ | heap | constant,
heap |
| ∅ | refset | constant,
refset |
| ∅ | set-basic | constant,
set |
| ∅ | store | constant,
store |
| ∅ | stringset | constant,
stringset |
| ∅ | node-index | constant,
key-set |
| ∅ | node-index | constant,
node-index |
| ∅ | nat-store | constant,
nat-set |
| ∅ | nat-set | 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 |
| ∅ | node-store | constant,
address-set |
| ∅ | node-store | constant,
node-store |
| ∅ | nat-list-set | constant,
nat-set |
| ∅ | address-list-set | constant,
address-set |
| ∅ | key-list-set | constant,
key-set |
| ∅ | address-store | constant,
address-set |
| ∅ | address-store | constant,
address-store |
| ∈ | zheap | predicate,
ref × zheap |
| ∈ | zbranch-array | predicate,
zbranch × zbranch-array |
| ∈ | heap | predicate,
ref × heap |
| ∈ | refset | predicate,
ref × refset |
| ∈ | store+set | predicate,
data × store |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | store | predicate,
elem × store |
| ∈ | stringset | predicate,
string × stringset |
| ∈ | array-copy | predicate,
elem × array |
| ∈ | list | predicate,
elem × list |
| ∈ | node-index | predicate,
address × node-index |
| ∈ | node-index | predicate,
key × key-set |
| ∈ | node-index | predicate,
key × node-index |
| ∈ | nat-store | predicate,
nat × nat-set |
| ∈ | nat-store | predicate,
nat × store |
| ∈ | nat-set | predicate,
nat × nat-set |
| ∈ | laddress-list | predicate,
laddress × laddress-list |
| ∈ | ablock-store | predicate,
ablock × store |
| ∈ | buffer | predicate,
data × buffer |
| ∈ | 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 |
| ∈ | node-store | predicate,
node × node-store |
| ∈ | node-store | predicate,
address × address-set |
| ∈ | node-store | predicate,
address × node-store |
| ∈ | branch-array | predicate,
branch × branch-array |
| ∈ | node-list | predicate,
node × node-list |
| ∈ | nat-list-set | predicate,
nat × nat-set |
| ∈ | nat-list-set | predicate,
nat × nat-list |
| ∈ | address-list-set | predicate,
address × address-set |
| ∈ | address-list-set | predicate,
address × address-list |
| ∈ | key-list-set | predicate,
key × key-set |
| ∈ | key-list-set | predicate,
key × key-list |
| ∈ | address-set-array | predicate,
address-set × address-set-array |
| ∈ | address-store | predicate,
elem × address-store |
| ∈ | address-store | predicate,
address × address-set |
| ∈ | address-store | predicate,
address × address-store |
| ∈ | string | predicate,
char × string |
| ∧ | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| ∧ | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| ∨ | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| ∨ | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| ∩ | refset | function,
refset × refset → refset |
| ∩ | set-union | function,
set × set → set |
| ∩ | stringset | function,
stringset × stringset → stringset |
| ∩ | node-index | function,
key-set × key-set → key-set |
| ∩ | nat-store | function,
nat-set × nat-set → nat-set |
| ∩ | nat-set | function,
nat-set × nat-set → nat-set |
| ∩ | node-store | function,
address-set × address-set → address-set |
| ∩ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∩ | address-list-set | function,
address-set × address-set → address-set |
| ∩ | key-list-set | function,
key-set × key-set → key-set |
| ∩ | address-store | function,
address-set × address-set → address-set |
| ∪ | zheap | function,
zheap × zheap → zheap |
| ∪ | heap | function,
heap × heap → heap |
| ∪ | refset | function,
refset × refset → refset |
| ∪ | set-union | function,
set × set → set |
| ∪ | stringset | function,
stringset × stringset → stringset |
| ∪ | node-index | function,
key-set × key-set → key-set |
| ∪ | nat-store | function,
nat-set × nat-set → nat-set |
| ∪ | nat-set | function,
nat-set × nat-set → nat-set |
| ∪ | node-store | function,
address-set × address-set → address-set |
| ∪ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∪ | address-list-set | function,
address-set × address-set → address-set |
| ∪ | key-list-set | function,
key-set × key-set → key-set |
| ∪ | address-store | function,
address-set × address-set → address-set |
| ≡ | zheap | predicate,
zheap × zheap |
| ≡ | separation | predicate,
heap × heap |
| ≡ | btree-inv | predicate,
zheap → bool × zheap → bool |
| ≤ | nat | predicate,
nat × nat |
| ≤ | zbranch-array-sorted | predicate,
key × key |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | zheap | predicate,
zheap → bool × zheap → bool |
| ⊆ | zheap | predicate,
zheap × zheap |
| ⊆ | heap | predicate,
heap × heap |
| ⊆ | refset | predicate,
refset × refset |
| ⊆ | set-basic | predicate,
set × set |
| ⊆ | store | predicate,
store × store |
| ⊆ | heap-sep | predicate,
heap → bool × heap → bool |
| ⊆ | stringset | predicate,
stringset × stringset |
| ⊆ | node-index | predicate,
key-set × key-set |
| ⊆ | node-index | predicate,
node-index × node-index |
| ⊆ | nat-store | predicate,
nat-set × nat-set |
| ⊆ | nat-set | 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 |
| ⊆ | node-store | predicate,
address-set × address-set |
| ⊆ | node-store | predicate,
node-store × node-store |
| ⊆ | nat-list-set | predicate,
nat-set × nat-set |
| ⊆ | address-list-set | predicate,
address-set × address-set |
| ⊆ | key-list-set | predicate,
key-set × key-set |
| ⊆ | address-store | predicate,
address-set × address-set |
| ⊆ | address-store | predicate,
address-store × address-store |
| ⊏ | string | predicate,
string × string |
| ⊑ | list-last | predicate,
list × 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 |
| ⊑ | node-list | predicate,
node-list × node-list |
| ⊑ | nat-list-set | predicate,
nat-list × nat-list |
| ⊑ | address-list-set | predicate,
address-list × address-list |
| ⊑ | key-list-set | predicate,
key-list × key-list |
| ⊑ | string | predicate,
string × string |
| ⊒ | list-last | predicate,
list × 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 |
| ⊒ | node-list | predicate,
node-list × node-list |
| ⊒ | nat-list-set | predicate,
nat-list × nat-list |
| ⊒ | address-list-set | predicate,
address-list × address-list |
| ⊒ | key-list-set | predicate,
key-list × key-list |
| ⊒ | string | predicate,
string × string |
| ⊕ | store+set | function,
store × store → store |
| ⊕ | node-index | function,
node-index × node-index → node-index |
| ⊕ | 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 |
| ⊕ | node-store | function,
node-store × node-store → node-store |
| ⊕ | address-store | function,
address-store × address-store → address-store |
| ⊖ | aubifs-base | function,
node-index × key-set → node-index |
| ⊖ | aubifs-base | function,
node-index × key → node-index |
| ⊗ | zheap | function,
zheap → bool × zheap → bool → zheap → bool |
| ⊗ | heap-sep | function,
heap → bool × heap → bool → heap → bool |
| ⊗_ | zheap | function,
nat → zheap → bool × nat × nat → zheap → bool |
| ⊗_ | iter-n | function,
nat → heap → bool × nat × nat → heap → bool |
| ⊥ | zheap | predicate,
zheap × zheap |
| ⊥ | heap | predicate,
heap × heap |
| ⌋ | error-class | predicate,
error |
| ⌝ | zheap | function,
bool → zheap → bool |
| ⌝ | heap-sep | function,
bool → heap → bool |