Check that all instantiations of the parameters of constants defined and used in Exercise 8.2 satisfy the requirements imposed by the (inst)-rule.
The following is the text used in Exercise 8.2.
The following summarises the derivation rules for $\lambda D_0$.
The (inst)-rule ensures that the substituted expressions $\bar{U}$ are derivable in the environment and context $\Delta; \Gamma$.
There are only two instantiations in Exercise 8.2, at line (7) and (8). Let's consider each in turn.
(7) In defining $p_7$, the type $\textit{bounded-from-above}(S,p_6)$ has instantiated
- $V$ as $S$
- $u$ and $p_6$
in that order.
The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.
Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$.
And so the instantiations of $\textit{bounded-from-above}(S,p_6)$ satisfy the requirements of the (inst)-rule.
(8) In defining $p_8$, the type $\text{least-upper-bound}(S, p_6, 1)$ has instantiated
- $V$ as $S$
- $u$ as $p_6$
- $s$ as 1
in that order.
The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.
Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$.
