| Symbol | Specification | Kind | Type |
|---|---|---|---|
| . ≪1 . | lexical-param | p | elem1 × elem1 |
| . ≪2 . | lexical-param | p | elem2 × elem2 |
| IHP | lexical-param | v | elem1 → bool |
| IHPQ | lexical | v | elem1 × elem2 → bool |
| IHQ | lexical-param | v | elem2 → bool |
| a | lexical-param | v | elem1 |
| a0 | lexical-param | v | elem1 |
| a1 | lexical-param | v | elem1 |
| b | lexical-param | v | elem2 |
| b0 | lexical-param | v | elem2 |
| b1 | lexical-param | v | elem2 |
| elem1 | lexical-param | s | |
| elem2 | lexical-param | s | |
| lex< | lexical | p | elem1 × elem2 × elem1 × elem2 |