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 "static_2/syntax/acle.ma".
16 include "basic_2/dynamic/cnv_aaa.ma".
18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
20 (* Properties with preorder for applicability domains ***********************)
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/
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-.
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-.