We call a definition $D$ correct in environment Δ if $\Delta,D; \emptyset ⊢ *: \Box$.
Consider $D_1$ to $D_6$ as in Exercise 9.6.
(a) On what condition can you derive that $D_1$ is correct in environment $\emptyset$?
(b) How do you prove that $D_2$ is correct in environment $D_1$?
(c) The same question for $D_3$ in environment $D_1,D_2$.
We remind ourselves of the (def) rule:
$$ \frac{ \Delta ; \Gamma \; \vdash \; K:L \quad \quad \Delta; \bar{x}:\bar{A} \; \vdash \; M:N }{ \Delta, \bar{x}:\bar{A} \triangleright a(\bar{x}) := M:N ; \Gamma \; \vdash \; K:L} \quad \text{ if } a \notin \Delta $$
We also remind ourselves of definitions $D_1$ to $D_6$:
$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n) \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\ D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \end{align*}$$
(a) Definition $D_1$ is correct in the empty environment $\emptyset$ if $D_1; \emptyset \vdash *: \Box$.
The (def) rule tells us the premises required to derive this.
$$ \frac{ \emptyset; \emptyset \; \vdash \; *:\Box \quad \quad \emptyset; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \; \vdash \; \sum ^n_{i=0}(f i) : \mathbb{R} }{ \emptyset, D_1 ; \emptyset \; \vdash \; *:\Box} $$
The first premise is simply the (sort) rule. The second premise requires the definition $D_1$ be well typed, that is, the definiens and its type can be derived from the context of the definition.
So the condition is that $D_1$ is well typed in the empty environment.
(b) Definition $D_2$ is correct in environment $D_1$ if $D_1, D_2 ; \emptyset \vdash *:\Box$.
The (def) rule tells us the premises required to derive this.
$$ \frac{ D_1; \emptyset \; \vdash \; *:\Box \quad \quad D_1; f : \mathbb{N} \to \mathbb{R}, d : \mathbb{R} \; \vdash \; \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p }{ D_1, D_2 ; \emptyset \; \vdash \; *:\Box} $$
The first premise is the requirement that $D_1$ is correct in the empty environment, from part(a) above.
The second premise is the requirement that $D_2$ is well-formed in the environment $D_1$.
(c) Definition $D_3$ is correct in environment $D_1, D_2$ if $D_1, D_2, D_3; \emptyset \vdash *:\Box$.
The (def) rule tells us the premises required to derive this.
$$ \frac{ D_1, D_2; \emptyset \; \vdash \; *:\Box \quad \quad D_1, D_2; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \; \vdash \; \texttt{formalprf}_3 : f n= f 0 + n \cdot d }{ D_1, D_2, D_3 ; \emptyset \; \vdash \; *:\Box} $$
The first premise is the requirement that $D_2$ is correct in the environment $D_1$.
The second premise is the requirement that $D_3$ is well-formed in the environment $D_1, D_2$.
