1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/rt_computation/cpms_drops.ma".
16 include "basic_2/dynamic/cnv.ma".
18 (* EXAMPLES *****************************************************************)
20 (* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************)
22 (* Note: extended validity of a closure, height of cnv_appl > 1 *)
23 lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h].
25 @(cnv_appl … 2 p … (⋆s) … (⋆s))
27 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
28 | /4 width=1 by cnv_bind, cnv_zero/
29 | /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
30 | /5 width=5 by cpm_cpms, cpm_bind, cpm_ell, lifts_uni, lifts_sort, lifts_bind/
34 (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
35 lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h].
37 @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
38 [ /2 width=1 by ylt_inj/
39 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
42 @(cnv_appl … 1 p … (⋆s) … (⋆s))
43 [ /2 width=1 by ylt_inj/
44 | /2 width=1 by cnv_sort, cnv_zero/
45 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
46 | /2 width=3 by cpms_ell, lifts_sort/
47 | /4 width=5 by cpms_lref, cpms_ell, lifts_uni, lifts_sort, lifts_bind/
49 | /4 width=3 by cpms_lref, cpms_ell, lifts_sort/
50 | /5 width=7 by cpms_ell, lifts_bind, lifts_flat, lifts_push_lref, lifts_push_zero, lifts_sort/