| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | recovery-entries | f | recoveryentries → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | recovery-entries | f | recoveryentries × lebadress → recoveryentries |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . .leb | lebadress | f | lebadress → nat |
| . .leb:= . | lebadress | f | lebadress × nat → lebadress |
| . .pnum | recovery-entry | f | recoveryentry → nat |
| . .pnum:= . | recovery-entry | f | recoveryentry × nat → recoveryentry |
| . .sqn | recovery-entry | f | recoveryentry → nat |
| . .sqn:= . | recovery-entry | f | recoveryentry × nat → recoveryentry |
| . .vol | lebadress | f | lebadress → volid |
| . .vol:= . | lebadress | f | lebadress × volid → lebadress |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | recovery-entries | pf | recoveryentries × lebadress → recoveryentry with λ recs, ladr. ladr ∈ recs |
| . [ . ] | recovery-entries | f | recoveryentries × lebadress × recoveryentry → recoveryentries |
| . × . | lebadress | f | volid × nat → lebadress |
| . ∈ . | recovery-entries | p | lebadress × recoveryentries |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . subseteq . | recovery-entries | p | recoveryentries × recoveryentries |
| ∅ | recovery-entries | c | recoveryentries |
| ladr | lebadress | v | lebadress |
| ladr1 | recovery-entries | v | lebadress |
| ladr2 | recovery-entries | v | lebadress |
| lebadress | lebadress | s | |
| m | nat-basic | v | nat |
| m0 | lebadress | v | nat |
| m1 | recovery-entry | v | nat |
| m2 | recovery-entry | v | nat |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| rec | recovery-entry | v | recoveryentry |
| rec0 | recovery-entries | v | recoveryentry |
| rec1 | recovery-entries | v | recoveryentry |
| rec2 | recovery-entries | v | recoveryentry |
| recovery-entry | recovery-entry | f | nat × nat → recoveryentry |
| recoveryentries | recovery-entries | s | |
| recoveryentry | recovery-entry | s | |
| recs | recovery-entries | v | recoveryentries |
| recs0 | recovery-entries | v | recoveryentries |
| recs1 | recovery-entries | v | recoveryentries |
| recs2 | recovery-entries | v | recoveryentries |
| v | volid | v | volid |
| v0 | volid | v | volid |
| v1 | volid | v | volid |
| v2 | volid | v | volid |
| volid | volid | s |