Consider the following environment $\Delta$ consisting of six definitions, in which we use, for the sake of convenience, some well-known formats such as the $\Sigma$ and infix-notations:
$$ \begin{align} D_1 \; &≡ \; f : \mathbb{N} → \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := Σ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} →\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} →\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} →\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} →\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} $$
Assume that $\texttt{formalprf}_3$ to $\texttt{formalprf}_6$ are meta-terms, standing for real proof terms.
(a) Rewrite this environment in flag format.
(b) What is a name used for $a_2$ in the standard literature?
(c) Find the δ-normal form with respect to $\Delta$ of $a_5(λx : \mathbb{N}. 2x,2,u,100)$, where $u$ is an inhabitant of $a_2(λx : \mathbb{N}. 2x,2)$.
(a) The following is the environment in flag format.
(b) $a_2$ defines an arithmetic progression, where $d$ is the common difference.
(c) The definition $D_5$ is
$$ 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 $$
This means $a_5(λx : \mathbb{N}. 2x,2,u,100)$ is
$$ a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : a_1(λx : \mathbb{N}. 2x,100) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2 $$
Continuing by unfolding $a_1$,
$$ a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : \sum _{i=0}^{100}((λx : \mathbb{N}. 2x)i) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2 $$
The above is the δ-normal form.
Out of interest we can continue to simplify,
$$ a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : \sum _{i=0}^{100}(2i) = 10100 $$
That is,
$$ \texttt{formalprf}_5 \; : \; \sum _{i=0}^{100}(2i) = 10100 $$
