--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/exclaim_5.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* NATIVE VALIDITY FOR TERMS ************************************************)
+
+(* activate genv *)
+(* Basic_2A1: uses: snv *)
+inductive nv (a) (h): relation3 genv lenv term ≝
+| nv_sort: ∀G,L,s. nv a h G L (⋆s)
+| nv_zero: ∀I,G,K,V. nv a h G K V → nv a h G (K.ⓑ{I}V) (#0)
+| nv_lref: ∀I,G,K,i. nv a h G K (#i) → nv a h G (K.ⓘ{I}) (#↑i)
+| nv_bind: ∀p,I,G,L,V,T. nv a h G L V → nv a h G (L.ⓑ{I}V) T → nv a h G L (ⓑ{p,I}V.T)
+| nv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n = 1) → nv a h G L V → nv a h G L T →
+ ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → nv a h G L (ⓐV.T)
+| nv_cast: ∀G,L,U,T,U0. nv a h G L U → nv a h G L T →
+ ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → nv a h G L (ⓝU.T)
+.
+
+interpretation "native validity (term)"
+ 'Exclaim a h G L T = (nv a h G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact nv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
+ ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
+#a #h #G #L #X * -G -L -X
+[ #G #L #s #H destruct
+| #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
+| #I #G #K #i #_ #H destruct
+| #p #I #G #L #V #T #_ #_ #H destruct
+| #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma nv_inv_zero (a) (h): ∀G,L. ⦃G, L⦄ ⊢ #0 ![a, h] →
+ ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
+/2 width=3 by nv_inv_zero_aux/ qed-.
+
+fact nv_inv_lref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀i. X = #(↑i) →
+ ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
+#a #h #G #L #X * -G -L -X
+[ #G #L #s #j #H destruct
+| #I #G #K #V #_ #j #H destruct
+| #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/
+| #p #I #G #L #V #T #_ #_ #j #H destruct
+| #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #j #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #j #H destruct
+]
+qed-.
+
+lemma nv_inv_lref (a) (h): ∀G,L,i. ⦃G, L⦄ ⊢ #↑i ![a, h] →
+ ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
+/2 width=3 by nv_inv_lref_aux/ qed-.
+
+fact nv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀l. X = §l → ⊥.
+#a #h #G #L #X * -G -L -X
+[ #G #L #s #l #H destruct
+| #I #G #K #V #_ #l #H destruct
+| #I #G #K #i #_ #l #H destruct
+| #p #I #G #L #V #T #_ #_ #l #H destruct
+| #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #l #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #l #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: snv_inv_gref *)
+lemma nv_inv_gref (a) (h): ∀G,L,l. ⦃G, L⦄ ⊢ §l ![a, h] → ⊥.
+/2 width=8 by nv_inv_gref_aux/ qed-.
+
+fact nv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] →
+ ∀p,I,V,T. X = ⓑ{p,I}V.T →
+ ∧∧ ⦃G, L⦄ ⊢ V ![a, h]
+ & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
+#a #h #G #L #X * -G -L -X
+[ #G #L #s #q #Z #X1 #X2 #H destruct
+| #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
+| #I #G #K #i #_ #q #Z #X1 #X2 #H destruct
+| #p #I #G #L #V #T #HV #HT #q #Z #X1 #X2 #H destruct /2 width=1 by conj/
+| #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: snv_inv_bind *)
+lemma nv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] →
+ ∧∧ ⦃G, L⦄ ⊢ V ![a, h]
+ & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
+/2 width=4 by nv_inv_bind_aux/ qed-.
+
+fact nv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T →
+ ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
+#a #h #G #L #X * -L -X
+[ #G #L #s #X1 #X2 #H destruct
+| #I #G #K #V #_ #X1 #X2 #H destruct
+| #I #G #K #i #_ #X1 #X2 #H destruct
+| #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
+| #n #p #G #L #V #W0 #T #U0 #Ha #HV #HT #HVW0 #HTU0 #X1 #X2 #H destruct /3 width=7 by ex5_4_intro/
+| #G #L #U #T #U0 #_ #_ #_ #_ #X1 #X2 #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: snv_inv_appl *)
+lemma nv_inv_appl (a) (h): ∀G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
+ ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
+/2 width=3 by nv_inv_appl_aux/ qed-.
+
+fact nv_inv_cast_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀U,T. X = ⓝU.T →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
+#a #h #G #L #X * -G -L -X
+[ #G #L #s #X1 #X2 #H destruct
+| #I #G #K #V #_ #X1 #X2 #H destruct
+| #I #G #K #i #_ #X1 #X2 #H destruct
+| #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
+| #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #X1 #X2 #H destruct
+| #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
+]
+qed-.
+
+(* Basic_2A1: uses: snv_inv_appl *)
+lemma nv_inv_cast (a) (h): ∀G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
+/2 width=3 by nv_inv_cast_aux/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/nativevalid_5.ma".
-include "basic_2/computation/scpds.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* activate genv *)
-inductive snv (h) (o): relation3 genv lenv term ≝
-| snv_sort: ∀G,L,s. snv h o G L (⋆s)
-| snv_lref: ∀I,G,L,K,V,i. ⬇[i] L ≘ K.ⓑ{I}V → snv h o G K V → snv h o G L (#i)
-| snv_bind: ∀a,I,G,L,V,T. snv h o G L V → snv h o G (L.ⓑ{I}V) T → snv h o G L (ⓑ{a,I}V.T)
-| snv_appl: ∀a,G,L,V,W0,T,U0,d. snv h o G L V → snv h o G L T →
- ⦃G, L⦄ ⊢ V •*➡*[h, o, 1] W0 → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] ⓛ{a}W0.U0 → snv h o G L (ⓐV.T)
-| snv_cast: ∀G,L,U,T,U0. snv h o G L U → snv h o G L T →
- ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 → ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0 → snv h o G L (ⓝU.T)
-.
-
-interpretation "stratified native validity (term)"
- 'NativeValid h o G L T = (snv h o G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact snv_inv_lref_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀i. X = #i →
- ∃∃I,K,V. ⬇[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, o].
-#h #o #G #L #X * -G -L -X
-[ #G #L #s #i #H destruct
-| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/
-| #a #I #G #L #V #T #_ #_ #i #H destruct
-| #a #G #L #V #W0 #T #U0 #d #_ #_ #_ #_ #i #H destruct
-| #G #L #U #T #U0 #_ #_ #_ #_ #i #H destruct
-]
-qed-.
-
-lemma snv_inv_lref: ∀h,o,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, o] →
- ∃∃I,K,V. ⬇[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, o].
-/2 width=3 by snv_inv_lref_aux/ qed-.
-
-fact snv_inv_gref_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀p. X = §p → ⊥.
-#h #o #G #L #X * -G -L -X
-[ #G #L #s #p #H destruct
-| #I #G #L #K #V #i #_ #_ #p #H destruct
-| #a #I #G #L #V #T #_ #_ #p #H destruct
-| #a #G #L #V #W0 #T #U0 #d #_ #_ #_ #_ #p #H destruct
-| #G #L #U #T #U0 #_ #_ #_ #_ #p #H destruct
-]
-qed-.
-
-lemma snv_inv_gref: ∀h,o,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, o] → ⊥.
-/2 width=8 by snv_inv_gref_aux/ qed-.
-
-fact snv_inv_bind_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
- ⦃G, L⦄ ⊢ V ¡[h, o] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, o].
-#h #o #G #L #X * -G -L -X
-[ #G #L #s #b #Z #X1 #X2 #H destruct
-| #I #G #L #K #V #i #_ #_ #b #Z #X1 #X2 #H destruct
-| #a #I #G #L #V #T #HV #HT #b #Z #X1 #X2 #H destruct /2 width=1 by conj/
-| #a #G #L #V #W0 #T #U0 #d #_ #_ #_ #_ #b #Z #X1 #X2 #H destruct
-| #G #L #U #T #U0 #_ #_ #_ #_ #b #Z #X1 #X2 #H destruct
-]
-qed-.
-
-lemma snv_inv_bind: ∀h,o,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, o] →
- ⦃G, L⦄ ⊢ V ¡[h, o] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, o].
-/2 width=4 by snv_inv_bind_aux/ qed-.
-
-fact snv_inv_appl_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀V,T. X = ⓐV.T →
- ∃∃a,W0,U0,d. ⦃G, L⦄ ⊢ V ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
- ⦃G, L⦄ ⊢ V •*➡*[h, o, 1] W0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, d] ⓛ{a}W0.U0.
-#h #o #G #L #X * -L -X
-[ #G #L #s #X1 #X2 #H destruct
-| #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
-| #a #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
-| #a #G #L #V #W0 #T #U0 #d #HV #HT #HVW0 #HTU0 #X1 #X2 #H destruct /2 width=6 by ex4_4_intro/
-| #G #L #U #T #U0 #_ #_ #_ #_ #X1 #X2 #H destruct
-]
-qed-.
-
-lemma snv_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, o] →
- ∃∃a,W0,U0,d. ⦃G, L⦄ ⊢ V ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
- ⦃G, L⦄ ⊢ V •*➡*[h, o, 1] W0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, d] ⓛ{a}W0.U0.
-/2 width=3 by snv_inv_appl_aux/ qed-.
-
-fact snv_inv_cast_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀U,T. X = ⓝU.T →
- ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
- ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0.
-#h #o #G #L #X * -G -L -X
-[ #G #L #s #X1 #X2 #H destruct
-| #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
-| #a #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
-| #a #G #L #V #W0 #T #U0 #d #_ #_ #_ #_ #X1 #X2 #H destruct
-| #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
-]
-qed-.
-
-lemma snv_inv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] →
- ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
- ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0.
-/2 width=3 by snv_inv_cast_aux/ qed-.
(* Relocation properties ****************************************************)
+| nv_lref: ∀I,G,L,K,V,i. ⬇[i] L ≘ K.ⓑ{I}V → nv a h G K V → nv a h G L (#i)
+
+lemma nv_inv_lref: ∀a,h,G,L,i. ⦃G, L⦄ ⊢ #i ![a, h] →
+ ∃∃I,K,V. ⬇[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ![a, h].
+/2 width=3 by nv_inv_lref_aux/ qed-.
+
+
lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≘ K →
∀U. ⬆[l, k] T ≘ U → ⦃G, L⦄ ⊢ U ¡[h, o].
#h #o #G #K #T #H elim H -G -K -T
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/da_aaa.ma".
+include "basic_2/computation/scpds_aaa.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Forward lemmas on atomic arity assignment for terms **********************)
+
+lemma snv_fwd_aaa: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
+#h #o #G #L #T #H elim H -G -L -T
+[ /2 width=2 by aaa_sort, ex_intro/
+| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
+| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
+| #a #G #L #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 * #B #HV * #X #HT
+ lapply (scpds_aaa_conf … HV … HVW0) -HVW0 #HW0
+ lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
+ elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
+ lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/
+| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
+ lapply (scpds_aaa_conf … HU … HU0) -HU0 #HU0
+ lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
+ lapply (aaa_mono … H … HU0) -U0 #H destruct /3 width=3 by aaa_cast, ex_intro/
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma snv_fwd_da: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃d. ⦃G, L⦄ ⊢ T ▪[h, o] d.
+#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_da/
+qed-.
+
+lemma snv_fwd_lstas: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ∀d. ∃U. ⦃G, L⦄ ⊢ T •*[h, d] U.
+#h #o #G #L #T #H #d elim (snv_fwd_aaa … H) -H
+#A #HT elim (aaa_lstas h … HT d) -HT /2 width=2 by ex_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lsubd_da.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_scpes.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on degree assignment for terms ********************************)
+
+fact da_cpr_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1.
+#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #_ #_ #_ #_ #d #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
+ lapply (da_inv_sort … H2) -H2
+ lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/
+| #i #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+ elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0
+ elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #d1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct
+ lapply (drop_mono … H … HLK1) -H #H destruct
+ elim (cpr_inv_lref1 … H3) -H3
+ [1,3: #H destruct
+ lapply (fqup_lref … G1 … HLK1)
+ elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
+ |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
+ lapply (drop_mono … H … HLK1) -H #H destruct
+ lapply (fqup_lref … G1 … HLK1)
+ elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
+ lapply (drop_fwd_drop2 … HLK2) -V2
+ /4 width=8 by da_lift, fqup_fpbg/
+ ]
+| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+ elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH2
+ elim (snv_inv_bind … H1) -H1 #_ #HT1
+ lapply (da_inv_bind … H2) -H2
+ elim (cpr_inv_bind1 … H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
+ | #T2 #HT12 #HT2 #H1 #H2 destruct
+ /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, drop_drop/
+ ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct
+ elim (snv_inv_appl … H1) -H1 #b1 #W1 #U1 #d1 #HV1 #HT1 #HVW1 #HTU1
+ lapply (da_inv_flat … H2) -H2 #Hd
+ elim (cpr_inv_appl1 … H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
+ | #b #V2 #W #W2 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW #HU
+ lapply (da_inv_bind … Hd) -Hd #Hd
+ elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -d1
+ elim (snv_fwd_da … HV1) #d1 #Hd1
+ elim (snv_fwd_da … HW) #d0 #Hd0
+ lapply (cprs_scpds_div … HW3 … Hd0 … 1 HVW1) -W3 #H
+ elim (da_scpes_aux … IH3 IH2 IH1 … Hd0 … Hd1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
+ <minus_n_O #H destruct >(plus_minus_k_k d1 1) in Hd1; // -H1 #Hd1
+ lapply (IH1 … HV1 … Hd1 … HV12 … HL12) -HV1 -Hd1 -HV12 [ /2 by fqup_fpbg/ ]
+ lapply (IH1 … Hd0 … HW2 … HL12) -Hd0 /2 width=1 by fqup_fpbg/ -HW
+ lapply (IH1 … HU … Hd … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hd -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
+ /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/
+ | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -d1 -HV1
+ elim (snv_inv_bind … HT1) -HT1 #_
+ lapply (da_inv_bind … Hd) -Hd
+ /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
+ ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+ elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
+ lapply (da_inv_flat … H2) -H2 #Hd
+ elim (cpr_inv_cast1 … H3) -H3
+ [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
+ | /3 width=7 by fqup_fpbg/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fsb_aaa.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* forward lemmas on "qrst" strongly normalizing closures *********************)
+
+lemma snv_fwd_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ⦥[h, o] ⦃G, L, T⦄.
+#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/multiple/fqus_alt.ma".
+include "basic_2/computation/scpds_lift.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Relocation properties ****************************************************)
+
+lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≘ K →
+ ∀U. ⬆[l, k] T ≘ U → ⦃G, L⦄ ⊢ U ¡[h, o].
+#h #o #G #K #T #H elim H -G -K -T
+[ #G #K #s #L #b #l #k #_ #X #H
+ >(lift_inv_sort1 … H) -X -K -l -k //
+| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #b #l #k #HLK #X #H
+ elim (lift_inv_lref1 … H) * #Hil #H destruct
+ [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by ylt_fwd_le/ #X #HL0 #H
+ elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #L0 #W #HLK0 #HVW #H destruct
+ /3 width=9 by snv_lref/
+ | lapply (drop_trans_ge … HLK … HK0 ?) -K
+ /3 width=9 by snv_lref, drop_inv_gen/
+ ]
+| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #b #l #k #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
+ /4 width=5 by snv_bind, drop_skip/
+| #a #G #K #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
+ elim (lift_total W0 l k)
+ elim (lift_total U0 (l+1) k)
+ /4 width=17 by snv_appl, scpds_lift, lift_bind/
+| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
+ elim (lift_total U0 l k)
+ /3 width=12 by snv_cast, scpds_lift/
+]
+qed.
+
+lemma snv_inv_lift: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≘ K →
+ ∀T. ⬆[l, k] T ≘ U → ⦃G, K⦄ ⊢ T ¡[h, o].
+#h #o #G #L #U #H elim H -G -L -U
+[ #G #L #s #K #b #l #k #_ #X #H
+ >(lift_inv_sort2 … H) -X -L -l -k //
+| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #b #l #k #HLK #X #H
+ elim (lift_inv_lref2 … H) * #Hil #H destruct
+ [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H
+ elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct
+ /3 width=12 by snv_lref/
+ | lapply (drop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/
+ ]
+| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #b #l #k #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
+ /4 width=5 by snv_bind, drop_skip/
+| #a #G #L #W #W1 #U #U1 #d #_ #_ #HW1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
+ elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0
+ elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0
+ elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
+ lapply (lift_inj … HY … HW01) -HY #H destruct
+ /3 width=6 by snv_appl/
+| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
+ elim (scpds_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
+ elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0
+ lapply (lift_inj … HX … HU01) -HX #H destruct
+ /3 width=5 by snv_cast/
+]
+qed-.
+
+(* Properties on subclosure *************************************************)
+
+lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I1 #G1 #L1 #V1 #H
+ elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
+ lapply (drop_inv_O2 … H) -H #H destruct //
+|2: *
+|5,6: /3 width=8 by snv_inv_lift/
+]
+[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|2,4: * #G1 #L1 #V1 #T1 #H
+ [1,3: elim (snv_inv_appl … H) -H //
+ |2,4: elim (snv_inv_cast … H) -H //
+ ]
+]
+qed-.
+
+lemma snv_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*]
+/2 width=5 by snv_fqu_conf/
+qed-.
+
+lemma snv_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=5 by fqup_strap1, snv_fqu_conf/
+qed-.
+
+lemma snv_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*]
+/2 width=5 by snv_fqup_conf/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/snv_lift.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_scpes.ma".
+include "basic_2/dynamic/lsubsv_snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_cpr_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h o G1 L1 T1.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
+ >(cpr_inv_sort1 … H2) -X //
+| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+ elim (lpr_drop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (fqup_lref … G1 … HLK1) #HKL
+ elim (cpr_inv_lref1 … H2) -H2
+ [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
+ | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+ lapply (drop_mono … H … HLK1) -HLK1 -H #H destruct
+ lapply (drop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/
+ ]
+| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+ elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+ elim (cpr_inv_bind1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
+ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+ /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, drop_drop/
+ ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+ elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1
+ elim (cpr_inv_appl1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H
+ elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1
+ elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW
+ lapply (scpds_cprs_trans … HVW2 … HXV) -XV
+ lapply (scpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?)
+ /2 width=7 by snv_appl, cprs_bind/
+ | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10
+ elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -d0
+ elim (snv_fwd_da … HV1) #d #HV1d
+ elim (snv_fwd_da … HW10) #d0 #HW10d
+ lapply (cprs_scpds_div … HW130 … HW10d … 1 HVW1) -W30 #HVW10
+ elim (da_scpes_aux … IH4 IH1 IH2 … HW10d … HV1d … HVW10) /2 width=1 by fqup_fpbg/
+ #_ #Hd <minus_n_O #H destruct >(plus_minus_k_k d 1) in HV1d; // -Hd #HV1d
+ lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
+ lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1d #HV2d
+ lapply (IH2 … HW10d … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10d #HW20d
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20
+ lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20
+ @snv_bind /2 width=1 by snv_cast_scpes/
+ @(lsubsv_snv_trans … HT20) -HT20
+ @(lsubsv_beta … (d-1)) //
+ @shnv_cast [1,2: // ] #d0 #Hd0
+ lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20d … HV2d … d0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
+ elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
+ elim (scpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+ elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H
+ elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3
+ lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+ lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
+ lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
+ lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2
+ elim (lift_total XV 0 1) #XW #HXVW
+ lapply (scpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2
+ lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3
+ elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3
+ lapply (scpds_cprs_trans … HXWV2 … HXW3) -XW
+ lapply (scpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W
+ /3 width=6 by snv_appl, snv_bind/
+ ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
+ elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
+ elim (cpr_inv_cast1 … H2) -H2
+ [ * #W2 #T2 #HW12 #HT12 #H destruct
+ elim (snv_fwd_da … HW1) #d #HW1d
+ lapply (scpds_div … HWU1 … HTU1) -U1 -d #HWT1
+ lapply (scpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/
+ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1
+ /2 width=1 by snv_cast_scpes/
+ | #H -IH3 -IH2 -HW1 -U1
+ lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/snv_lift.ma".
+include "basic_2/dynamic/snv_scpes.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on nat-iterated stratified static type assignment for terms ***)
+
+fact snv_lstas_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas h o G1 L1 T1.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #HG0 #HL0 #HT0 #_ #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
+ >(lstas_inv_sort1 … H2) -X //
+| #i #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #T #H2 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0
+ elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d0 ] #HLK1 [ #Hd1 | #Hd0 #H ]
+ lapply (drop_mono … HLK0 … HLK1) -HLK0 #H0 destruct
+ elim (lstas_inv_lref1 … H2) -H2 * #K #Y #X [3,6: #d ] #HLK #HYX [1,2: #HXT #H0 |3,5: #HXT |4,6: #H1 #H2 ]
+ lapply (drop_mono … HLK … HLK1) -HLK #H destruct
+ [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ]
+ lapply (fqup_lref … G1 … HLK1) #H
+ lapply (drop_fwd_drop2 … HLK1) /4 width=8 by snv_lift, snv_lref, fqup_fpbg/
+| #p #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
+ elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+ lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct
+ elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1
+ lapply (da_inv_flat … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct
+ lapply (IH1 … HT1 … Hd1 … HT10) /2 width=1 by fqup_fpbg/ #HT0
+ lapply (lstas_scpds_aux … IH1 IH4 IH3 IH2 … Hd1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -d1 #H
+ elim (scpes_inv_abst2 … H) -H /3 width=6 by snv_appl, scpds_cprs_trans/
+| #U1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_cast … H1) -H1
+ lapply (da_inv_flat … Hd1) -Hd1
+ lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_scpes.ma".
+include "basic_2/dynamic/lsubsv_lstas.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on sn parallel reduction for local environments ***************)
+
+fact lstas_cpr_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h o G1 L1 T1.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #_ #_ #_ #_ #d1 #d2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
+ >(lstas_inv_sort1 … H2) -X2
+ >(cpr_inv_sort1 … H3) -X3 /2 width=3 by ex2_intro/
+| #i #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3
+ elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0
+ elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d ] #HLK1 [ #HVd1 | #HWd1 #H destruct ]
+ lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
+ elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #X0 [3,6: #d0 ] #HK0 #HVX0 [1,2: #HX02 #H |3,5: #HX02 |4,6: #H1 #H2 ] destruct
+ lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
+ [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ]
+ lapply (fqup_lref … G1 … HLK1) #HKV1
+ elim (lpr_drop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #W2 | #V2 ] #HK12 [ #HW12 | #HW12 | #HV12 ] #H destruct
+ lapply (drop_fwd_drop2 … HLK2) #H2
+ elim (cpr_inv_lref1 … H3) -H3
+ [1,3,5: #H destruct -HLK1
+ |2,4,6: * #K #V #X #H #HVX #HX3
+ lapply (drop_mono … H … HLK1) -H -HLK1 #H destruct
+ ]
+ [ lapply (IH2 … HWd1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H
+ elim (da_lstas … H d0) -H
+ elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
+ elim (lift_total V2 0 (i+1))
+ /3 width=12 by cpcs_lift, lstas_succ, ex2_intro/
+ | elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0
+ /3 width=5 by fqup_fpbg, lstas_zero, ex2_intro/
+ | elim (IH1 … HVd1 … HVX0 … HV12 … HK12) -IH1 -HVd1 -HVX0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
+ elim (lift_total W2 0 (i+1))
+ /4 width=12 by cpcs_lift, lstas_ldef, ex2_intro/
+ | elim (IH1 … HVd1 … HVX0 … HVX … HK12) -IH1 -HVd1 -HVX0 -HVX -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -d1 #W2 #HXW2 #HW02
+ elim (lift_total W2 0 (i+1))
+ /3 width=12 by cpcs_lift, lstas_lift, ex2_intro/
+ ]
+| #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1
+ elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_bind … H1) -H1 #_ #HT1
+ lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
+ elim (cpr_inv_bind1 … H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH1 … Hd1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hd1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
+ /4 width=5 by cpcs_bind2, lpr_cpr_conf, lstas_bind, ex2_intro/
+ | #T3 #HT13 #HXT3 #H1 #H2 destruct
+ elim (IH1 … Hd1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hd1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+ elim (lstas_inv_lift1 … HTU3 L2 … HXT3) -T3
+ /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, drop_drop, ex2_intro/
+ ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
+ elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1
+ lapply (da_inv_flat … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_appl1 … H2) -H2 #X #HT1U #H destruct
+ elim (cpr_inv_appl1 … H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct -a -d0 -W1 -U1 -HV1 -IH4 -IH3 -IH2
+ elim (IH1 … Hd1 … HT1U … HT12 … HL12) -IH1 -Hd1 -HT1U
+ /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/
+ | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
+ lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
+ elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -d0
+ elim (snv_fwd_da … HW2) #d0 #HW2d
+ lapply (cprs_scpds_div … HW20 … HW2d … HVW1) -W0 #H21
+ elim (snv_fwd_da … HV1) #d #HV1d
+ elim (da_scpes_aux … IH4 IH3 IH2 … HW2d … HV1d … H21) /2 width=1 by fqup_fpbg/ #_ #H
+ <minus_n_O #H0 destruct >(plus_minus_k_k d 1) in HV1d; // -H #HV1d
+ lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
+ lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
+ lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH2 … HW2d … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2d #HW3d
+ lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV1d #HV2d
+ elim (IH1 … Hd1 … HT2U … HT23 (L2.ⓛW3)) -HT2U /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+ elim (lsubsv_lstas_trans … o … HTU3 … Hd21 … (L2.ⓓⓝW3.V2)) -HTU3
+ [ #U4 #HT3U4 #HU43 -IH1 -IH2 -IH3 -IH4 -d -d1 -HW3 -HV2 -HT2
+ @(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4
+ @(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43
+ @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
+ /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
+ | -U3
+ @(lsubsv_beta … (d-1)) /3 width=7 by fqup_fpbg/
+ @shnv_cast [1,2: // ] #d0 #Hd0
+ lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3d … HV2d … d0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3d -HV2d -H32
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
+ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
+ ]
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -d0 -W1 -HV1 -IH4 -IH3 -IH2
+ elim (snv_inv_bind … HT1) -HT1 #_ #HT0
+ lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+ elim (lstas_inv_bind1 … HT1U) -HT1U #U0 #HTU0 #H destruct
+ elim (IH1 … Hd1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hd1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
+ lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
+ lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
+ lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
+ lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02
+ lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?)
+ /4 width=3 by lstas_appl, lstas_bind, cpr_theta, ex2_intro/
+ ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_cast … H1) -H1 #U1 #_ #HT1 #_ #_ -U1
+ lapply (da_inv_flat … Hd1) -Hd1 #Hd1
+ lapply (lstas_inv_cast1 … H2) -H2 #HTU1
+ elim (cpr_inv_cast1 … H3) -H3
+ [ * #U2 #T2 #_ #HT12 #H destruct
+ elim (IH1 … Hd1 … HTU1 … HT12 … HL12) -IH1 -Hd1 -HTU1 -HL12
+ /3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/
+ | #HT1X3 elim (IH1 … Hd1 … HTU1 … HT1X3 … HL12) -IH1 -Hd1 -HTU1 -HL12
+ /2 width=3 by fqup_fpbg, ex2_intro/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fsb_aaa.ma".
+include "basic_2/dynamic/snv_da_lpr.ma".
+include "basic_2/dynamic/snv_lstas.ma".
+include "basic_2/dynamic/snv_lstas_lpr.ma".
+include "basic_2/dynamic/snv_lpr.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Main preservation properties *********************************************)
+
+lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ∧∧ IH_da_cpr_lpr h o G L T
+ & IH_snv_cpr_lpr h o G L T
+ & IH_snv_lstas h o G L T
+ & IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
+#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A
+#G #L #T #A #_ #IH -A @and4_intro
+[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
+| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
+]
+@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
+qed-.
+
+theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
+qed-.
+
+theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
+qed-.
+
+(* Advanced preservation properties *****************************************)
+
+lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.
+
+lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
+#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
+ ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 →
+ ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbg_fpbs.ma".
+include "basic_2/equivalence/scpes_cpcs.ma".
+include "basic_2/equivalence/scpes_scpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
+
+definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
+
+definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+
+definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ∀d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
+ ∀U. ⦃G, L⦄ ⊢ T •*[h, d2] U → ⦃G, L⦄ ⊢ U ¡[h, o].
+
+(* Properties for the preservation results **********************************)
+
+fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_cprs_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
+#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+ ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2.
+#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d1 #Hd1 #T2 #d2 * #T #d0 #Hd20 #H #HT1 #HT2 #L2 #HL12
+lapply (da_mono … H … Hd1) -H #H destruct
+lapply (lstas_da_conf … HT1 … Hd1) #Hd12
+lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
+/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
+qed-.
+
+fact da_scpes_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
+ ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 →
+ ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22.
+#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #d11 #Hd11 #d12 #Hd12 #d21 #d22 * #T #HT1 #HT2
+elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd11 … HT1 … L) -Hd11 -HT1 //
+elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 //
+/3 width=7 by da_mono, and3_intro/
+qed-.
+
+fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (IH1 … Hd21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
+[2: /3 width=12 by da_cprs_lpr_aux/
+|3: /3 width=10 by snv_cprs_lpr_aux/
+|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
+] -G0 -L0 -T0 -T1 -T -d1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #d2 * #W1 #d1 #Hd21 #HTd1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
+lapply (IH2 … H01 … HTd1 … HT12 … HL12) -L0 -T0 // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
+qed-.
+
+fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
+ ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2.
+#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #d1 #d2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
+elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
+elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
+elim (cprs_conf … H1 … H2) -T0
+/3 width=5 by scpds_div, scpds_cprs_trans/
+qed-.
+
+fact lstas_scpds_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L,T. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2
+lapply (da_mono … H … HTd) -H #H destruct
+lapply (lstas_da_conf … HT1 … HTd) #HTd1
+lapply (lstas_da_conf … HTX … HTd) #HXd
+lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?)
+[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2
+elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12)
+[ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd
+ /5 width=6 by lstas_scpds, scpds_div, cprs_strap1, lstas_cpr, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro/
+| elim (da_lstas … HTd1 0) #X1 #HTX1 #_
+ lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
+ elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXd … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXd -HXT1 -HXT2
+ /4 width=8 by cpcs_scpes, cpcs_cpr_conf, fpbg_fpbs_trans, lstas_fpbs, lstas_cpr, monotonic_le_minus_l/
+]
+qed-.
+
+fact scpes_le_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
+ ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20
+elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_
+elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX1 ]
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd12 … HTX2 … HT20) -HT20
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX2 ]
+lapply (lstas_scpes_trans … Hd11 … HTX1 … HX1) [ // ] -Hd11 -HTX1 -HX1 -H1 #H1
+lapply (lstas_scpes_trans … Hd12 … HTX2 … HX2) [ // ] -Hd12 -HTX2 -HX2 -H2 #H2
+/2 width=4 by scpes_canc_dx/ (**) (* full auto fails *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snv_cast_scpes: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ⦃G, L⦄ ⊢ U •*⬌*[h, o, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o].
+#h #o #G #L #U #T #HU #HT * /2 width=3 by snv_cast/
+qed.
T,U,V,W: term
X,Y,Z : reserved: transient objet denoted by a capital letter
-a :
+a : applicability condition (true = restricted, false = general)
b : local dropping kind parameter (true = restricted, false = general)
c : rt-reduction count parameter
d : term degree
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ![ break term 46 a, break term 46 h ] )"
+ non associative with precedence 45
+ for @{ 'Exclaim $a $h $G $L $T }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )"
- non associative with precedence 45
- for @{ 'NativeValid $h $o $G $L $T }.
]
(*
class "wine"
- [ { "" * } {
- [ { "" * } {
- [ [ "" ] "" * ]
- }
- ]
- }
- ]
-(*
[ { "higher order dynamic typing" * } {
[ { "higher order native type assignment" * } {
[ [ "" ] "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
[ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
}
]
-*)
[ { "local env. ref. for stratified native validity" * } {
[ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
}
]
- [ { "stratified native validity" * } {
+*)
+ [ { "native validity" * } {
+(*
[ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
- [ [ "" ] "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ]
+*)
+ [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" (* "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ]
}
]
}
]
+(*
class "prune"
[ { "equivalence" * } {
[ { "decomposed rt-equivalence" * } {
../../matitac.opt `cat partial.txt`
cd basic_2/rt_computation/
../../../../matitac.opt `cat partial.txt`
+cd ../dynamic/
+../../../../matitac.opt `cat partial.txt`
cd ../../
projects / helm.git / commitdiff