matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.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 "static_2/syntax/acle.ma".
  16 include "basic_2/dynamic/cnv_aaa.ma".
  17
  18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  19
  20 (* Properties with preorder for applicability domains ***********************)
  21
  22 lemma cnv_acle_trans (h) (a1) (a2):
  23       a1 ⊆ a2 → ∀G,L,T. ❪G,L❫ ⊢ T ![h,a1] → ❪G,L❫ ⊢ T ![h,a2].
  24 #h #a1 #a2 #Ha12 #G #L #T #H elim H -G -L -T
  25 [ /1 width=1 by cnv_sort/
  26 | /3 width=1 by cnv_zero/
  27 | /3 width=1 by cnv_lref/
  28 | /3 width=1 by cnv_bind/
  29 | #n1 #p #G #L #V #W #T #U #Hn1 #_ #_ #HVW #HTU #IHV #IHT
  30   elim (Ha12 … Hn1) -a1 #n2 #Hn2 #Hn12
  31   /3 width=11 by cnv_appl_ge/
  32 | /3 width=3 by cnv_cast/
  33 ]
  34 qed-.
  35
  36 lemma cnv_acle_omega (h) (a):
  37       ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ T ![h,𝛚].
  38 /3 width=3 by cnv_acle_trans, acle_omega/ qed-.
  39
  40 lemma cnv_acle_one (h) (a) (n):
  41       ∀G,L,T. ❪G,L❫ ⊢ T ![h,𝟏] → ad a n → ❪G,L❫ ⊢ T ![h,a].
  42 /3 width=3 by cnv_acle_trans, acle_one/ qed-.