| Symbol | Specification | Kind | Type |
|---|
| # . | buffer | f | buffer → nat |
| # . | laddress-list | f | laddress-list → nat |
| # . | string | f | string → nat |
| # . | encoding-group-node | f | group-node-list → nat |
| # . | avolume | f | avolume → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | laddress-list | f | laddress → laddress-list |
| . ' | string | f | char → string |
| . ' | encoding-group-node | f | group-node → group-node-list |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | laddress-list | f | laddress-list × laddress → laddress-list |
| . + . | string | f | char × string → string |
| . + . | laddress-list | f | laddress-list × laddress-list → laddress-list |
| . + . | string | f | string × string → string |
| . + . | laddress-list | f | laddress × laddress-list → laddress-list |
| . + . | string | f | string × char → string |
| . + . | encoding-group-node | f | group-node-list × group-node → group-node-list |
| . + . | avolume | f | avolume × avolume → avolume |
| . + . | encoding-group-node | f | group-node-list × group-node-list → group-node-list |
| . + . | encoding-group-node | f | group-node × group-node-list → group-node-list |
| . ++ . | laddress-list | f | laddress-list × laddress → laddress-list |
| . ++ . | string | f | string × char → string |
| . ++ . | encoding-group-node | f | group-node-list × group-node → group-node-list |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | string | f | char × char → string |
| . +2 . | encoding-group-node | f | group-node × group-node → group-node-list |
| . +2 . | laddress-list | f | laddress × laddress → laddress-list |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | string | f | string × char → string |
| . -1l . | laddress-list | f | laddress-list × laddress → laddress-list |
| . -1l . | encoding-group-node | f | group-node-list × group-node → group-node-list |
| . -l . | string | f | string × char → string |
| . -l . | encoding-group-node | f | group-node-list × group-node → group-node-list |
| . -l . | laddress-list | f | laddress-list × laddress → laddress-list |
| . -p . | laddress-list | f | laddress-list × nat → laddress-list |
| . -p . | string | f | string × nat → string |
| . -p . | encoding-group-node | f | group-node-list × nat → group-node-list |
| . .align↓ | awbuf-inv | f | buffer → buffer |
| . .align↓ | awbuf-inv | f | avolume → avolume |
| . .alignedsize | encoding-group-node | f | group-node → nat |
| . .butlast | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . .butlast | encoding-group-node | pf | group-node-list → group-node-list with λ gndx. gndx ≠ [] |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .char1 | string | pf | string → char with λ str. str ≠ "" |
| . .data | node | pf | node → buffer with λ nd. nd.data? |
| . .data | aleb | pf | aleb → buffer with λ aleb. aleb.mapped? |
| . .data:= . | aleb | pf | aleb × buffer → aleb with λ aleb, buf. aleb.mapped? |
| . .data:= . | node | pf | node × buffer → node with λ nd, buf. nd.data? |
| . .data? | key | p | key |
| . .data? | node | p | node |
| . .dentry? | key | p | key |
| . .dentry? | node | p | node |
| . .directory | node | pp | node with λ nd. nd.inode? |
| . .directory:= . | node | pf | node × bool → node with λ nd, boolvar. nd.inode? |
| . .end | groupnode | p | group-node |
| . .end:= . | groupnode | f | group-node × bool → group-node |
| . .flags | lprops | f | lprops → lpropflags |
| . .flags:= . | lprops | f | lprops × lpropflags → lprops |
| . .flashsize | encoding-group-node | f | group-node → nat |
| . .flashsize | encoding-group-node | f | group-node-list → nat |
| . .gcheapidx | lprops | f | lprops → nat |
| . .gcheapidx:= . | lprops | f | lprops × nat → lprops |
| . .gndlist | encoding-group-node | f | group-block → group-node-list |
| . .gndlist:= . | encoding-group-node | f | group-block × group-node-list → group-block |
| . .head | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .head | encoding-group-node | pf | group-node-list → group-node with λ gndx. gndx ≠ [] |
| . .ino | key | f | key → nat |
| . .ino | node | pf | node → nat with λ nd. nd.dentry? |
| . .ino:= . | key | f | key × nat → key |
| . .ino:= . | node | pf | node × nat → node with λ nd, m. nd.dentry? |
| . .inode? | key | p | key |
| . .inode? | node | p | node |
| . .isbuf? | bufleb | p | bufleb |
| . .ispadding | node-header | p | node-header |
| . .ispadding:= . | node-header | f | node-header × bool → node-header |
| . .key | node | f | node → key |
| . .key:= . | node | f | node × key → node |
| . .ladrlist | encoding-group-node | f | group-block → laddress-list |
| . .ladrlist:= . | encoding-group-node | f | group-block × laddress-list → group-block |
| . .last | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .last | encoding-group-node | pf | group-node-list → group-node with λ gndx. gndx ≠ [] |
| . .last | string | pf | string → char with λ str. str ≠ "" |
| . .leb | bufleb | pf | bufleb → nat with λ bleb. bleb.isbuf? |
| . .mapped? | aleb | p | aleb |
| . .meta | node | pf | node → metadata with λ nd. nd.inode? |
| . .meta:= . | node | pf | node × metadata → node with λ nd, md. nd.inode? |
| . .name | key | pf | key → string with λ key. key.dentry? |
| . .name:= . | key | pf | key × string → key with λ key, str. key.dentry? |
| . .nd | groupnode | f | group-node → node |
| . .nd:= . | groupnode | f | group-node × node → group-node |
| . .nlink | node | pf | node → nat with λ nd. nd.inode? |
| . .nlink:= . | node | pf | node × nat → node with λ nd, m. nd.inode? |
| . .nsubdirs | node | pf | node → nat with λ nd. nd.inode? |
| . .nsubdirs:= . | node | pf | node × nat → node with λ nd, m. nd.inode? |
| . .off | laddress | f | laddress → nat |
| . .off:= . | laddress | f | laddress × nat → laddress |
| . .part | key | pf | key → nat with λ key. key.data? |
| . .part:= . | key | pf | key × nat → key with λ key, m. key.data? |
| . .ref-size | lprops | f | lprops → nat |
| . .ref-size | encoding-group-node | f | group-block → nat |
| . .ref-size:= . | lprops | f | lprops × nat → lprops |
| . .ref-size:= . | encoding-group-node | f | group-block × nat → group-block |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .size | node-header | f | node-header → nat |
| . .size | node | pf | node → nat with λ nd. nd.trunc? ∨ nd.inode? |
| . .size | laddress | f | laddress → nat |
| . .size | lprops | f | lprops → nat |
| . .size:= . | node | pf | node × nat → node with λ nd, m. nd.trunc? ∨ nd.inode? |
| . .size:= . | node-header | f | node-header × nat → node-header |
| . .size:= . | lprops | f | lprops × nat → lprops |
| . .size:= . | laddress | f | laddress × nat → laddress |
| . .sqnum | groupnode | f | group-node → nat |
| . .sqnum:= . | groupnode | f | group-node × nat → group-node |
| . .start | groupnode | p | group-node |
| . .start:= . | groupnode | f | group-node × bool → group-node |
| . .tail | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . .tail | encoding-group-node | pf | group-node-list → group-node-list with λ gndx. gndx ≠ [] |
| . .toString | debug | f | nat → string |
| . .trunc? | node | p | node |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . < . | laddress-list | p | laddress-list × laddress-list |
| . < . | encoding-group-node | p | group-node-list × group-node-list |
| . > . | nat | p | nat × nat |
| . [ . ] | laddress-list | pf | laddress-list × nat × laddress → laddress-list with λ lax, n, ladr. n < # lax |
| . [ . ] | laddress-list | pf | laddress-list × nat → laddress with λ lax, n. n < # lax |
| . [ . ] | encoding-group-node | pf | group-node-list × nat × group-node → group-node-list with λ gndx, n, gnd. n < # gndx |
| . [ . ] | encoding-group-node | pf | group-node-list × nat → group-node with λ gndx, n. n < # gndx |
| . [ . ] | avolume | pf | avolume × nat × aleb → avolume with λ avol, n, aleb. n < # avol |
| . [ . ] | avolume | pf | avolume × nat → aleb with λ avol, n. n < # avol |
| . [ . ] | string | pf | string × nat × char → string with λ str, n, char. n < # str |
| . [ . ] | string | pf | string × nat → char with λ str, n. n < # str |
| . [ . ] | buffer | pf | buffer × nat × data → buffer with λ buf, n, d. n < # buf |
| . [ . ] | buffer | pf | buffer × nat → data with λ buf, n. n < # buf |
| . ↓ . | awbuf-inv | p | aleb × aleb |
| . ↓ . | awbuf-inv | p | avolume × avolume |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | laddress-list | p | laddress × laddress-list |
| . ∈ . | string | p | char × string |
| . ∈ . | encoding-group-node | p | group-node × group-node-list |
| . ∈ . | avolume | p | aleb × avolume |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | laddress-list | p | laddress-list × laddress-list |
| . ⊑ . | string | p | string × string |
| . ⊑ . | encoding-group-node | p | group-node-list × group-node-list |
| . ⊒ . | laddress-list | p | laddress-list × laddress-list |
| . ⊒ . | string | p | string × string |
| . ⊒ . | encoding-group-node | p | group-node-list × group-node-list |
| @ | laddress | f | nat × nat → laddress |
| [] | encoding-group-node | c | group-node-list |
| [] | laddress-list | c | laddress-list |
| ⊏ | string | p | string × string |
| ⌊ . ⌋ | error-class | p | error |
| ALIGNEDSIZE | encoding-node-base | v | nat,flexible |
| BUF | encoding-node-base | v | buffer,flexible |
| Boolvar | encoding-node-header | v | bool,flexible |
| EACCESS | error | c | error |
| EB_PAGE_SIZE | eraseblock | c | nat |
| EBADFD | error | c | error |
| ECOMMIT | error | c | error |
| EEXISTS | error | c | error |
| EFAIL | error | c | error |
| EINVAL | error | c | error |
| EIO | error | c | error |
| EISDIR | error | c | error |
| ENOENT | error | c | error |
| ENOMEM | error | c | error |
| ENOSPC | error | c | error |
| ENOTDIR | error | c | error |
| ENOTEMPTY | error | c | error |
| EROFS | error | c | error |
| ERR | error-class | v | error,flexible |
| ERR0 | error-class | v | error,flexible |
| ESUCCESS | error | c | error |
| EUCLEAN | error | c | error |
| GND | encoding-group-node | v | group-node,flexible |
| ISPAD | encoding-node-base | v | bool,flexible |
| LEB_SIZE | eraseblock | c | nat |
| LP_FREE | lprops | c | lpropflags |
| LP_GROUP_NODES | lprops | c | lpropflags |
| LP_INDEX_NODES | lprops | c | lpropflags |
| NDHD | encoding-node-base | v | node-header,flexible |
| NDSIZE | encoding-node-base | v | nat,flexible |
| NODE_HEADER_SIZE | node-header-size | c | nat |
| OFFSET | encoding-node-base | v | nat,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PEB_SIZE | eraseblock | c | nat |
| SIZE | encoding-node-base | v | nat,flexible |
| SIZE0 | encoding-node-base | v | nat,flexible |
| TRAILER | encoding-node-base | v | buffer,flexible |
| VFS_PAGE_SIZE | page | c | nat |
| abs-failed | abs-node | p | buffer |
| abs-leb | encoding-group-node | p | aleb × group-block × lprops |
| abs-node | encoding-group-node | p | buffer × group-node |
| abs-nodes | encoding-group-node | p | buffer × nat × group-node-list × laddress-list × bool |
| abs-nodes | encoding-group-node | p | buffer × group-node-list × laddress-list × bool |
| abs-padding | abs-node | p | buffer |
| aleb | aleb | s | |
| aleb | aleb | v | aleb |
| aleb0 | avolume | v | aleb |
| aleb1 | avolume | v | aleb |
| align↑ | align | f | nat × nat → nat |
| align↓ | align | f | nat × nat → nat |
| avol | avolume | v | avolume |
| avol0 | avolume | v | avolume |
| avol1 | avolume | v | avolume |
| avol2 | avolume | v | avolume |
| avolume | avolume | s | |
| awbuf-inv | awbuf-inv | p | avolume × bufleb |
| bleb | bufleb | v | bufleb |
| boolvar | node-header | v | bool |
| boolvar0 | node-header | v | bool |
| boolvar1 | groupnode | v | bool |
| boolvar2 | groupnode | v | bool |
| buf | buffer | v | buffer |
| buf0 | buffer | v | buffer |
| buf1 | buffer | v | buffer |
| buf2 | buffer | v | buffer |
| buffer | buffer | s | |
| buffered | bufleb | f | nat → bufleb |
| bufleb | bufleb | s | |
| butlastn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| butlastn | encoding-group-node | pf | nat × group-node-list → group-node-list with λ n, gndx. n ≤ # gndx |
| butlastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| char | char | s | |
| char | char | v | char |
| char0 | char | v | char |
| char1 | char | v | char |
| char2 | char | v | char |
| cmp | avolume | pp | avolume × aleb × nat × nat with λ avol, aleb, m, n. m + n ≤ # avol |
| cmp | avolume | pp | avolume × nat × avolume × nat × nat with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| cmp | buffer | pp | buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf |
| cmp | buffer | pp | buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | avolume | pf | avolume × nat × avolume × nat × nat → avolume with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| d | data | v | data |
| d0 | data | v | data |
| d1 | data | v | data |
| d2 | data | v | data |
| data | data | s | |
| datakey | key | f | nat × nat → key |
| datanode | node | f | key × buffer → node |
| debug# | debug | pr | string : |
| decode_group_node# | encoding-group-node | pr | nat × nat × buffer : group-node : error (nondeterministic) |
| decode_group_node_headerless# | encoding-group-node | pr | nat × buffer : group-node × nat : error (nondeterministic) |
| decode_header# | encoding-node-header | pr | nat × buffer : node-header : error (nondeterministic) |
| decode_header_empty# | encoding-node-header | pr | nat × buffer : node-header × nat : error (nondeterministic) |
| dentrykey | key | f | nat × string → key |
| dentrynode | node | f | key × nat → node |
| disj | laddress-list | p | laddress-list × laddress-list |
| disj | encoding-group-node | p | group-node-list × group-node-list |
| disj | string | p | string × string |
| dropn | encoding-group-node | f | nat × group-node-list → group-node-list |
| dropn | laddress-list | f | nat × laddress-list → laddress-list |
| dups | laddress-list | p | laddress-list |
| dups | string | p | string |
| dups | encoding-group-node | p | group-node-list |
| empty | buffer | c | data |
| empty | avolume | c | aleb |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| encode_group_node# | encoding-group-node | pr | group-node × nat : nat × buffer : error (nondeterministic) |
| encode_group_node_headerless# | encoding-group-node | pr | group-node × nat : buffer × nat : error (nondeterministic) |
| encode_header# | encoding-node-header | pr | node-header × nat : buffer : error (nondeterministic) |
| encode_header_empty# | encoding-node-header | pr | node-header × nat : buffer × nat : error (nondeterministic) |
| encoding-size | encoding-node-header | f | node-header → nat |
| err | error | v | error |
| err0 | error | v | error |
| err1 | error | v | error |
| error | error | s | |
| fail# | error-class | pr | : : error (nondeterministic) |
| fail_or_success# | error-class | pr | : : error (nondeterministic) |
| fill | avolume | pf | avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol |
| fill | buffer | f | buffer × data → buffer |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fill | avolume | f | avolume × aleb → avolume |
| fillfirst | string | f | nat × char × string → string |
| fillfirst | laddress-list | f | nat × laddress × laddress-list → laddress-list |
| fillfirst | encoding-group-node | f | nat × group-node × group-node-list → group-node-list |
| firstn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| firstn | encoding-group-node | pf | nat × group-node-list → group-node-list with λ n, gndx. n ≤ # gndx |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| frome | string | f | string × char → string |
| frome | encoding-group-node | f | group-node-list × group-node → group-node-list |
| frome | laddress-list | f | laddress-list × laddress → laddress-list |
| gblock | encoding-group-node | v | group-block |
| gnd | groupnode | v | group-node |
| gnd0 | encoding-group-node | v | group-node |
| gnd1 | encoding-group-node | v | group-node |
| gnd2 | encoding-group-node | v | group-node |
| gnd3 | encoding-group-node | v | group-node |
| gnd4 | encoding-group-node | v | group-node |
| gnd5 | encoding-group-node | v | group-node |
| gndx | encoding-group-node | v | group-node-list |
| gndx0 | encoding-group-node | v | group-node-list |
| gndx1 | encoding-group-node | v | group-node-list |
| gndx3 | encoding-group-node | v | group-node-list |
| gndx7 | encoding-group-node | v | group-node-list |
| group-block | encoding-group-node | s | |
| group-node | groupnode | s | |
| group-node-list | encoding-group-node | s | |
| group-node-size-headerless | encoding-group-node | f | group-node → nat |
| groupblock | encoding-group-node | f | group-node-list × laddress-list × nat → group-block |
| id○ | avolume | p | avolume × avolume × nat |
| id○ | buffer | p | buffer × buffer × nat |
| idrange | avolume | pp | avolume × nat × nat with λ avol, m, n. m + n ≤ # avol |
| idrange | buffer | pp | buffer × nat × nat with λ buf, m, n. m + n ≤ # buf |
| inodekey | key | f | nat → key |
| inodenode | node | f | key × metadata × bool × nat × nat × nat → node |
| is-aligned | align | p | nat × nat |
| is-encoded | encoding-node-header | p | node-header × buffer |
| is-encoded | encoding-group-node | p | group-node × buffer |
| is-encoded-empty | encoding-node-header | p | node-header × buffer |
| is-garbage | encoding | p | buffer |
| is-garbage-header | encoding-node-header | p | buffer |
| is-garbage-rnode-empty | encoding-node-header | p | buffer |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| ispad | encoding-node-base | v | bool |
| isvalidtrailer | node-header-size | p | buffer |
| key | key | s | |
| key | key | v | key |
| key0 | node | v | key |
| laddress | laddress | s | |
| laddress-list | laddress-list | s | |
| ladr | laddress | v | laddress |
| ladr0 | laddress-list | v | laddress |
| ladr1 | laddress-list | v | laddress |
| ladr2 | laddress-list | v | laddress |
| lastn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| lastn | encoding-group-node | pf | nat × group-node-list → group-node-list with λ n, gndx. n ≤ # gndx |
| lastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| lax | laddress-list | v | laddress-list |
| lax0 | laddress-list | v | laddress-list |
| lax1 | laddress-list | v | laddress-list |
| lax2 | laddress-list | v | laddress-list |
| lax3 | laddress-list | v | laddress-list |
| lp | lprops | v | lprops |
| lp0 | lprops | v | lprops |
| lpf | lprops | v | lpropflags |
| lpf0 | lprops | v | lpropflags |
| lpropflags | lprops | s | |
| lprops | lprops | s | |
| m | nat-basic | v | nat |
| m0 | lprops | v | nat |
| m1 | lprops | v | nat |
| m2 | lprops | v | nat |
| m3 | lprops | v | nat |
| m4 | lprops | v | nat |
| mapped | aleb | f | buffer → aleb |
| max | min-max | f | nat × nat → nat |
| md | metadata | v | metadata |
| md0 | node | v | metadata |
| metadata | metadata | s | |
| min | min-max | f | nat × nat → nat |
| mkavolume | avolume | f | nat → avolume |
| mkbuf | buffer | f | nat → buffer |
| mkemparray | avolume | f | nat → avolume |
| mkempbuf | buffer | f | nat → buffer |
| mkgnode | groupnode | f | node × nat × bool × bool → group-node |
| mklist | laddress-list | f | laddress × nat → laddress-list |
| mklist | string | f | char × nat → string |
| mklist | encoding-group-node | f | group-node × nat → group-node-list |
| mklp | lprops | f | nat × nat × lpropflags × nat → lprops |
| mkzarray | avolume | f | nat → avolume |
| mkzbuf | buffer | f | nat → buffer |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| nd | node | v | node |
| nd0 | node | v | node |
| nd1 | node | v | node |
| nd2 | node | v | node |
| nd3 | node | v | node |
| ndhd | node-header | v | node-header |
| ndhd0 | encoding-node-header | v | node-header |
| ndhd1 | encoding-node-header | v | node-header |
| nobuffer | bufleb | c | bufleb |
| node | node | s | |
| node-header | node-header | s | |
| nodeheader | node-header | f | nat × bool → node-header |
| pos | string | f | char × string → nat |
| pos | laddress-list | f | laddress × laddress-list → nat |
| pos | encoding-group-node | f | group-node × group-node-list → nat |
| prefixn | laddress-list | f | nat × laddress-list → laddress-list |
| prefixn | encoding-group-node | f | nat × group-node-list → group-node-list |
| range= | avolume | p | avolume × nat × avolume × nat × nat |
| range= | buffer | p | buffer × nat × buffer × nat × nat |
| resize | buffer | f | buffer × nat → buffer |
| resize | avolume | f | avolume × nat → avolume |
| restn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| restn | encoding-group-node | pf | nat × group-node-list → group-node-list with λ n, gndx. n ≤ # gndx |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| rev | buffer | f | buffer → buffer |
| rev | avolume | pf | avolume × nat → avolume with λ avol, n. n ≤ # avol |
| rev | buffer | pf | buffer × nat → buffer with λ buf, n. n ≤ # buf |
| rev | laddress-list | f | laddress-list → laddress-list |
| rev | string | f | string → string |
| rev | encoding-group-node | f | group-node-list → group-node-list |
| rev | avolume | f | avolume → avolume |
| rmdup | string | f | string → string |
| rmdup | encoding-group-node | f | group-node-list → group-node-list |
| rmdup | laddress-list | f | laddress-list → laddress-list |
| slice | laddress-list | f | nat × nat × laddress-list → laddress-list |
| slice | encoding-group-node | f | nat × nat × group-node-list → group-node-list |
| splice | buffer | f | buffer × nat × buffer × nat × nat → buffer |
| splice | avolume | f | avolume × nat × avolume × nat × nat → avolume |
| str | string | v | string |
| str0 | string | v | string |
| str1 | string | v | string |
| str2 | string | v | string |
| str3 | string | v | string |
| string | string | s | |
| subarray | avolume | pf | avolume × nat × nat → avolume with λ avol, m, n. m + n ≤ # avol |
| subarray | buffer | pf | buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf |
| sublist | laddress-list | pf | nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax |
| sublist | encoding-group-node | pf | nat × nat × group-node-list → group-node-list with λ n, m, gndx. n + m ≤ # gndx |
| sublist | string | pf | nat × nat × string → string with λ n, m, str. n + m ≤ # str |
| synced | awbuf-inv | p | avolume |
| truncnode | node | f | key × nat → node |
| unmapped | aleb | c | aleb |
| validtrailer | node-header-size | c | buffer |
| weak | abs-list | v | bool |
| zero | buffer | c | data |
| zero | avolume | c | aleb |
| zeropage | page | c | buffer |