| Symbol | Specification | Kind | Type |
|---|
| # . | string | f | string → nat |
| # . | branch-array | f | branch-array → nat |
| # . | zbranch-array | f | zbranch-array → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | string | f | char → string |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | string | f | char × string → string |
| . + . | string | f | string × char → string |
| . + . | string | f | string × string → string |
| . ++ . | string | f | string × char → string |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | string | f | char × char → string |
| . - . | 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 |
| . -l . | string | f | string × char → string |
| . -p . | string | f | string × nat → string |
| . .adr | zbranch | f | zbranch → address |
| . .adr | branch | f | branch → address |
| . .adr:= . | branch | f | branch × address → branch |
| . .adr:= . | zbranch | f | zbranch × address → zbranch |
| . .branch? | branch | p | branch |
| . .branch? | zbranch | p | zbranch |
| . .branches | indexnode | f | index-node → branch-array |
| . .branches:= . | indexnode | f | index-node × branch-array → index-node |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .char1 | string | pf | string → char with λ str. str ≠ "" |
| . .child | zbranch | pf | zbranch → ref with λ zbr. zbr.branch? |
| . .child:= . | zbranch | pf | zbranch × ref → zbranch with λ zbr, r. zbr.branch? |
| . .data? | key | p | key |
| . .dentry? | key | p | key |
| . .dirty | znode | p | znode |
| . .dirty:= . | znode | f | znode × bool → znode |
| . .entry? | branch | p | branch |
| . .entry? | zbranch | p | zbranch |
| . .ino | key | f | key → nat |
| . .ino:= . | key | f | key × nat → key |
| . .inode? | key | p | key |
| . .key | zbranch | f | zbranch → key |
| . .key | branch | f | branch → key |
| . .key:= . | zbranch | f | zbranch × key → zbranch |
| . .key:= . | branch | f | branch × key → branch |
| . .last | string | pf | string → char with λ str. str ≠ "" |
| . .leaf | indexnode | p | index-node |
| . .leaf | znode | p | znode |
| . .leaf:= . | znode | f | znode × bool → znode |
| . .leaf:= . | indexnode | f | index-node × bool → index-node |
| . .name | key | pf | key → string with λ key. key.dentry? |
| . .name:= . | key | pf | key × string → key with λ key, str. key.dentry? |
| . .parent | znode | f | znode → ref |
| . .parent:= . | znode | f | znode × ref → znode |
| . .part | key | pf | key → nat with λ key. key.data? |
| . .part:= . | key | pf | key × nat → key with λ key, m. key.data? |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .usedsize | znode | f | znode → nat |
| . .usedsize | indexnode | f | index-node → nat |
| . .usedsize:= . | indexnode | f | index-node × nat → index-node |
| . .usedsize:= . | znode | f | znode × nat → znode |
| . .zbranches | znode | f | znode → zbranch-array |
| . .zbranches:= . | znode | f | znode × zbranch-array → znode |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . < . | key-order-def | p | key × key |
| . < . | string-less | p | char × char |
| . < . | string-less | p | string × string |
| . > . | nat | p | nat × nat |
| . [ . ] | branch-array | pf | branch-array × nat × branch → branch-array with λ brar, n, br. n < # brar |
| . [ . ] | branch-array | pf | branch-array × nat → branch with λ brar, n. n < # brar |
| . [ . ] | zbranch-array | pf | zbranch-array × nat × zbranch → zbranch-array with λ zbrar, n, zbr. n < # zbrar |
| . [ . ] | zbranch-array | pf | zbranch-array × nat → zbranch with λ zbrar, n. n < # zbrar |
| . [ . ] | string | pf | string × nat × char → string with λ str, n, char. n < # str |
| . [ . ] | string | pf | string × nat → char with λ str, n. n < # str |
| . ∈ . | string | p | char × string |
| . ∈ . | branch-array | p | branch × branch-array |
| . ∈ . | zbranch-array | p | zbranch × zbranch-array |
| . ≤ . | nat | p | nat × nat |
| . ≤ . | zbranch-array-sorted | p | key × key |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | string | p | string × string |
| . ⊒ . | string | p | string × string |
| ⊏ | string | p | string × string |
| ADR_DUMMY | constants | c | address |
| BRANCH_SIZE | constants | c | nat |
| Boolvar | key-order | v | bool,flexible |
| MIN_SIZE | constants | c | nat |
| 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 |
| align↑ | align | f | nat × nat → nat |
| align↓ | align | f | nat × nat → nat |
| boolvar | indexnode | v | bool |
| boolvar0 | indexnode | v | bool |
| boolvar1 | key-order | v | bool |
| boolvar2 | znode | 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 |
| butlastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| bv | znode-ops | v | bool |
| char | char | s | |
| char | char | v | char |
| char0 | char | v | char |
| char1 | char | v | char |
| char2 | char | v | char |
| char3 | string-less | v | char |
| 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 |
| cmp | zbranch-array | pp | zbranch-array × zbranch × nat × nat with λ zbrar, zbr, m, n. m + n ≤ # zbrar |
| cmp | zbranch-array | pp | zbranch-array × nat × zbranch-array × nat × nat with λ zbrar, m, zbrar0, m0, n. m + n ≤ # zbrar ∧ m0 + n ≤ # zbrar0 |
| copy | zbranch-array | pf | zbranch-array × nat × zbranch-array × nat × nat → zbranch-array with λ zbrar, m, zbrar0, m0, n. m + n ≤ # zbrar ∧ m0 + n ≤ # zbrar0 |
| 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 |
| datakey | key | f | nat × nat → key |
| dentrykey | key | f | nat × string → key |
| disj | string | p | string × string |
| dups | string | p | string |
| fill | branch-array | pf | branch-array × branch × nat × nat → branch-array with λ brar, br, n, m. n + m ≤ # brar |
| fill | zbranch-array | f | zbranch-array × zbranch → zbranch-array |
| fill | zbranch-array | pf | zbranch-array × zbranch × nat × nat → zbranch-array with λ zbrar, zbr, n, m. n + m ≤ # zbrar |
| fill | branch-array | f | branch-array × branch → branch-array |
| fillfirst | string | f | nat × char × string → string |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| frome | string | f | string × char → string |
| id○ | branch-array | p | branch-array × branch-array × nat |
| id○ | zbranch-array | p | zbranch-array × zbranch-array × nat |
| idrange | branch-array | pp | branch-array × nat × nat with λ brar, m, n. m + n ≤ # brar |
| idrange | zbranch-array | pp | zbranch-array × nat × nat with λ zbrar, m, n. m + n ≤ # zbrar |
| ind | indexnode | v | index-node |
| index-node | indexnode | s | |
| indexnode | indexnode | f | branch-array × bool × nat → index-node |
| ino | key-order-def | v | nat |
| inodekey | key | f | nat → key |
| is-aligned | align | p | nat × nat |
| key | key | s | |
| key | key | v | key |
| key0 | zbranch | v | key |
| key1 | key-order | v | key |
| lastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| len | znode-ops | v | nat |
| load | znode-ops | f | ref × index-node → znode |
| load | znode-ops | f | branch-array × nat × nat → zbranch-array |
| load | znode-ops | f | branch → zbranch |
| m | nat-basic | v | nat |
| m0 | array-copy | v | nat |
| m1 | key | v | nat |
| m2 | key | v | nat |
| mkbranch | branch | f | key × address → branch |
| mkbrarray | branch-array | f | nat → branch-array |
| mkentry | branch | f | key × address → branch |
| mklist | string | f | char × nat → string |
| mkzbranch | zbranch | f | key × address × ref → zbranch |
| mkzbrarray | zbranch-array | f | nat → zbranch-array |
| mkzentry | zbranch | f | key × address → zbranch |
| mkznode | znode | f | ref × zbranch-array × bool × bool × nat → znode |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| null | ref | c | ref |
| nused | znode-ops | v | nat |
| pos | string | f | char × string → nat |
| r | ref | v | ref |
| r0 | ref | v | ref |
| r1 | ref | v | ref |
| ref | ref | s | |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| rev | branch-array | pf | branch-array × nat → branch-array with λ brar, n. n ≤ # brar |
| rev | zbranch-array | pf | zbranch-array × nat → zbranch-array with λ zbrar, n. n ≤ # zbrar |
| rev | branch-array | f | branch-array → branch-array |
| rev | string | f | string → string |
| rev | zbranch-array | f | zbranch-array → zbranch-array |
| rmdup | string | f | string → string |
| save | znode-ops | f | zbranch → branch |
| save | znode-ops | f | zbranch-array × nat × nat → branch-array |
| save | znode-ops | f | znode → index-node |
| scan | znode-ops | f | key × zbranch-array × nat × nat → nat |
| shl | znode-ops | f | zbranch-array × nat × nat → zbranch-array |
| shr | znode-ops | f | zbranch-array × nat × nat → zbranch-array |
| sorted | zbranch-array-sorted | p | zbranch-array × nat × nat |
| sortedchars | string-less | c | string |
| str | string | v | string |
| str0 | string | v | string |
| str1 | string | v | string |
| str2 | string | v | string |
| str3 | string | v | string |
| string | string | s | |
| subarray | branch-array | pf | branch-array × nat × nat → branch-array with λ brar, m, n. m + n ≤ # brar |
| subarray | zbranch-array | pf | zbranch-array × nat × nat → zbranch-array with λ zbrar, m, n. m + n ≤ # zbrar |
| sublist | string | pf | nat × nat × string → string with λ n, m, str. n + m ≤ # str |
| zbr | zbranch | v | zbranch |
| zbr0 | zbranch-array | v | zbranch |
| zbr1 | zbranch-array | v | zbranch |
| zbranch | zbranch | s | |
| zbranch-array | zbranch-array | s | |
| zbrar | zbranch-array | v | zbranch-array |
| zbrar0 | zbranch-array | v | zbranch-array |
| zbrar1 | zbranch-array | v | zbranch-array |
| zbrar2 | zbranch-array | v | zbranch-array |
| znd | znode | v | znode |
| znode | znode | s | |