]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2A/examples/ex_snv_eta.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / examples / ex_snv_eta.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basic_2A/dynamic/snv.ma".
16
17 (* EXAMPLES *****************************************************************)
18
19 (* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
20
21 (* extended validity of a closure, last arg of snv_appl > 1 *)
22 lemma snv_extended: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, g].
23 #h #g #a #G #L #k elim (deg_total h g k)
24 #d #Hd @(snv_appl … a … (⋆k) … (⋆k) (0+1+1))
25 [ /4 width=5 by snv_lref, drop_drop_lt/
26 | /4 width=13 by snv_bind, snv_lref/
27 | /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
28 | @(lstas_scpds … (d+1+1))
29   /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/
30 ]
31 qed.
32
33 (* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **)
34 lemma snv_restricted: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛⓛ{a}⋆k.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, g].
35 #h #g #a #G #L #k elim (deg_total h g k)
36 #d #Hd @(snv_appl … a … (⋆k) … (ⓐ#0.#2) (0+1))
37 [ /4 width=5 by snv_lref, drop_drop_lt/
38 | @snv_lref [4: // |1,2,3: skip ]
39   @snv_bind //
40   @(snv_appl … a … (⋆k) … (⋆k) (0+1))
41   [ @snv_lref [4: // |1,2,3: skip ] //
42   | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //
43   | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/
44   | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/
45     @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/
46   ]
47 | /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
48 | @(lstas_scpds … (d+1+1)) //
49   [ @da_ldec [3: // |1,2: skip ]
50     @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ]
51     /3 width=1 by da_sort, da_bind/
52   | @lstas_succ [4: // |1,2: skip ]
53     [2: @lstas_bind | skip ]
54     [2: @lstas_appl | skip ]
55     [2: @lstas_zero
56         [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ]
57     |1: skip ]
58     /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/
59   ]
60 ]
61 qed.