--- /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/rt_computation/cpts_cpms.ma".
+include "basic_2/rt_equivalence/cpcs_cpcs.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+include "basic_2/dynamic/cnv_preserve_cpcs.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with t-bound t-computarion for terms **********************)
+
+lemma cpts_cpms_conf_eq (h) (n) (a) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![h,a] → ∀T1. ⦃G,L⦄ ⊢ T0 ⬆*[h,n] T1 →
+ ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#h #a #n #G #L #T0 #HT0 #T1 #HT01 #T2 #HT02
+/3 width=6 by cpts_fwd_cpms, cnv_cpms_conf_eq/
+qed-.
+
+(* Inversion lemmas with t-bound t-computarion for terms ********************)
+
+lemma cnv_inv_cast_cpts (h) (a) (nu) (nt) (G) (L):
+ ∀U1. ⦃G,L⦄ ⊢ U1 ![h,a] → ∀U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,nu] U2 →
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+ ⦃G,L⦄ ⊢ U1 ⬌*[h,nu,nt] T1 → ⦃G,L⦄ ⊢ U2 ⬌*[h] T2.
+#h #a #nu #nt #G #L #U1 #HU1 #U2 #HU12 #T1 #HT1 #T2 #HT12 * #X1 #HUX1 #HTX1
+/3 width=8 by cpts_cpms_conf_eq, cpcs_canc_dx/
+qed-.
+
+lemma cnv_inv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
+ ∀V1. ⦃G,L⦄ ⊢ V1 ![h,a] → ∀V2. ⦃G,L⦄ ⊢ V1 ⬆*[h,nv] V2 →
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+ ∀V0. ⦃G,L⦄ ⊢ V1 ➡*[nv,h] V0 → ∀T0. ⦃G,L⦄ ⊢ T1 ➡*[nt,h] ⓛ{p}V0.T0 →
+ ∃∃W0,U0. ⦃G,L⦄ ⊢ V2 ➡*[h] W0 & ⦃G,L⦄ ⊢ T2 ➡*[h] ⓛ{p}W0.U0.
+#h #a #nv #nt #p #G #L #V1 #HV1 #V2 #HV12 #T1 #HT1 #T2 #HT12 #V0 #HV20 #T0 #HT20
+lapply (cpts_cpms_conf_eq … HV1 … HV12 … HV20) -nv -V1 #HV20
+lapply (cpts_cpms_conf_eq … HT1 … HT12 … HT20) -nt -T1 #HT20
+lapply (cpcs_bind_sn … Abst … T0 HV20 p) -HV20 #HV20
+lapply (cpcs_canc_dx … HT20 … HV20) -V0 #HT20
+elim (cpcs_inv_cprs … HT20) -HT20 #X #HT2X #HT0X
+elim (cpms_inv_abst_sn … HT0X) -HT0X #V0 #X0 #HV20 #_ #H destruct
+/2 width=4 by ex2_2_intro/
+qed-.
+
+(* Properties with t-bound t-computarion for terms **************************)
+
+lemma cnv_cast_cpts (h) (a) (nu) (nt) (G) (L):
+ ∀U1. ⦃G,L⦄ ⊢ U1 ![h,a] → ∀U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,nu] U2 →
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+ ⦃G,L⦄ ⊢ U2 ⬌*[h] T2 → ⦃G,L⦄ ⊢ U1 ⬌*[h,nu,nt] T1.
+#h #a #nu #nt #G #L #U1 #HU1 #U2 #HU12 #T1 #HT1 #T2 #HT12 #HUT2
+elim (cpcs_inv_cprs … HUT2) -HUT2 #X2 #HUX2 #HTX2
+/3 width=5 by cpts_cprs_trans, cpms_div/
+qed-.
+
+lemma cnv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
+ ∀V1. ⦃G,L⦄ ⊢ V1 ![h,a] → ∀V2. ⦃G,L⦄ ⊢ V1 ⬆*[h,nv] V2 →
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+ ∀V0. ⦃G,L⦄ ⊢ V2 ➡*[h] V0 → ∀T0. ⦃G,L⦄ ⊢ T2 ➡*[h] ⓛ{p}V0.T0 →
+ ∃∃W0,U0. ⦃G,L⦄ ⊢ V1 ➡*[nv,h] W0 & ⦃G,L⦄ ⊢ T1 ➡*[nt,h] ⓛ{p}W0.U0.
+#h #a #nv #nt #p #G #L #V1 #HV1 #V2 #HV12 #T1 #HT1 #T2 #HT12 #V0 #HV20 #T0 #HT20
+/3 width=6 by cpts_cprs_trans, ex2_2_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 "ground_2/lib/ltc.ma".
+include "basic_2/notation/relations/ptystar_6.ma".
+include "basic_2/rt_transition/cpt.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+definition cpts (h) (G) (L): relation3 nat term term ≝
+ ltc … plus … (cpt h G L).
+
+interpretation
+ "t-bound context-sensitive parallel t-computarion (term)"
+ 'PTyStar h n G L T1 T2 = (cpts h G L n T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cpts_ind_sn (h) (G) (L) (T2) (Q:relation2 …):
+ Q 0 T2 →
+ (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T → ⦃G,L⦄ ⊢ T ⬆*[h,n2] T2 → Q n2 T → Q (n1+n2) T1) →
+ ∀n,T1. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → Q n T1.
+#h #G #L #T2 #Q @ltc_ind_sn_refl //
+qed-.
+
+lemma cpts_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
+ Q 0 T1 →
+ (∀n1,n2,T,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n1] T → Q n1 T → ⦃G,L⦄ ⊢ T ⬆[h,n2] T2 → Q (n1+n2) T2) →
+ ∀n,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → Q n T2.
+#h #G #L #T1 #Q @ltc_ind_dx_refl //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cpt_cpts (h) (G) (L):
+ ∀n,T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2.
+/2 width=1 by ltc_rc/ qed.
+
+lemma cpts_step_sn (h) (G) (L):
+ ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T ⬆*[h,n2] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n1+n2] T2.
+/2 width=3 by ltc_sn/ qed-.
+
+lemma cpts_step_dx (h) (G) (L):
+ ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ⬆*[h,n1] T →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T ⬆[h,n2] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n1+n2] T2.
+/2 width=3 by ltc_dx/ qed-.
+
+lemma cpts_bind_dx (h) (n) (G) (L):
+ ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
+ ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆*[h,n] T2 →
+ ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆*[h,n] ⓑ{p,I}V2.T2.
+#h #n #G #L #V1 #V2 #HV12 #I #T1 #T2 #H #a @(cpts_ind_sn … H) -T1
+/3 width=3 by cpts_step_sn, cpt_cpts, cpt_bind/ qed.
+
+lemma cpts_appl_dx (h) (n) (G) (L):
+ ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆*[h,n] ⓐV2.T2.
+#h #n #G #L #V1 #V2 #HV12 #T1 #T2 #H @(cpts_ind_sn … H) -T1
+/3 width=3 by cpts_step_sn, cpt_cpts, cpt_appl/
+qed.
+
+lemma cpts_ee (h) (n) (G) (L):
+ ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 →
+ ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆*[h,↑n] U2.
+#h #n #G #L #U1 #U2 #H @(cpts_ind_sn … H) -U1 -n
+[ /3 width=1 by cpt_cpts, cpt_ee/
+| #n1 #n2 #U1 #U #HU1 #HU2 #_ #T >plus_S1
+ /3 width=3 by cpts_step_sn, cpt_ee/
+]
+qed.
+
+lemma cpts_refl (h) (G) (L): reflexive … (cpts h G L 0).
+/2 width=1 by cpt_cpts/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma cpts_sort (h) (G) (L) (n):
+ ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆*[h,n] ⋆((next h)^n s).
+#h #G #L #n elim n -n [ // ]
+#n #IH #s <plus_SO_dx
+/3 width=3 by cpts_step_dx, cpt_sort/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpts_inv_sort_sn (h) (n) (G) (L) (s):
+ ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆*[h,n] X2 → X2 = ⋆(((next h)^n) s).
+#h #n #G #L #s #X2 #H @(cpts_ind_dx … H) -X2 //
+#n1 #n2 #X #X2 #_ #IH #HX2 destruct
+elim (cpt_inv_sort_sn … HX2) -HX2 #H #_ destruct //
+qed-.
+
+lemma cpts_inv_lref_sn_ctop (h) (n) (G) (i):
+ ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆*[h,n] X2 → ∧∧ X2 = #i & n = 0.
+#h #n #G #i #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpt_inv_lref_sn_ctop … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_zero_sn_unit (h) (n) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆*[h,n] X2 → ∧∧ X2 = #0 & n = 0.
+#h #n #I #G #K #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpt_inv_zero_sn_unit … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_gref_sn (h) (n) (G) (L) (l):
+ ∀X2. ⦃G,L⦄ ⊢ §l ⬆*[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpt_inv_gref_sn … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_cast_sn (h) (n) (G) (L) (U1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆*[h,n] X2 →
+ ∨∨ ∃∃U2,T2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 & ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 & X2 = ⓝU2.T2
+ | ∃∃m. ⦃G,L⦄ ⊢ U1 ⬆*[h,m] X2 & n = ↑m.
+#h #n #G #L #U1 #T1 #X2 #H @(cpts_ind_dx … H) -n -X2
+[ /3 width=5 by or_introl, ex3_2_intro/
+| #n1 #n2 #X #X2 #_ * *
+ [ #U #T #HU1 #HT1 #H #HX2 destruct
+ elim (cpt_inv_cast_sn … HX2) -HX2 *
+ [ #U2 #T2 #HU2 #HT2 #H destruct
+ /4 width=5 by cpts_step_dx, ex3_2_intro, or_introl/
+ | #m #HX2 #H destruct <plus_n_Sm
+ /4 width=3 by cpts_step_dx, ex2_intro, or_intror/
+ ]
+ | #m #HX #H #HX2 destruct
+ /4 width=3 by cpts_step_dx, ex2_intro, or_intror/
+ ]
+]
+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 "static_2/static/aaa.ma".
+include "basic_2/rt_computation/cpts_drops.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+lemma cpts_total_aaa (h) (G) (L) (T1):
+ ∀A. ⦃G,L⦄ ⊢ T1 ⁝ A → ∀n. ∃T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2.
+#h #G #L #T1 #A #H elim H -G -L -T1 -A
+[ #G #L #s #n /3 width=2 by ex_intro/
+| #I #G #K #V1 #B #_ #IH #n -B
+ cases I -I
+ [ elim (IH n) -IH #V2 #HV12
+ elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+ /3 width=4 by cpts_delta, ex_intro/
+ | cases n -n
+ [ /2 width=2 by ex_intro/
+ | #n elim (IH n) -IH #V2 #HV12
+ elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+ /3 width=4 by cpts_ell, ex_intro/
+ ]
+ ]
+| #I #G #K #A #i #_ #IH #n -A
+ elim (IH n) -IH #T #HT
+ elim (lifts_total T (𝐔❴1❵)) #U #HTU
+ /3 width=4 by cpts_lref, ex_intro/
+| #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+ elim (IHV 0) -IHV #V2 #HV12
+ elim (IHT n) -IHT #T2 #HT12
+ /3 width=3 by cpts_bind_dx, ex_intro/
+| #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+ elim (IHV 0) -IHV #V2 #HV12
+ elim (IHT n) -IHT #T2 #HT12
+ /3 width=3 by cpts_bind_dx, ex_intro/
+| #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+ elim (IHV 0) -IHV #V2 #HV12
+ elim (IHT n) -IHT #T2 #HT12
+ /3 width=3 by cpts_appl_dx, ex_intro/
+| #G #L #U1 #T1 #A #_ #_ #IHU #_ #n -A
+ cases n -n
+ [ /2 width=2 by ex_intro/
+ | #n elim (IHU n) -IHU #U2 #HU12
+ /3 width=3 by cpts_ee, 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/rt_transition/cpt_cpm.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_computation/cpts.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Forward lemmas with t-bound rt-computation for terms *********************)
+
+lemma cpts_fwd_cpms (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 #H
+@(cpts_ind_dx … H) -n -T2 [ // ]
+#n1 #n2 #T #T2 #_ #IH #HT2
+/3 width=3 by cpms_step_dx, cpt_fwd_cpm/
+qed-.
+
+lemma cpts_cprs_trans (h) (n) (G) (L) (T):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T →
+ ∀T2. ⦃G,L⦄ ⊢ T ➡*[h] T2 → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T #T1 #HT1 #T2 #HT2
+/3 width=3 by cpts_fwd_cpms, cpms_cprs_trans/ 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 "static_2/relocation/drops_ltc.ma".
+include "basic_2/rt_transition/cpt_drops.ma".
+include "basic_2/rt_computation/cpts.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Properties with generic slicing for local environments *******************)
+
+lemma cpts_lifts_sn (h) (n) (G):
+ d_liftable2_sn … lifts (λL. cpts h G L n).
+/3 width=6 by d2_liftable_sn_ltc, cpt_lifts_sn/ qed-.
+
+lemma cpts_lifts_bi (h) (n) (G):
+ d_liftable2_bi … lifts (λL. cpts h G L n).
+#h #n #G @d_liftable2_sn_bi
+/2 width=6 by cpts_lifts_sn, lifts_mono/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma cpts_inv_lifts_sn (h) (n) (G):
+ d_deliftable2_sn … lifts (λL. cpts h G L n).
+/3 width=6 by d2_deliftable_sn_ltc, cpt_inv_lifts_sn/ qed-.
+
+lemma cpts_inv_lifts_bi (h) (n) (G):
+ d_deliftable2_bi … lifts (λL. cpts h G L n).
+#h #n #G @d_deliftable2_sn_bi
+/2 width=6 by cpts_inv_lifts_sn, lifts_inj/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpts_delta (h) (n) (G):
+ ∀K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆*[h,n] V2 →
+ ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆*[h,n] W2.
+#h #n #G #K #V1 #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=3 by cpt_cpts, cpt_delta/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+ elim (lifts_total V (𝐔❴1❵)) #W #HVW
+ /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_ell (h) (n) (G):
+ ∀K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆*[h,n] V2 →
+ ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆*[h,↑n] W2.
+#h #n #G #K #V1 #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=3 by cpt_cpts, cpt_ell/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+ elim (lifts_total V (𝐔❴1❵)) #W #HVW >plus_S1
+ /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_lref (h) (n) (I) (G):
+ ∀K,T,i. ⦃G,K⦄ ⊢ #i ⬆*[h,n] T →
+ ∀U. ⇧*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆*[h,n] U.
+#h #n #I #G #K #T #i #H @(cpts_ind_dx … H) -T
+[ /3 width=3 by cpt_cpts, cpt_lref/
+| #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2
+ elim (lifts_total T (𝐔❴1❵)) #U #TU
+ /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_cast_sn (h) (n) (G) (L):
+ ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 →
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆*[h,n] ⓝU2.T2.
+#h #n #G #L #U1 #U2 #H @(cpts_ind_sn … H) -U1 -n
+[ /3 width=3 by cpt_cpts, cpt_cast/
+| #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H
+ elim (cpt_fwd_plus … H) -H #T #HT1 #HT2
+ /3 width=3 by cpts_step_sn, cpt_cast/
+]
+qed.
+
+lemma cpts_delta_drops (h) (n) (G):
+ ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV →
+ ∀V2. ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 →
+ ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆*[h,n] W2.
+#h #n #G #L #K #V #i #HLK #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=6 by cpt_cpts, cpt_delta_drops/
+| #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2
+ lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+ elim (lifts_total V1 (𝐔❴↑i❵)) #W1 #HVW1
+ /3 width=11 by cpt_lifts_bi, cpts_step_dx/
+]
+qed.
+
+lemma cpts_ell_drops (h) (n) (G):
+ ∀L,K,W,i. ⇩*[i] L ≘ K.ⓛW →
+ ∀W2. ⦃G,K⦄ ⊢ W ⬆*[h,n] W2 →
+ ∀V2. ⇧*[↑i] W2 ≘ V2 → ⦃G,L⦄ ⊢ #i ⬆*[h,↑n] V2.
+#h #n #G #L #K #W #i #HLK #W2 #H @(cpts_ind_dx … H) -W2
+[ /3 width=6 by cpt_cpts, cpt_ell_drops/
+| #n1 #n2 #W1 #W2 #_ #IH #HW12 #V2 #HWV2
+ lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+ elim (lifts_total W1 (𝐔❴↑i❵)) #V1 #HWV1 >plus_S1
+ /3 width=11 by cpt_lifts_bi, cpts_step_dx/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpts_inv_lref_sn_drops (h) (n) (G) (L) (i):
+ ∀X2. ⦃G,L⦄ ⊢ #i ⬆*[h,n] X2 →
+ ∨∨ ∧∧ X2 = #i & n = 0
+ | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 & ⇧*[↑i] V2 ≘ X2
+ | ∃∃m,K,V,V2. ⇩*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬆*[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & n = ↑m.
+#h #n #G #L #i #X2 #H @(cpts_ind_dx … H) -X2
+[ /3 width=1 by or3_intro0, conj/
+| #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH *
+ [ #H1 #H2 destruct
+ elim (cpt_inv_lref_sn_drops … HT2) -HT2 *
+ [ /3 width=1 by or3_intro0, conj/
+ | /4 width=6 by cpt_cpts, or3_intro1, ex3_3_intro/
+ | /4 width=8 by cpt_cpts, or3_intro2, ex4_4_intro/
+ ]
+ | #K #V0 #V #HLK #HV0 #HVT
+ lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+ elim (cpt_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+ /4 width=6 by cpts_step_dx, ex3_3_intro, or3_intro1/
+ | #m #K #V0 #V #HLK #HV0 #HVT #H destruct
+ lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+ elim (cpt_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+ /4 width=8 by cpts_step_dx, ex4_4_intro, or3_intro2/
+ ]
+]
+qed-.
+
+lemma cpts_inv_delta_sn (h) (n) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬆*[h,n] X2 →
+ ∨∨ ∧∧ X2 = #0 & n = 0
+ | ∃∃V2. ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 & ⇧*[1] V2 ≘ X2.
+#h #n #G #K #V #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=3 by ex2_intro, or_intror/
+| #m #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+]
+qed-.
+
+lemma cpts_inv_ell_sn (h) (n) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 ⬆*[h,n] X2 →
+ ∨∨ ∧∧ X2 = #0 & n = 0
+ | ∃∃m,V2. ⦃G,K⦄ ⊢ V ⬆*[h,m] V2 & ⇧*[1] V2 ≘ X2 & n = ↑m.
+#h #n #G #K #V #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+| #m #Y #X #V2 #H #HV2 #HVT2 #H0 destruct
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=5 by ex3_2_intro, or_intror/
+]
+qed-.
+
+lemma cpts_inv_lref_sn (h) (n) (I) (G) (K) (i):
+ ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆*[h,n] X2 →
+ ∨∨ ∧∧ X2 = #↑i & n = 0
+ | ∃∃T2. ⦃G,K⦄ ⊢ #i ⬆*[h,n] T2 & ⇧*[1] T2 ≘ X2.
+#h #n #I #G #K #i #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #L #V #V2 #H #HV2 #HVU2
+ lapply (drops_inv_drop1 … H) -H #HLK
+ elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+ [| // ] #T2 #HVT2 #HTU2
+ /4 width=6 by cpts_delta_drops, ex2_intro, or_intror/
+| #m #L #V #V2 #H #HV2 #HVU2 #H0 destruct
+ lapply (drops_inv_drop1 … H) -H #HLK
+ elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+ [| // ] #T2 #HVT2 #HTU2
+ /4 width=6 by cpts_ell_drops, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpts_inv_succ_sn (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,↑n] T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆*[h,1] T & ⦃G,L⦄ ⊢ T ⬆*[h,n] T2.
+#h #n #G #L #T1 #T2
+@(insert_eq_0 … (↑n)) #m #H
+@(cpts_ind_sn … H) -T1 -m
+[ #H destruct
+| #x1 #n2 #T1 #T #HT1 #HT2 #IH #H
+ elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H
+ [ #H1 #H2 destruct -HT2
+ elim IH -IH // #T0 #HT0 #HT02
+ /3 width=3 by cpts_step_sn, ex2_intro/
+ | #n1 #H1 #H2 destruct -IH
+ elim (cpt_fwd_plus … 1 n1 … T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0
+ /3 width=5 by cpts_step_sn, cpt_cpts, ex2_intro/
+ ]
+]
+qed-.
/3 width=3 by cpg_ee, ist_succ, ex2_intro/
qed.
-(* Basic properties *********************************************************)
-
lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
/3 width=3 by cpg_refl, ex2_intro/ qed.
+(* Advanced properties ******************************************************)
+
+lemma cpt_sort (h) (G) (L):
+ ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
+#h #G #L * //
+#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
]
qed-.
+lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
+ ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
+ ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
+#h #n #G #L #s #X2 * #c #Hc #H
+elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma cpt_inv_zero_sn (h) (n) (G) (L):
+ ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = #0 & n = 0
+ | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
+ | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
+#h #n #G #L #X2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+ /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+ elim (ist_inv_plus_SO_dx … H2) -H2 // #m #Hc #H destruct
+ /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
+]
+qed-.
+
+lemma cpt_inv_zero_sn_unit (h) (n) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆[h,n] X2 → ∧∧ X2 = #0 & n = 0.
+#h #n #I #G #K #X2 #H
+elim (cpt_inv_zero_sn … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
+ ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = #(↑i) & n = 0
+ | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
+#h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
+[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/
+| #I #K #V2 #HV2 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpt_inv_lref_sn_ctop (n) (h) (G) (i):
+ ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆[h,n] X2 → ∧∧ X2 = #i & n = 0.
+#h #n #G * [| #i ] #X2 #H
+[ elim (cpt_inv_zero_sn … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpt_inv_lref_sn … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+
+lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
+ ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
+#H1 #H2 destruct /2 width=1 by conj/
+qed-.
+
lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2
(**************************************************************************)
include "basic_2/rt_transition/cpg_drops.ma".
-include "basic_2/rt_transition/cpt.ma".
+include "basic_2/rt_transition/cpt_fqu.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
d_deliftable2_bi … lifts (λL. cpt h G L n).
#h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpt_delta_drops (h) (n) (G):
+ ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV → ∀V2. ⦃G,K⦄ ⊢ V ⬆[h,n] V2 →
+ ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆[h,n] W2.
+#h #n #G #L #K #V #i #HLK #V2 *
+/3 width=8 by cpg_delta_drops, ex2_intro/
+qed.
+
+lemma cpt_ell_drops (h) (n) (G):
+ ∀L,K,V,i. ⇩*[i] L ≘ K.ⓛV → ∀V2. ⦃G,K⦄ ⊢ V ⬆[h,n] V2 →
+ ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆[h,↑n] W2.
+#h #n #G #L #K #V #i #HLK #V2 *
+/3 width=8 by cpg_ell_drops, ist_succ, ex2_intro/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpt_inv_atom_sn_drops (h) (n) (I) (G) (L):
+ ∀X2. ⦃G,L⦄ ⊢ ⓪{I} ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = ⓪{I} & n = 0
+ | ∃∃s. X2 = ⋆(⫯[h]s) & I = Sort s & n = 1
+ | ∃∃K,V,V2,i. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i
+ | ∃∃m,K,V,V2,i. ⇩*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i & n = ↑m.
+#h #n #I #G #L #X2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
+[ #H1 #H2 destruct
+ /3 width=1 by or4_intro0, conj/
+| #s #H1 #H2 #H3 destruct
+ /3 width=3 by or4_intro1, ex3_intro/
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+ /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+ elim (ist_inv_plus_SO_dx … H2) -H2
+ /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
+]
+qed-.
+
+lemma cpt_inv_lref_sn_drops (h) (n) (G) (L) (i):
+ ∀X2. ⦃G,L⦄ ⊢ #i ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = #i & n = 0
+ | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2
+ | ∃∃m,K,V,V2. ⇩*[i] L ≘ K. ⓛV & ⦃G,K⦄ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & n = ↑m.
+#h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
+[ #H1 #H2 destruct
+ /3 width=1 by or3_intro0, conj/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+ elim (ist_inv_plus_SO_dx … H) -H
+ /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+fact cpt_fwd_plus_aux (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ∀n1,n2. n1+n2 = n →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T & ⦃G,L⦄ ⊢ T ⬆[h,n2] T2.
+#h #n #G #L #T1 #T2 #H @(cpt_ind … H) -G -L -T1 -T2 -n
+[ #I #G #L #n1 #n2 #H
+ elim (plus_inv_O3 … H) -H #H1 #H2 destruct
+ /2 width=3 by ex2_intro/
+| #G #L #s #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct /2 width=3 by ex2_intro/
+ | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
+ /2 width=3 by ex2_intro/
+ ]
+| #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #V #HV1 #HV2
+ elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+ /5 width=11 by cpt_lifts_bi, cpt_delta, drops_refl, drops_drop, ex2_intro/
+| #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct -IH /3 width=3 by cpt_ell, ex2_intro/
+ | #n1 #H1 #H2 destruct -HV12
+ elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
+ elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+ /5 width=11 by cpt_lifts_bi, cpt_ell, drops_refl, drops_drop, ex2_intro/
+ ]
+| #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ elim (lifts_total T 𝐔❴↑O❵) #U #HTU
+ /5 width=11 by cpt_lifts_bi, cpt_lref, drops_refl, drops_drop, ex2_intro/
+| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpt_bind, ex2_intro/
+| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpt_appl, ex2_intro/
+| #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
+ elim IHU [|*: // ] -IHU #U #HU1 #HU2
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpt_cast, ex2_intro/
+| #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct -IH /3 width=4 by cpt_ee, cpt_cast, ex2_intro/
+ | #n1 #H1 #H2 destruct -HU12
+ elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
+ /3 width=3 by cpt_ee, ex2_intro/
+ ]
+]
+qed-.
+
+lemma cpt_fwd_plus (h) (n1) (n2) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n1+n2] T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T & ⦃G,L⦄ ⊢ T ⬆[h,n2] T2.
+/2 width=3 by cpt_fwd_plus_aux/ qed-.
(i.e. no induction on the degree).
</news>
<news class="beta" date="2018 November 1.">
- Extended (λδ-2A) and restricted (λδ-1A) type rules justified.
+ Extended (λδ-2A) and restricted (λδ-1B) validity rules justified.
</news>
<news class="alpha" date="2018 September 21.">
λδ-2A completed with
λδ-2A appears too complex and is dismissed.
</news>
<news class="gamma" date="2014 October 28.">
- λδ version 2A is released.
+ λδ-2A is released.
</news>
<news class="beta" date="2014 September 9.">
Iterated static type assignment defined (more elegantly)
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_cpts" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" + "cnv_eval" * ]
}
]
}
]
class "sky"
[ { "rt-computation" * } {
+ [ { "context-sensitive parallel t-computation" * } {
+ [ [ "for terms" ] "cpts" + "( ⦃?,?⦄ ⊢ ? ⬆*[?,?] ? )" "cpts_drops" + "cpts_aaa" + "cpts_cpms" * ]
+ }
+ ]
[ { "context-sensitive parallel r-computation" * } {
[ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_csx" + "cpre_cpms" + "cpre_cpre" * ]
[ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
projects / helm.git / commitdiff