appendix sectionnotation

Semi-unification and polymorphic recursion

symbol	meaning	owner
symbol	meaning	owner
$M ⪯_{su} N$	$M$ becomes $N$ under one inequality-local matcher, after the shared outer substitution	definition 5.1, definition 5.2
$S$ ; $R_{i}$	shared outer substitution; matcher local to inequality $i$	definition 5.2
$A; \bar{ρ} ⊢_{FO} e : τ$	first-order Milner–Mycroft template typing with protected monotypes	definition 5.6
$SEI (A, \bar{ρ}, e^{p})$	generated mixed equation/semi-inequality problem rooted at occurrence $p$	definition 5.11
$P ▹_{m} Q$	constructive many-one reduction from decision problem $P$ to $Q$	theorem 5.26