Exercise 5.2
Give a complete (i.e. unshortened) λP-derivation of
$$ S : ∗ ⊢ S →S →∗ : \Box $$
(a) in tree format,
(b) in flag format.
(a) The following shows the derivation in tree format.
$$(1) \; \emptyset \vdash * : \Box \quad (sort)$$
$$ \frac{(1) \; \emptyset \vdash * : \Box}{(2) \; S:* \vdash S:*} \quad (var)$$
$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box}{(3) \; S:* \vdash *:\Box} \quad (weak)$$
$$ \frac{(3) \; S:* \vdash *:\Box \qquad (2) \; S:* \vdash S:*}{(4) \; S:*, x:S \vdash *:\Box} \quad (weak)$$
$$ \frac{(2) \; S:* \vdash S:* \qquad (4) \; S:*, x:S \vdash *:\Box}{(5) \; S:* \vdash S \to *:\Box} \quad (form)$$
$$ \frac{(5) \; S:* \vdash S \to *:\Box \qquad (2) \; S:* \vdash S:*}{(6) \; S:*, x:S \vdash S \to *:\Box} \quad (weak)$$
$$ \frac{(2) \; S:* \vdash S:* \qquad (6) \; S:*, x:S \vdash S \to *:\Box}{(7) \; S:* \vdash S \to S \to *:\Box} \quad (form)$$
(b) The following shows the derivation in flag format.
