| Symbol | Specification | Kind | Type |
|---|
| # . | string | f | string → nat |
| # . | laddress-list | f | laddress-list → nat |
| # . | branch-array | f | branch-array → nat |
| # . | encoding-index-node | f | index-node-list → nat |
| # . | buffer | f | buffer → 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-index-node | f | index-node → index-node-list |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | string | f | char × string → string |
| . + . | laddress-list | f | laddress-list × laddress → laddress-list |
| . + . | string | f | string × string → string |
| . + . | laddress-list | f | laddress-list × laddress-list → laddress-list |
| . + . | string | f | string × char → string |
| . + . | laddress-list | f | laddress × laddress-list → laddress-list |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | encoding-index-node | f | index-node-list × index-node → index-node-list |
| . + . | avolume | f | avolume × avolume → avolume |
| . + . | encoding-index-node | f | index-node-list × index-node-list → index-node-list |
| . + . | encoding-index-node | f | index-node × index-node-list → index-node-list |
| . ++ . | laddress-list | f | laddress-list × laddress → laddress-list |
| . ++ . | string | f | string × char → string |
| . ++ . | encoding-index-node | f | index-node-list × index-node → index-node-list |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | string | f | char × char → string |
| . +2 . | encoding-index-node | f | index-node × index-node → index-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-index-node | f | index-node-list × index-node → index-node-list |
| . -l . | string | f | string × char → string |
| . -l . | laddress-list | f | laddress-list × laddress → laddress-list |
| . -l . | encoding-index-node | f | index-node-list × index-node → index-node-list |
| . -p . | string | f | string × nat → string |
| . -p . | laddress-list | f | laddress-list × nat → laddress-list |
| . -p . | encoding-index-node | f | index-node-list × nat → index-node-list |
| . .adr | branch | f | branch → address |
| . .adr:= . | branch | f | branch × address → branch |
| . .align↓ | awbuf-inv | f | avolume → avolume |
| . .align↓ | awbuf-inv | f | buffer → buffer |
| . .alignedsize | encoding-index-node | f | index-node → nat |
| . .branch? | branch | p | branch |
| . .branches | indexnode | f | index-node → branch-array |
| . .branches:= . | indexnode | f | index-node × branch-array → index-node |
| . .butlast | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . .butlast | encoding-index-node | pf | index-node-list → index-node-list with λ indx. indx ≠ [] |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .char1 | string | pf | string → char with λ str. str ≠ "" |
| . .data | aleb | pf | aleb → buffer with λ aleb. aleb.mapped? |
| . .data:= . | aleb | pf | aleb × buffer → aleb with λ aleb, buf. aleb.mapped? |
| . .data? | key | p | key |
| . .dentry? | key | p | key |
| . .entry? | branch | p | branch |
| . .flags | lprops | f | lprops → lpropflags |
| . .flags:= . | lprops | f | lprops × lpropflags → lprops |
| . .flashsize | encoding-index-node | f | index-node → nat |
| . .flashsize | encoding-index-node | f | index-node-list → nat |
| . .gcheapidx | lprops | f | lprops → nat |
| . .gcheapidx:= . | lprops | f | lprops × nat → lprops |
| . .head | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .head | encoding-index-node | pf | index-node-list → index-node with λ indx. indx ≠ [] |
| . .indlist | encoding-index-node | f | index-block → index-node-list |
| . .indlist:= . | encoding-index-node | f | index-block × index-node-list → index-block |
| . .ino | key | f | key → nat |
| . .ino:= . | key | f | key × nat → key |
| . .inode? | key | p | key |
| . .isbuf? | bufleb | p | bufleb |
| . .ispadding | node-header | p | node-header |
| . .ispadding:= . | node-header | f | node-header × bool → node-header |
| . .key | branch | f | branch → key |
| . .key:= . | branch | f | branch × key → branch |
| . .ladrlist | encoding-index-node | f | index-block → laddress-list |
| . .ladrlist:= . | encoding-index-node | f | index-block × laddress-list → index-block |
| . .last | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .last | encoding-index-node | pf | index-node-list → index-node with λ indx. indx ≠ [] |
| . .last | string | pf | string → char with λ str. str ≠ "" |
| . .leaf | indexnode | p | index-node |
| . .leaf:= . | indexnode | f | index-node × bool → index-node |
| . .leb | bufleb | pf | bufleb → nat with λ bleb. bleb.isbuf? |
| . .mapped? | aleb | p | aleb |
| . .name | key | pf | key → string with λ key. key.dentry? |
| . .name:= . | key | pf | key × string → key with λ key, str. key.dentry? |
| . .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-index-node | f | index-block → nat |
| . .ref-size:= . | lprops | f | lprops × nat → lprops |
| . .ref-size:= . | encoding-index-node | f | index-block × nat → index-block |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .size | node-header | f | node-header → nat |
| . .size | laddress | f | laddress → nat |
| . .size | lprops | f | lprops → nat |
| . .size:= . | lprops | f | lprops × nat → lprops |
| . .size:= . | node-header | f | node-header × nat → node-header |
| . .size:= . | laddress | f | laddress × nat → laddress |
| . .tail | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . .tail | encoding-index-node | pf | index-node-list → index-node-list with λ indx. indx ≠ [] |
| . .toString | debug | f | nat → string |
| . .usedsize | indexnode | f | index-node → nat |
| . .usedsize:= . | indexnode | f | index-node × nat → index-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-index-node | p | index-node-list × index-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-index-node | pf | index-node-list × nat × index-node → index-node-list with λ indx, n, ind. n < # indx |
| . [ . ] | encoding-index-node | pf | index-node-list × nat → index-node with λ indx, n. n < # indx |
| . [ . ] | avolume | pf | avolume × nat × aleb → avolume with λ avol, n, aleb. n < # avol |
| . [ . ] | avolume | pf | avolume × nat → aleb with λ avol, n. n < # avol |
| . [ . ] | buffer | pf | buffer × nat × data → buffer with λ buf, n, d. n < # buf |
| . [ . ] | buffer | pf | buffer × nat → data with λ buf, n. n < # buf |
| . [ . ] | string | pf | string × nat → char with λ str, n. n < # str |
| . [ . ] | branch-array | pf | branch-array × nat × branch → branch-array with λ brar, n, br. n < # brar |
| . [ . ] | string | pf | string × nat × char → string with λ str, n, char. n < # str |
| . [ . ] | branch-array | pf | branch-array × nat → branch with λ brar, n. n < # brar |
| . ↓ . | awbuf-inv | p | avolume × avolume |
| . ↓ . | awbuf-inv | p | aleb × aleb |
| . ∈ . | string | p | char × string |
| . ∈ . | laddress-list | p | laddress × laddress-list |
| . ∈ . | branch-array | p | branch × branch-array |
| . ∈ . | encoding-index-node | p | index-node × index-node-list |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | avolume | p | aleb × avolume |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | laddress-list | p | laddress-list × laddress-list |
| . ⊑ . | string | p | string × string |
| . ⊑ . | encoding-index-node | p | index-node-list × index-node-list |
| . ⊒ . | laddress-list | p | laddress-list × laddress-list |
| . ⊒ . | string | p | string × string |
| . ⊒ . | encoding-index-node | p | index-node-list × index-node-list |
| @ | laddress | f | nat × nat → laddress |
| [] | encoding-index-node | c | index-node-list |
| [] | laddress-list | c | laddress-list |
| ⊏ | string | p | string × string |
| ⌊ . ⌋ | error-class | p | error |
| ADR_DUMMY | constants | c | address |
| ALIGNEDSIZE | encoding-node-base | v | nat,flexible |
| BRANCH_SIZE | constants | c | nat |
| 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 |
| IND | encoding-index-node | v | index-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 |
| MIN_SIZE | constants | c | nat |
| 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 |
| abs-failed | abs-node | p | buffer |
| abs-leb | encoding-index-node | p | aleb × index-block × lprops |
| abs-node | encoding-index-node | p | buffer × index-node |
| abs-nodes | encoding-index-node | p | buffer × nat × index-node-list × laddress-list × bool |
| abs-nodes | encoding-index-node | p | buffer × index-node-list × laddress-list × bool |
| abs-padding | abs-node | p | buffer |
| address | address | s | |
| adr | address | v | address |
| adr0 | address | v | address |
| adr1 | address | v | address |
| adr2 | address | v | address |
| adr3 | address | v | address |
| adr4 | address | v | address |
| adr5 | address | v | address |
| 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 | indexnode | v | bool |
| boolvar0 | indexnode | v | bool |
| boolvar1 | encoding-node-header | v | bool |
| br | branch | v | branch |
| br0 | branch-array | v | branch |
| br1 | branch-array | v | branch |
| branch | branch | s | |
| branch-array | branch-array | s | |
| brar | branch-array | v | branch-array |
| brar0 | branch-array | v | branch-array |
| brar1 | branch-array | v | branch-array |
| brar2 | branch-array | v | branch-array |
| 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 | string | pf | nat × string → string with λ n, str. n ≤ # str |
| butlastn | encoding-index-node | pf | nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx |
| 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 |
| cmp | branch-array | pp | branch-array × branch × nat × nat with λ brar, br, m, n. m + n ≤ # brar |
| cmp | branch-array | pp | branch-array × nat × branch-array × nat × nat with λ brar, m, brar0, m0, n. m + n ≤ # brar ∧ m0 + n ≤ # brar0 |
| copy | branch-array | pf | branch-array × nat × branch-array × nat × nat → branch-array with λ brar, m, brar0, m0, n. m + n ≤ # brar ∧ m0 + n ≤ # brar0 |
| copy | avolume | pf | avolume × nat × avolume × nat × nat → avolume with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| 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 |
| debug# | debug | pr | string : |
| 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) |
| decode_index_node# | encoding-index-node | pr | nat × nat × buffer : index-node : error (nondeterministic) |
| decode_index_node_headerless# | encoding-index-node | pr | nat × buffer : index-node × nat : error (nondeterministic) |
| dentrykey | key | f | nat × string → key |
| disj | laddress-list | p | laddress-list × laddress-list |
| disj | encoding-index-node | p | index-node-list × index-node-list |
| disj | string | p | string × string |
| dropn | encoding-index-node | f | nat × index-node-list → index-node-list |
| dropn | laddress-list | f | nat × laddress-list → laddress-list |
| dups | laddress-list | p | laddress-list |
| dups | string | p | string |
| dups | encoding-index-node | p | index-node-list |
| empty | buffer | c | data |
| empty | avolume | c | aleb |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| 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) |
| encode_index_node# | encoding-index-node | pr | index-node × nat : nat × buffer : error (nondeterministic) |
| encode_index_node_headerless# | encoding-index-node | pr | index-node × 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 | branch-array | f | branch-array × branch → branch-array |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fill | buffer | f | buffer × data → buffer |
| fill | branch-array | pf | branch-array × branch × nat × nat → branch-array with λ brar, br, n, m. n + m ≤ # brar |
| 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-index-node | f | nat × index-node × index-node-list → index-node-list |
| firstn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| firstn | encoding-index-node | pf | nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| frome | string | f | string × char → string |
| frome | encoding-index-node | f | index-node-list × index-node → index-node-list |
| frome | laddress-list | f | laddress-list × laddress → laddress-list |
| iblock | encoding-index-node | v | index-block |
| id○ | branch-array | p | branch-array × branch-array × nat |
| 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 |
| idrange | branch-array | pp | branch-array × nat × nat with λ brar, m, n. m + n ≤ # brar |
| ind | indexnode | v | index-node |
| ind0 | encoding-index-node | v | index-node |
| ind1 | encoding-index-node | v | index-node |
| ind2 | encoding-index-node | v | index-node |
| ind3 | encoding-index-node | v | index-node |
| ind4 | encoding-index-node | v | index-node |
| ind5 | encoding-index-node | v | index-node |
| index-block | encoding-index-node | s | |
| index-node | indexnode | s | |
| index-node-list | encoding-index-node | s | |
| index-node-size-headerless | encoding-index-node | f | index-node → nat |
| indexblock | encoding-index-node | f | index-node-list × laddress-list × nat → index-block |
| indexnode | indexnode | f | branch-array × bool × nat → index-node |
| indx | encoding-index-node | v | index-node-list |
| indx0 | encoding-index-node | v | index-node-list |
| indx1 | encoding-index-node | v | index-node-list |
| indx3 | encoding-index-node | v | index-node-list |
| indx7 | encoding-index-node | v | index-node-list |
| inodekey | key | f | nat → key |
| is-aligned | align | p | nat × nat |
| is-encoded | encoding-index-node | p | index-node × buffer |
| is-encoded | encoding-node-header | p | node-header × 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 | branch | 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-index-node | pf | nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx |
| 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 |
| min | min-max | f | nat × nat → nat |
| mkavolume | avolume | f | nat → avolume |
| mkbranch | branch | f | key × address → branch |
| mkbrarray | branch-array | f | nat → branch-array |
| mkbuf | buffer | f | nat → buffer |
| mkemparray | avolume | f | nat → avolume |
| mkempbuf | buffer | f | nat → buffer |
| mkentry | branch | f | key × address → branch |
| mklist | string | f | char × nat → string |
| mklist | encoding-index-node | f | index-node × nat → index-node-list |
| mklist | laddress-list | f | laddress × nat → laddress-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 | |
| 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-header | node-header | s | |
| nodeheader | node-header | f | nat × bool → node-header |
| pos | string | f | char × string → nat |
| pos | encoding-index-node | f | index-node × index-node-list → nat |
| pos | laddress-list | f | laddress × laddress-list → nat |
| prefixn | laddress-list | f | nat × laddress-list → laddress-list |
| prefixn | encoding-index-node | f | nat × index-node-list → index-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-index-node | pf | nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| rev | string | f | string → string |
| rev | avolume | pf | avolume × nat → avolume with λ avol, n. n ≤ # avol |
| rev | branch-array | f | branch-array → branch-array |
| rev | buffer | pf | buffer × nat → buffer with λ buf, n. n ≤ # buf |
| rev | buffer | f | buffer → buffer |
| rev | branch-array | pf | branch-array × nat → branch-array with λ brar, n. n ≤ # brar |
| rev | avolume | f | avolume → avolume |
| rev | laddress-list | f | laddress-list → laddress-list |
| rev | encoding-index-node | f | index-node-list → index-node-list |
| rmdup | string | f | string → string |
| rmdup | encoding-index-node | f | index-node-list → index-node-list |
| rmdup | laddress-list | f | laddress-list → laddress-list |
| slice | laddress-list | f | nat × nat × laddress-list → laddress-list |
| slice | encoding-index-node | f | nat × nat × index-node-list → index-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 | branch-array | pf | branch-array × nat × nat → branch-array with λ brar, m, n. m + n ≤ # brar |
| 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-index-node | pf | nat × nat × index-node-list → index-node-list with λ n, m, indx. n + m ≤ # indx |
| sublist | string | pf | nat × nat × string → string with λ n, m, str. n + m ≤ # str |
| synced | awbuf-inv | p | avolume |
| unmapped | aleb | c | aleb |
| validtrailer | node-header-size | c | buffer |
| weak | abs-list | v | bool |
| zero | buffer | c | data |
| zero | avolume | c | aleb |