--- /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/gcp_aaa.ma".
+include "basic_2/rt_computation/cpxs_aaa.ma".
+include "basic_2/rt_computation/csx_gcp.ma".
+include "basic_2/rt_computation/csx_gcr.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+
+(* Main properties with atomic arity assignment *****************************)
+
+theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L #T #A #H
+@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H)
+qed.
+
+(* Advanced eliminators *****************************************************)
+
+fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
+ (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
+#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
+qed-.
+
+lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
+ (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
+
+fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
+ (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
+#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
+qed-.
+
+(* Basic_2A1: was: aaa_ind_csx_alt *)
+lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
+ (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⬈ * [ break term 46 h , break term 46 o , break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedTySNStrong $h $o $T $G $L }.
+++ /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( G ⊢ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
- non associative with precedence 45
- for @{ 'SN $h $o $T $f $G $L }.
+++ /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( G ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
- non associative with precedence 45
- for @{ 'SNAlt $h $o $T $f $G $L }.
/3 width=1 by lexs_atom, lexs_next, lexs_push/
qed-.
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
+ (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) →
+ ∀f,L1,L2. L1 ⦻*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
+ L1 ⦻*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
+#f #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+]
+qed-.
+
lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 →
∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
--- /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/reduction/lpx_aaa.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+#h #o #G #L #T1 #A #HT1 #T2 #HT12
+@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
+qed-.
+
+lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/lpx_aaa.ma".
-include "basic_2/computation/cpxs.ma".
+include "basic_2/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_computation/cpxs.ma".
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
-(* Properties about atomic arity assignment on terms ************************)
+(* Properties with atomic arity assignment on terms *************************)
-lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-#h #o #G #L #T1 #A #HT1 #T2 #HT12
+lemma cpxs_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+#h #G #L #T1 #A #HT1 #T2 #HT12
@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
qed-.
-
-lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ 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/gcp_aaa.ma".
-include "basic_2/computation/cpxs_aaa.ma".
-include "basic_2/computation/csx_theq_vector.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Main properties on atomic arity assignment *******************************)
-
-theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L #T #A #H
-@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H)
-qed.
-
-(* Advanced eliminators *****************************************************)
-
-fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
-qed-.
-
-lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
-/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
-
-fact aaa_ind_csx_alt_aux: ∀h,o,G,L,A. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by cpxs_aaa_conf/
-qed-.
-
-lemma aaa_ind_csx_alt: ∀h,o,G,L,A. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
-/5 width=9 by aaa_ind_csx_alt_aux, aaa_csx/ 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/predtysnstrong_5.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
+ λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
+
+interpretation
+ "strong normalization for uncounted context-sensitive parallel rt-transition on referred entries (local environment)"
+ 'PRedTySNStrong h o T G L = (lfsx h o T G L).
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: was: lsx_ind *)
+lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
+#h #o #G #T #R #H0 #L1 #H elim H -L1
+/5 width=1 by lfdeq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: was: lsx_intro *)
+lemma lfsx_intro: ∀h,o,G,L1,T.
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+/5 width=1 by lfdeq_sym, SN_intro/ qed.
+(*
+lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
+[ #H1 #H2 destruct //
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
+ @lfdeq_sort
+qed.
+
+lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L.
+#h #o #G #L1 #l #p @lfsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lfpx_fwd_length, lfdeq_gref/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L.
+#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/
+qed-.
+
+lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
+qed-.
+
+lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, T, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
+qed-.
+
+lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L.
+#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
+/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
+
+(* Basic_2A1: removed theorems 5:
+ lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge
+*)
+*)
--- /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/lfdeq_fqus.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was: lsx_atom *)
+lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
+#h #o #G #T @lfsx_intro
+#Y #H #HI lapply (lfpx_inv_atom_sn … H) -H
+#H destruct elim HI -HI //
+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/sn_6.ma".
-include "basic_2/multiple/lleq.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝
- λh,o,l,T,G. SN … (lpx h o G) (lleq l T).
-
-interpretation
- "extended strong normalization (local environment)"
- 'SN h o l T G L = (lsx h o T l G L).
-
-(* Basic eliminators ********************************************************)
-
-lemma lsx_ind: ∀h,o,G,T,l. ∀R:predicate lenv.
- (∀L1. G ⊢ ⬊*[h, o, T, l] L1 →
- (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. G ⊢ ⬊*[h, o, T, l] L → R L.
-#h #o #G #T #l #R #H0 #L1 #H elim H -L1
-/5 width=1 by lleq_sym, SN_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsx_intro: ∀h,o,G,L1,T,l.
- (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊*[h, o, T, l] L2) →
- G ⊢ ⬊*[h, o, T, l] L1.
-/5 width=1 by lleq_sym, SN_intro/ qed.
-
-lemma lsx_atom: ∀h,o,G,T,l. G ⊢ ⬊*[h, o, T, l] ⋆.
-#h #o #G #T #l @lsx_intro
-#X #H #HT lapply (lpx_inv_atom1 … H) -H
-#H destruct elim HT -HT //
-qed.
-
-lemma lsx_sort: ∀h,o,G,L,l,s. G ⊢ ⬊*[h, o, ⋆s, l] L.
-#h #o #G #L1 #l #s @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpx_fwd_length, lleq_sort/
-qed.
-
-lemma lsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬊*[h, o, §p, l] L.
-#h #o #G #L1 #l #p @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpx_fwd_length, lleq_gref/
-qed.
-
-lemma lsx_ge_up: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l + yinj k →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → G ⊢ ⬊*[h, o, U, l] L.
-#h #o #G #L #T #U #lt #l #k #Hltlm #HTU #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge_up/
-qed-.
-
-lemma lsx_ge: ∀h,o,G,L,T,l1,l2. l1 ≤ l2 →
- G ⊢ ⬊*[h, o, T, l1] L → G ⊢ ⬊*[h, o, T, l2] L.
-#h #o #G #L #T #l1 #l2 #Hl12 #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓑ{a,I}V.T, l] L →
- G ⊢ ⬊*[h, o, V, l] L.
-#h #o #a #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/
-qed-.
-
-lemma lsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬊*[h, o, V, l] L.
-#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/
-qed-.
-
-lemma lsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬊*[h, o, T, l] L.
-#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/
-qed-.
-
-lemma lsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ②{I}V.T, l] L →
- G ⊢ ⬊*[h, o, V, l] L.
-#h #o * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬊*[h, o, V, l] L ∧ G ⊢ ⬊*[h, o, T, l] L.
-/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-.
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
+lfsx.ma lfsx_fqup.ma
(* Basic inversion lemmas ***************************************************)
-lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = ⋆.
+lemma lfpx_inv_atom_sn: ∀h,G,Y2,T. ⦃G, ⋆⦄ ⊢ ⬈[h, T] Y2 → Y2 = ⋆.
/2 width=3 by lfxs_inv_atom_sn/ qed-.
-lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 →
(* Basic inversion lemmas ***************************************************)
-lemma lfdeq_inv_atom_sn: ∀h,o,I,Y2. ⋆ ≡[h, o, ⓪{I}] Y2 → Y2 = ⋆.
+lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆.
/2 width=3 by lfxs_inv_atom_sn/ qed-.
-lemma lfdeq_inv_atom_dx: ∀h,o,I,Y1. Y1 ≡[h, o, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 →
(* Basic inversion lemmas ***************************************************)
-lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.
-#R #I #Y2 * /2 width=4 by lexs_inv_atom1/
+lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆.
+#R #Y2 #T * /2 width=4 by lexs_inv_atom1/
qed-.
-lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfxs_inv_atom_dx: ∀R,Y1,T. Y1 ⦻*[R, T] ⋆ → Y1 = ⋆.
#R #I #Y1 * /2 width=4 by lexs_inv_atom2/
qed-.
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
projects / helm.git / commitdiff