(* *)
(**************************************************************************)
+include "basic_2/rt_computation/cpmuwe_cpmuwe.ma".
include "basic_2/rt_conversion/cpce_drops.ma".
-include "basic_2/dynamic/cnv_cpmhe.ma".
+include "basic_2/dynamic/cnv_cpmuwe.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ]
[ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W
lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W
- elim (cpmhe_total_csx … H1W) -H1W #X #n #HWX
+ elim (cpmuwe_total_csx … H1W) -H1W #X #n #HWX
elim (abst_dec X) [ * | -IH ]
[ #p #V1 #U #H destruct
- lapply (cpmhe_fwd_cpms … HWX) -HWX #HWX
+ lapply (cpmuwe_fwd_cpms … HWX) -HWX #HWX
elim (IH G K V1) -IH
[ #V2 #HV12
elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2
@(ex_intro … (#i))
@cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0
lapply (drops_mono … HLK0 … HLK) -i -L #H destruct
- lapply (cpmhe_abst … HWU0) -HWU0 #HWU0
- elim (cnv_cpmhe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W
- elim (theq_inv_pair1 … H) -V0 -U0 #V0 #U0 #H destruct
+ lapply (cpmuwe_abst … HWU0) -HWU0 #HWU0
+ elim (cnv_cpmuwe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W
+ elim (tweq_inv_abst_sn … H) -V0 -U0 #V0 #U0 #H destruct
/2 width=4 by/
]
| /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/
+++ /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/cpms_cnh.ma".
-include "basic_2/rt_computation/cpmhe_csx.ma".
-include "basic_2/rt_equivalence/cpes.ma".
-include "basic_2/dynamic/cnv_preserve.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Properties with head evaluation for t-bound rt-transition on terms *******)
-
-lemma cnv_cpmhe_trans (a) (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
- ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
-/3 width=4 by cpmhe_fwd_cpms, cnv_cpms_trans/ qed-.
-
-lemma cnv_R_cpmhe_total (a) (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmhe h G L T1 n.
-/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmhe_total_csx/ qed-.
-
-axiom cnv_R_cpmhe_dec (a) (h) (G) (L):
- ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmhe h G L T n).
-
-(* Main inversions with head evaluation for t-bound rt-transition on terms **)
-
-theorem cnv_cpmhe_mono (a) (h) (G) (L):
- ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*[h,n1] 𝐍*⦃T1⦄ →
- ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*[h,n2] 𝐍*⦃T2⦄ →
- ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ⩳ T2.
-#a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2
-elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
-/4 width=8 by cpms_div, cpms_inv_cnh_sn, theq_canc_dx, conj/
-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_computation/cpmuwe_csx.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with head evaluation for t-bound rt-transition on terms *******)
+
+lemma cnv_cpmuwe_trans (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
+/3 width=4 by cpmuwe_fwd_cpms, cnv_cpms_trans/ qed-.
+
+lemma cnv_R_cpmuwe_total (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n.
+/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
+
+axiom cnv_R_cpmuwe_dec (a) (h) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
+
+(* Main inversions with head evaluation for t-bound rt-transition on terms **)
+
+theorem cnv_cpmuwe_mono (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 →
+ ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 →
+ ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ≅ T2.
+#a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+/4 width=4 by cpms_div, tweq_canc_dx, conj/
+qed-.
(* *)
(**************************************************************************)
+include "basic_2/rt_computation/cpmuwe_cpmuwe.ma".
include "basic_2/rt_equivalence/cpes_cpes.ma".
-include "basic_2/dynamic/cnv_cpmhe.ma".
+include "basic_2/dynamic/cnv_cpmuwe.ma".
include "basic_2/dynamic/cnv_cpes.ma".
include "basic_2/dynamic/cnv_preserve_cpes.ma".
elim (IH G L V) [| -IH #HV | // ]
[ elim (IH G L T) -IH [| #HT #HV | // ]
[ #HT #HV
- elim (cnv_R_cpmhe_total … HT) #n #Hn
- elim (dec_min (R_cpmhe h G L T) … Hn) -Hn
- [| /2 width=2 by cnv_R_cpmhe_dec/ ] #n0 #_ -n
+ elim (cnv_R_cpmuwe_total … HT) #n #Hn
+ elim (dec_min (R_cpmuwe h G L T) … Hn) -Hn
+ [| /2 width=2 by cnv_R_cpmuwe_dec/ ] #n0 #_ -n
elim (ac_dec … Ha n0) -Ha
[ * #n #Hn #Ha * #X0 #HX0 #_
elim (abst_dec X0)
[ * #p #W #U0 #H destruct
elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
- [ lapply (cpmhe_fwd_cpms … HX0) -HX0 #HTU0
+ [ lapply (cpmuwe_fwd_cpms … HX0) -HX0 #HTU0
elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0
/3 width=7 by cnv_appl_cpes, or_introl/
(* Note: argument type mismatch *)
| @or_intror #H -n
elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX
- lapply (cpmhe_abst … HTUX) -HTUX #HTUX
- elim (cnv_cpmhe_mono … HT … HTUX … HX0) -a -T #H #_
+ lapply (cpmuwe_abst … HTUX) -HTUX #HTUX
+ elim (cnv_cpmuwe_mono … HT … HTUX … HX0) -a -T #H #_
elim (cpes_fwd_abst_bi … H) -H #_ #HWX -n0 -m0 -p -q -UX -U0
/3 width=3 by cpes_cpes_trans/
- | lapply (cnv_cpmhe_trans … HT … HX0) -T #H
+ | lapply (cnv_cpmuwe_trans … HT … HX0) -T #H
elim (cnv_inv_bind … H) -H #HW #_ //
]
(* Note: no expected type *)
| #HnX0
@or_intror #H
elim (cnv_inv_appl_cpes … H) -H #m0 #q #W0 #U0 #_ #_ #_ #_ #HTU0
- lapply (cpmhe_abst … HTU0) -HTU0 #HTU0
- elim (cnv_cpmhe_mono … HT … HTU0 … HX0) -T #_ #H
- elim (theq_inv_pair1 … H) -W0 -U0 #W0 #U0 #H destruct
+ lapply (cpmuwe_abst … HTU0) -HTU0 #HTU0
+ elim (cnv_cpmuwe_mono … HT … HTU0 … HX0) -T #_ #H
+ elim (tweq_inv_abst_sn … H) -W0 -U0 #W0 #U0 #H destruct
/2 width=4 by/
]
(* Note: failed applicability *)
@or_intror #H
elim (cnv_inv_appl … H) -H #m0 #q #W0 #U0 #Hm0 #_ #_ #_ #HTU0
elim (lt_or_ge m0 n0) #H0 [| /3 width=3 by ex2_intro/ ] -Hm0 -Hge
- /4 width=6 by cpmhe_abst, ex_intro/
+ /4 width=6 by cpmuwe_abst, ex_intro/
]
]
]
(**************************************************************************)
include "basic_2/rt_computation/cprs_cprs.ma".
-include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv_aaa.ma".
include "basic_2/dynamic/nta.ma".
+++ /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 T1 ➡* [ break term 46 h, break term 46 n ] 𝐍 *⦃ break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PRedEvalStar $h $n $G $L $T1 $T2 }.
--- /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 T1 ➡*𝐍𝐖*[ break term 46 h, break term 46 n ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedEvalWStar $h $n $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ ⥲[ break term 46 h ] ð\9d\90\8dâ¦\83 break term 46 T â¦\84 )"
+notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ â\9e¡ð\9d\90\8dð\9d\90\96*[ break term 46 h ] break term 46 T )"
non associative with precedence 45
for @{ 'PRedITNormal $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 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/preditnormal_4.ma".
+include "static_2/syntax/tweq.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
+
+definition cnuw (h) (G) (L): predicate term ≝
+ λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → T1 ≅ T2.
+
+interpretation
+ "normality for t-unbound weak head context-sensitive parallel rt-transition (term)"
+ 'PRedITNormal h G L T = (cnuw h G L T).
+
+lemma cpm_inv_lref1_ctop (n) (h) (G):
+ ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 * [| #i ] #H
+[ elim (cpm_inv_zero1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpm_inv_lref1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+
+lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cpms_inv_lref1_ctop (n) (h) (G):
+ ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_gref1 (n) (h) (G) (L):
+ ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0.
+#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cnuw_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⋆s.
+#h #G #L #s1 #n #X #H
+lapply (cpms_inv_sort1 … H) -H #H destruct //
+qed.
+
+lemma cnuw_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ➡𝐍𝐖*[h] #i.
+#h #G #i #n #X #H
+elim (cpms_inv_lref1_ctop … H) -H #H #_ destruct //
+qed.
+
+lemma cnuw_zero_unit (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ➡𝐍𝐖*[h] #0.
+#h #G #L #I #n #X #H
+elim (cpms_inv_zero1_unit … H) -H #H #_ destruct //
+qed.
+
+lemma cnuw_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] §l.
+#h #G #L #l1 #n #X #H
+elim (cpms_inv_gref1 … H) -H #H #_ destruct //
+qed.
+
+(* Basic_inversion lemmas ***************************************************)
+
+lemma cnuw_inv_zero_pair (h) (I) (G) (L): ∀V. ⦃G,L.ⓑ{I}V⦄ ⊢ ➡𝐍𝐖*[h] #0 → ⊥.
+#h * #G #L #V #H
+elim (lifts_total V (𝐔❴1❵)) #W #HVW
+[ lapply (H 0 W ?) [ /3 width=3 by cpm_cpms, cpm_delta/ ]
+| lapply (H 1 W ?) [ /3 width=3 by cpm_cpms, cpm_ell/ ]
+] -H #HW
+lapply (tweq_inv_lref_sn … HW) -HW #H destruct
+/2 width=5 by lifts_inv_lref2_uni_lt/
+qed-.
+
+lemma cnuw_inv_cast (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓝV.T → ⊥.
+#h #G #L #V #T #H
+lapply (H 0 T ?) [ /3 width=1 by cpm_cpms, cpm_eps/ ] -H #H
+/2 width=3 by tweq_inv_cast_sn_XY_Y/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cnuw_fwd_appl (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T.
+#h #G #L #V #T1 #HT1 #n #T2 #HT12
+lapply (HT1 n (ⓐV.T2) ?) -HT1
+/2 width=3 by cpms_appl_dx, tweq_inv_appl_bi/
+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_computation/cnuw.ma".
+include "basic_2/rt_computation/cprs_tweq.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cnuw_inv_abbr_pos (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] +ⓓV.T → ⊥.
+#h #G #L #V #T1 #H
+elim (cprs_abbr_pos_twneq h G L V T1) #T2 #HT12 #HnT12
+/3 width=2 by/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cnuw_abbr_neg (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] -ⓓV.T.
+#h #G #L #V1 #T1 #n #X #H
+elim (cpms_inv_abbr_sn_dx … H) -H *
+[ #V2 #T2 #_ #_ #H destruct /1 width=1 by tweq_abbr_neg/
+| #X1 #_ #_ #H destruct
+]
+qed.
+
+lemma cnuw_abst (h) (p) (G) (L): ∀W,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓛ{p}W.T.
+#h #p #G #L #W1 #T1 #n #X #H
+elim (cpms_inv_abst_sn … H) -H #W2 #T2 #_ #_ #H destruct
+/1 width=1 by tweq_abst/
+qed.
+
+lemma cnuw_cpms_trans (h) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1 →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2.
+#h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23
+/4 width=5 by cpms_trans, tweq_canc_sn/
+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/lifts_tweq.ma".
+include "basic_2/rt_computation/cpms_drops.ma".
+include "basic_2/rt_computation/cnuw.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
+
+(* Properties with generic relocation ***************************************)
+
+lemma cnuw_lifts (h) (G): d_liftable1 … (cnuw h G).
+#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H
+elim (cpms_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K /2 width=6 by tweq_lifts_bi/
+qed-.
+
+(* Inversion lemmas with generic relocation *********************************)
+
+lemma cnuw_inv_lifts (h) (G): d_deliftable1 … (cnuw h G).
+#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
+elim (cpms_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L /2 width=6 by tweq_inv_lifts_bi/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cnuw_lref (h) (I) (G) (L):
+ ∀i. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i → ⦃G,L.ⓘ{I}⦄ ⊢ ➡𝐍𝐖*[h] #↑i.
+#h #I #G #L #i #Hi #n #X2 #H
+elim (cpms_inv_lref_sn … H) -H *
+[ #H #_ destruct //
+| #T2 #HT2 #HTX2
+ lapply (Hi … HT2) -Hi -HT2 #H
+ lapply (tweq_inv_lref_sn … H) -H #H destruct
+ lapply (lifts_inv_lref1_uni … HTX2) -HTX2 #H destruct //
+]
+qed.
+
+lemma cnuw_atom_drops (h) (b) (G) (L):
+ ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i.
+#h #b #G #L #i #Hi #n #X #H
+elim (cpms_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK
+lapply (drops_gen b … HLK) -HLK #HLK
+lapply (drops_mono … Hi … HLK) -L #H destruct
+qed.
+
+lemma cnuw_unit_drops (h) (I) (G) (L):
+ ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i.
+#h #I #G #L #K #i #HLK #n #X #H
+elim (cpms_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY
+lapply (drops_mono … HLK … HLY) -L #H destruct
+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/syntax/tweq_simple.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_computation/cnuw.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
+
+(* Advanced forward lemma with with simple terms ****************************)
+(*
+lemma cnuw_fwd_appl_simple (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → 𝐒⦃T⦄.
+#h #G #L #V #T #HT
+elim (simple_dec_ex T) [ // ] * #p #I #W #U #H destruct
+*)
+(* Advanced properties with simple terms ************************************)
+
+lemma cnuw_appl_simple (h) (G) (L):
+ ∀V,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T.
+#h #G #L #V1 #T1 #H1T1 #H2T1 #n #X #H
+elim (cpms_inv_appl_sn … H) -H *
+[ #V2 #T2 #_ #HT12 #H destruct -H1T1
+ /3 width=2 by tweq_appl/
+| #n1 #n2 #p #V2 #T2 #HT12 #_ #_ -n -n2
+ lapply (H2T1 … HT12) -H2T1 -n1 #H
+ lapply (tweq_simple_trans … H H1T1) -H -H1T1 #H
+ elim (simple_inv_bind … H)
+| #n1 #n2 #p #V2 #W2 #W #T2 #_ #_ #HT12 #_ #_ -n -n2 -V2 -W2
+ lapply (H2T1 … HT12) -H2T1 -n1 #H
+ lapply (tweq_simple_trans … H H1T1) -H -H1T1 #H
+ elim (simple_inv_bind … H)
+]
+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/cpr_tdeq.ma".
+include "basic_2/rt_computation/cnuw_simple.ma".
+include "basic_2/rt_computation/cnuw_drops.ma".
+include "basic_2/rt_computation/cnuw_cnuw.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
+
+(* Properties with context-free sort-irrelevant equivalence for terms *******)
+
+lemma cnuw_dec_tdeq (h) (G) (L):
+ ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1
+ | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
+#h #G #L #T1 elim T1 -T1 *
+[ #s /3 width=5 by cnuw_sort, or_introl/
+| #i elim (drops_F_uni L i)
+ [ /3 width=7 by cnuw_atom_drops, or_introl/
+ | * * [ #I | * #V ] #K #HLK
+ [ /3 width=8 by cnuw_unit_drops, or_introl/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ ]
+ ]
+| #l /3 width=5 by cnuw_gref, or_introl/
+| #p * [ cases p ] #V1 #T1 #_ #_
+ [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2
+ elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
+ [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
+ @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
+ /2 width=7 by tdeq_lifts_inv_pair_sn/
+ | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | /3 width=5 by cnuw_abbr_neg, or_introl/
+ | /3 width=5 by cnuw_abst, or_introl/
+ ]
+| * #V1 #T1 #_ #IH
+ [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
+ [ elim IH -IH
+ [ /3 width=6 by cnuw_appl_simple, or_introl/
+ | * #n #T2 #HT12 #HnT12
+ @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
+ elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
+ ]
+ | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+ @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ ]
+ | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
+ /2 width=4 by tdeq_inv_pair_xy_y/
+ ]
+]
+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/predevalstar_6.ma".
-include "basic_2/rt_transition/cnh.ma".
-include "basic_2/rt_computation/cpms.ma".
-
-(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************)
-
-definition cpmhe (h) (n) (G) (L): relation2 term term ≝
- λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
-
-interpretation "t-unbound evaluation for t-bound context-sensitive parallel rt-transition (term)"
- 'PRedEvalStar h n G L T1 T2 = (cpmhe h n G L T1 T2).
-
-definition R_cpmhe (h) (G) (L) (T): predicate nat ≝
- λn. ∃U. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃U⦄.
-
-(* Basic properties *********************************************************)
-
-lemma cpmhe_intro (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
-/2 width=1 by conj/ qed.
-
-(* Advanced properties ******************************************************)
-
-lemma cpmhe_sort (h) (n) (G) (L) (T):
- ∀s. ⦃G,L⦄ ⊢ T ➡*[n,h] ⋆s → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃⋆s⦄.
-/3 width=5 by cnh_sort, cpmhe_intro/ qed.
-
-lemma cpmhe_ctop (h) (n) (G) (T):
- ∀i. ⦃G,⋆⦄ ⊢ T ➡*[n,h] #i → ⦃G,⋆⦄ ⊢ T ➡*[h,n] 𝐍*⦃#i⦄.
-/3 width=5 by cnh_ctop, cpmhe_intro/ qed.
-
-lemma cpmhe_zero (h) (n) (G) (L) (T):
- ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[n,h] #0 → ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[h,n] 𝐍*⦃#0⦄.
-/3 width=6 by cnh_zero, cpmhe_intro/ qed.
-
-lemma cpmhe_gref (h) (n) (G) (L) (T):
- ∀l. ⦃G,L⦄ ⊢ T ➡*[n,h] §l → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃§l⦄.
-/3 width=5 by cnh_gref, cpmhe_intro/ qed.
-
-lemma cpmhe_abst (h) (n) (p) (G) (L) (T):
- ∀W,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃ⓛ{p}W.U⦄.
-/3 width=5 by cnh_abst, cpmhe_intro/ qed.
-
-lemma cpmhe_abbr_neg (h) (n) (G) (L) (T):
- ∀V,U. ⦃G,L⦄ ⊢ T ➡*[n,h] -ⓓV.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃-ⓓV.U⦄.
-/3 width=5 by cnh_abbr_neg, cpmhe_intro/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma cpmhe_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 * #HT12 #_ //
-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/cpm_cpx.ma".
-include "basic_2/rt_transition/cnh_tdeq.ma".
-include "basic_2/rt_computation/csx.ma".
-include "basic_2/rt_computation/cpmhe.ma".
-
-(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************)
-
-(* Properties with strong normalization for unbound rt-transition for terms *)
-
-lemma cpmhe_total_csx (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
-#h #G #L #T1 #H
-@(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnh_dec_tdeq h G L T1)
-[ -IHT1 #HT1 /3 width=4 by cpmhe_intro, ex1_2_intro/
-| * #n1 #T0 #HT10 #HnT10
- elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
- #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmhe_intro, ex1_2_intro/
-]
-qed-.
-
-lemma R_cpmhe_total_csx (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmhe h G L T1 n.
-#h #G #L #T1 #H
-elim (cpmhe_total_csx … H) -H #T2 #n #HT12
-/3 width=3 by ex_intro (* 2x *)/
-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/syntax/theq_theq.ma".
-include "basic_2/rt_transition/cnh_cnh.ma".
-include "basic_2/rt_computation/cpms.ma".
-
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Inversion lemmas with normal terms for head t-unbound rt-transition ******)
-
-lemma cpms_inv_cnh_sn (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → T1 ⩳ T2.
-#h #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 //
-#n1 #n2 #T1 #T0 #HT10 #_ #IH #HT1
-/4 width=9 by cnh_cpm_trans, theq_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 "basic_2/notation/relations/predevalwstar_6.ma".
+include "basic_2/rt_computation/cnuw.ma".
+
+(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************)
+
+definition cpmuwe (h) (n) (G) (L): relation2 term term ≝
+ λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2.
+
+interpretation "t-unbound whd evaluation for t-bound context-sensitive parallel rt-transition (term)"
+ 'PRedEvalWStar h n G L T1 T2 = (cpmuwe h n G L T1 T2).
+
+definition R_cpmuwe (h) (G) (L) (T): predicate nat ≝
+ λn. ∃U. ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] U.
+
+(* Basic properties *********************************************************)
+
+lemma cpmuwe_intro (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2 → ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
+/2 width=1 by conj/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma cpmuwe_sort (h) (n) (G) (L) (T):
+ ∀s. ⦃G,L⦄ ⊢ T ➡*[n,h] ⋆s → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] ⋆s.
+/3 width=5 by cnuw_sort, cpmuwe_intro/ qed.
+
+lemma cpmuwe_ctop (h) (n) (G) (T):
+ ∀i. ⦃G,⋆⦄ ⊢ T ➡*[n,h] #i → ⦃G,⋆⦄ ⊢ T ➡*𝐍𝐖*[h,n] #i.
+/3 width=5 by cnuw_ctop, cpmuwe_intro/ qed.
+
+lemma cpmuwe_zero_unit (h) (n) (G) (L) (T):
+ ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[n,h] #0 → ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*𝐍𝐖*[h,n] #0.
+/3 width=6 by cnuw_zero_unit, cpmuwe_intro/ qed.
+
+lemma cpmuwe_gref (h) (n) (G) (L) (T):
+ ∀l. ⦃G,L⦄ ⊢ T ➡*[n,h] §l → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] §l.
+/3 width=5 by cnuw_gref, cpmuwe_intro/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpmuwe_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 * #HT12 #_ //
+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_computation/cnuw_cnuw.ma".
+include "basic_2/rt_computation/cpmuwe.ma".
+
+(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpmuwe_abbr_neg (h) (n) (G) (L) (T):
+ ∀V,U. ⦃G,L⦄ ⊢ T ➡*[n,h] -ⓓV.U → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
+/3 width=5 by cnuw_abbr_neg, cpmuwe_intro/ qed.
+
+lemma cpmuwe_abst (h) (n) (p) (G) (L) (T):
+ ∀W,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] ⓛ{p}W.U.
+/3 width=5 by cnuw_abst, cpmuwe_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/cpm_cpx.ma".
+include "basic_2/rt_computation/csx.ma".
+include "basic_2/rt_computation/cnuw_tdeq.ma".
+include "basic_2/rt_computation/cpmuwe.ma".
+
+(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************)
+
+(* Properties with strong normalization for unbound rt-transition for terms *)
+
+lemma cpmuwe_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
+#h #G #L #T1 #H
+@(csx_ind … H) -T1 #T1 #_ #IHT1
+elim (cnuw_dec_tdeq h G L T1)
+[ -IHT1 #HT1 /3 width=4 by cpmuwe_intro, ex1_2_intro/
+| * #n1 #T0 #HT10 #HnT10
+ elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
+ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmuwe_intro, ex1_2_intro/
+]
+qed-.
+
+lemma R_cpmuwe_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmuwe h G L T1 n.
+#h #G #L #T1 #H
+elim (cpmuwe_total_csx … H) -H #T2 #n #HT12
+/3 width=3 by ex_intro (* 2x *)/
+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/syntax/tweq_tweq.ma".
+include "static_2/relocation/lifts_tweq.ma".
+include "basic_2/rt_transition/cpr_drops_basic.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************)
+
+(* Properties with sort-irrelevant whd equivalence on terms *****************)
+
+lemma cprs_abbr_pos_twneq (h) (G) (L) (V) (T1):
+ ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[h] T2 & (+ⓓV.T1 ≅ T2 → ⊥).
+#h #G #L #V #U1
+elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
+elim (tweq_dec U1 U2) [ #HpU12 | -HTU2 #HnU12 ]
+[ @(ex2_intro … T2) (**) (* full auto not tried *)
+ [ /3 width=6 by cpms_zeta, cpms_step_sn, cpm_bind/
+ | /4 width=6 by tweq_inv_abbr_pos_sn_X_lifts_Y_Y, tweq_canc_sn, tweq_abbr_pos/
+ ]
+| /4 width=3 by cpm_cpms, cpm_bind, tweq_inv_abbr_pos_bi, 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 "static_2/syntax/theq_tdeq.ma".
-include "basic_2/rt_computation/cpxs_lsubr.ma".
-include "basic_2/rt_computation/cpxs_cnx.ma".
-include "basic_2/rt_computation/lpxs_cpxs.ma".
-
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Forward lemmas with head equivalence for terms ***************************)
-
-lemma cpxs_fwd_sort: ∀h,G,L,X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2.
-#h #G #L #X2 #s1 #H
-elim (cpxs_inv_sort1 … H) -H #s2 #H destruct //
-qed-.
-
-(* Note: probably this is an inversion lemma *)
-(* Basic_2A1: was: cpxs_fwd_delta *)
-lemma cpxs_fwd_delta_drops: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
- ∀V2. ⬆*[↑i] V1 ≘ V2 →
- ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 →
- ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H
-elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
-* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
-lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
-/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/
-qed-.
-
-(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
- ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2.
-#h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
- elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
- lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
- /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
-| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
- elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
-]
-qed-.
-
-lemma cpxs_fwd_theta: ∀h,p,G,L,V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 →
- ∀V2. ⬆*[1] V1 ≘ V2 →
- ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2.
-#h #p #G #L #V1 #V #T #X2 #H #V2 #HV12
-elim (cpxs_inv_appl1 … H) -H *
-[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
-| #q #W #T0 #HT0 #HU
- elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
- [ #V3 #T3 #_ #_ #H destruct
- | #X #HT2 #H #H0 destruct
- elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
- @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
- /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/
- ]
-| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
- @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
- elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
- [ #V5 #T5 #HV5 #HT5 #H destruct
- /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
- | #X #HT1 #H #H0 destruct
- elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
- @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
- ]
-]
-qed-.
-
-lemma cpxs_fwd_cast: ∀h,G,L,W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 →
- ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2.
-#h #G #L #W #T #X2 #H
-elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/
-qed-.
-
-lemma cpxs_fwd_cnx: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
- ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
-/3 width=5 by cpxs_inv_cnx1, tdeq_theq/ 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/syntax/theq_simple_vector.ma".
-include "static_2/relocation/lifts_vector.ma".
-include "basic_2/rt_computation/cpxs_theq.ma".
-
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Vector form of forward lemmas with head equivalence for terms ************)
-
-lemma cpxs_fwd_sort_vector: ∀h,G,L,s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
-#h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/
-#V #Vs #IHVs #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair/
-| #p #W1 #T1 #HT1 #HU
- lapply (IHVs … HT1) -IHVs -HT1 #HT1
- elim (theq_inv_applv_bind_simple … HT1) //
-| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- lapply (IHVs … HT1) -IHVs -HT1 #HT1
- elim (theq_inv_applv_bind_simple … HT1) //
-]
-qed-.
-
-(* Basic_2A1: was: cpxs_fwd_delta_vector *)
-lemma cpxs_fwd_delta_drops_vector: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
- ∀V2. ⬆*[↑i] V1 ≘ V2 →
- ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
- ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
-elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
-#V #Vs #IHVs #X2 #H -K -V1
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
-| #q #W0 #T0 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (theq_inv_applv_bind_simple … HT0) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
- ]
-| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (theq_inv_applv_bind_simple … HT0) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,p,G,L,Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
- ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
-#h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
-| #q #W1 #T1 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (theq_inv_applv_bind_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
- ]
-| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (theq_inv_applv_bind_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector: ∀h,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
- ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
- ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
-#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
-#V1b #V2b #V1a #V2a #HV12a #HV12b #p
-generalize in match HV12a; -HV12a
-generalize in match V2a; -V2a
-generalize in match V1a; -V1a
-elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
-#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
-| #q #W0 #T0 #HT0 #HU
- elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
- [ -HV12a -HV12b -HU
- elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1b (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
- [ -HV12a #V1 #T1 #_ #_ #H destruct
- | -V1b #X #HT1 #H #H0 destruct
- elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
- @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0))
- /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/
- ]
- ]
-| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
- elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0
- [ -HV12a -HV10a -HV0a -HU
- elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1b -V1b (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
- [ #V1 #T1 #HV1 #HT1 #H destruct
- lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
- @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
- | #X #HT1 #H #H0 destruct
- elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
- @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
- @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
- ]
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,G,L,Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
- ∨∨ ⒶVs. ⓝW. T ⩳ X2
- | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2
- | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
-#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
-#V #Vs #IHVs #W #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/
-| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (theq_inv_applv_bind_simple … HT0) //
- | @or3_intro1 -W (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
- | @or3_intro2 -T (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
- ]
-| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (theq_inv_applv_bind_simple … HT0) //
- | @or3_intro1 -W (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
- | @or3_intro2 -T (**) (* explicit constructor *)
- @(cpxs_trans … HU) -X2
- @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
- ]
-]
-qed-.
-
-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
- ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
-#h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
-#V #Vs #IHVs #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair/
-| #p #W0 #T0 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (theq_inv_applv_bind_simple … HT0) //
-| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (theq_inv_applv_bind_simple … HT0) //
-]
-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/syntax/toeq_tdeq.ma".
+include "basic_2/rt_computation/cpxs_lsubr.ma".
+include "basic_2/rt_computation/cpxs_cnx.ma".
+include "basic_2/rt_computation/lpxs_cpxs.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Forward lemmas with sort-irrelevant outer equivalence for terms **********)
+
+lemma cpxs_fwd_sort (h) (G) (L):
+ ∀X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2.
+#h #G #L #X2 #s1 #H
+elim (cpxs_inv_sort1 … H) -H #s2 #H destruct //
+qed-.
+
+(* Note: probably this is an inversion lemma *)
+(* Basic_2A1: was: cpxs_fwd_delta *)
+lemma cpxs_fwd_delta_drops (h) (I) (G) (L) (K):
+ ∀V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+ ∀V2. ⬆*[↑i] V1 ≘ V2 →
+ ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 →
+ ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2.
+#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H
+elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
+* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
+lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
+/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/
+qed-.
+
+(* Basic_1: was just: pr3_iso_beta *)
+lemma cpxs_fwd_beta (h) (p) (G) (L):
+ ∀V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
+ ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2.
+#h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+ elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
+ lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
+ /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
+| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
+ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+]
+qed-.
+
+lemma cpxs_fwd_theta (h) (p) (G) (L):
+ ∀V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 →
+ ∀V2. ⬆*[1] V1 ≘ V2 →
+ ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2.
+#h #p #G #L #V1 #V #T #X2 #H #V2 #HV12
+elim (cpxs_inv_appl1 … H) -H *
+[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
+| #q #W #T0 #HT0 #HU
+ elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+ [ #V3 #T3 #_ #_ #H destruct
+ | #X #HT2 #H #H0 destruct
+ elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
+ @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
+ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/
+ ]
+| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
+ @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
+ elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+ [ #V5 #T5 #HV5 #HT5 #H destruct
+ /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
+ | #X #HT1 #H #H0 destruct
+ elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
+ lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
+ ]
+]
+qed-.
+
+lemma cpxs_fwd_cast (h) (G) (L):
+ ∀W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 →
+ ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2.
+#h #G #L #W #T #X2 #H
+elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/
+qed-.
+
+lemma cpxs_fwd_cnx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
+ ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
+/3 width=5 by cpxs_inv_cnx1, tdeq_toeq/ 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/syntax/toeq_simple_vector.ma".
+include "static_2/relocation/lifts_vector.ma".
+include "basic_2/rt_computation/cpxs_toeq.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Vector form of forward lemmas with outer equivalence for terms ***********)
+
+lemma cpxs_fwd_sort_vector (h) (G) (L):
+ ∀s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
+#h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/
+#V #Vs #IHVs #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair/
+| #p #W1 #T1 #HT1 #HU
+ lapply (IHVs … HT1) -IHVs -HT1 #HT1
+ elim (toeq_inv_applv_bind_simple … HT1) //
+| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ lapply (IHVs … HT1) -IHVs -HT1 #HT1
+ elim (toeq_inv_applv_bind_simple … HT1) //
+]
+qed-.
+
+(* Basic_2A1: was: cpxs_fwd_delta_vector *)
+lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
+ ∀V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+ ∀V2. ⬆*[↑i] V1 ≘ V2 →
+ ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
+ ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
+#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
+elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
+#V #Vs #IHVs #X2 #H -K -V1
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (toeq_inv_applv_bind_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
+ ]
+| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (toeq_inv_applv_bind_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_beta *)
+lemma cpxs_fwd_beta_vector (h) (p) (G) (L):
+ ∀Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
+ ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
+#h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#V0 #Vs #IHVs #V #W #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
+| #q #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (toeq_inv_applv_bind_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
+ ]
+| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (toeq_inv_applv_bind_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_abbr *)
+lemma cpxs_fwd_theta_vector (h) (G) (L):
+ ∀V1b,V2b. ⬆*[1] V1b ≘ V2b →
+ ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
+ ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
+#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
+#V1b #V2b #V1a #V2a #HV12a #HV12b #p
+generalize in match HV12a; -HV12a
+generalize in match V2a; -V2a
+generalize in match V1a; -V1a
+elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
+#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+ elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
+ [ -HV12a -HV12b -HU
+ elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1b (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+ [ -HV12a #V1 #T1 #_ #_ #H destruct
+ | -V1b #X #HT1 #H #H0 destruct
+ elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+ @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0))
+ /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/
+ ]
+ ]
+| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
+ elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0
+ [ -HV12a -HV10a -HV0a -HU
+ elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1b -V1b (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+ [ #V1 #T1 #HV1 #HT1 #H destruct
+ lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
+ @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
+ | #X #HT1 #H #H0 destruct
+ elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
+ lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+ @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
+ @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
+ ]
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_cast *)
+lemma cpxs_fwd_cast_vector (h) (G) (L):
+ ∀Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
+ ∨∨ ⒶVs. ⓝW. T ⩳ X2
+ | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2
+ | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
+#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+#V #Vs #IHVs #W #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/
+| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (toeq_inv_applv_bind_simple … HT0) //
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+ | @or3_intro2 -T (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+ ]
+| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (toeq_inv_applv_bind_simple … HT0) //
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+ | @or3_intro2 -T (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -X2
+ @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+ ]
+]
+qed-.
+
+(* Basic_1: was just: nf2_iso_appls_lref *)
+lemma cpxs_fwd_cnx_vector (h) (G) (L):
+ ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
+ ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
+#h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#V #Vs #IHVs #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair/
+| #p #W0 #T0 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (toeq_inv_applv_bind_simple … HT0) //
+| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (toeq_inv_applv_bind_simple … HT0) //
+]
+qed-.
(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
-include "basic_2/rt_computation/cpxs_theq_vector.ma".
-include "basic_2/rt_computation/csx_simple_theq.ma".
+include "basic_2/rt_computation/cpxs_toeq_vector.ma".
+include "basic_2/rt_computation/csx_simple_toeq.ma".
include "basic_2/rt_computation/csx_cnx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_vector.ma".
(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
- ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄.
+lemma csx_applv_cnx (h) (G) (L):
+ ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
+ ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄.
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
- @csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs
+ @csx_appl_simple_toeq /2 width=1 by applv_simple/ -IHV -HV -HVs
#X #H #H0
lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
elim (H0) -H0 //
(* Advanced properties ******************************************************)
(* Note: strong normalization does not depend on this any more *)
-lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
+lemma csx_applv_sort (h) (G) (L):
+ ∀s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
/3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cpxs_theq_vector.ma".
-include "basic_2/rt_computation/csx_simple_theq.ma".
+include "basic_2/rt_computation/cpxs_toeq_vector.ma".
+include "basic_2/rt_computation/csx_simple_toeq.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
include "basic_2/rt_computation/csx_lpx.ma".
include "basic_2/rt_computation/csx_vector.ma".
#V0 #Vs #IHV #V #W #T #H1T
lapply (csx_fwd_pair_sn … H1T) #HV0
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
+@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
#X #H #H0
elim (cpxs_fwd_beta_vector … H) -H #H
[ -H1T elim H0 -H0 //
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
- @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
+ @csx_appl_simple_toeq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
#X #H #H0
elim (cpxs_fwd_delta_drops_vector … HLK … HV12 … H) -HLK -HV12 -H #H
[ -H1T elim H0 -H0 //
lapply (csx_appl_theta … H … HW12) -H -HW12 #H
lapply (csx_fwd_pair_sn … H) #HW1
lapply (csx_fwd_flat_dx … H) #H1
-@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
+@csx_appl_simple_toeq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
elim (cpxs_fwd_theta_vector … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
[ -H #H elim H2 -H2 //
| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
lapply (csx_fwd_pair_sn … H1U) #HV
lapply (csx_fwd_flat_dx … H1U) #H2U
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T
+@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T
#X #H #H0
elim (cpxs_fwd_cast_vector … H) -H #H
[ -H1U -H1T elim H0 -H0 //
+++ /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/syntax/theq_simple.ma".
-include "static_2/syntax/theq_theq.ma".
-include "basic_2/rt_transition/cpx_simple.ma".
-include "basic_2/rt_computation/cpxs.ma".
-include "basic_2/rt_computation/csx_csx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-
-(* Properties with head equivalence for terms *******************************)
-
-(* Basic_1: was just: sn3_appl_appl *)
-(* Basic_2A1: was: csx_appl_simple_tsts *)
-lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
- (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
- 𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
-#h #G #L #V #H @(csx_ind … H) -V
-#V #_ #IHV #T1 #H @(csx_ind … H) -T1
-#T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (tdneq_inv_pair … H) -H
-[ #H elim H -H //
-| -IHT1 #HV0
- @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
- @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-| -IHV -H1T1 #H1T10
- @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
- elim (theq_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/
- | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_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 "static_2/syntax/toeq_simple.ma".
+include "static_2/syntax/toeq_toeq.ma".
+include "basic_2/rt_transition/cpx_simple.ma".
+include "basic_2/rt_computation/cpxs.ma".
+include "basic_2/rt_computation/csx_csx.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+
+(* Properties with outer equivalence for terms ******************************)
+
+(* Basic_1: was just: sn3_appl_appl *)
+(* Basic_2A1: was: csx_appl_simple_tsts *)
+lemma csx_appl_simple_toeq (h) (G) (L):
+ ∀V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+ (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
+ 𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
+#h #G #L #V #H @(csx_ind … H) -V
+#V #_ #IHV #T1 #H @(csx_ind … H) -T1
+#T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1_simple … HL) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (tdneq_inv_pair … H) -H
+[ #H elim H -H //
+| -IHT1 #HV0
+ @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
+ @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+| -IHV -H1T1 #H1T10
+ @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
+ elim (toeq_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, toeq_canc_sn, simple_toeq_repl_dx/
+ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_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/notation/relations/preditnormal_4.ma".
-include "static_2/syntax/theq.ma".
-include "basic_2/rt_transition/cpm.ma".
-
-(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
-
-definition cnh (h) (G) (L): predicate term ≝
- λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ⩳ T2.
-
-interpretation
- "normality for head t-unbound context-sensitive parallel rt-transition (term)"
- 'PRedITNormal h G L T = (cnh h G L T).
-
-(* Basic properties *********************************************************)
-
-lemma cnh_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄.
-#h #G #L #s1 #n #X #H
-elim (cpm_inv_sort1 … H) -H #H #_ destruct //
-qed.
-
-lemma cnh_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #G * [| #i ] #n #X #H
-[ elim (cpm_inv_zero1 … H) -H *
- [ #H #_ destruct //
- | #Y #X1 #X2 #_ #_ #H destruct
- | #m #Y #X1 #X2 #_ #_ #H destruct
- ]
-| elim (cpm_inv_lref1 … H) -H *
- [ #H #_ destruct //
- | #Z #Y #X0 #_ #_ #H destruct
- ]
-]
-qed.
-
-lemma cnh_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄.
-#h #G #L #I #n #X #H
-elim (cpm_inv_zero1 … H) -H *
-[ #H #_ destruct //
-| #Y #X1 #X2 #_ #_ #H destruct
-| #m #Y #X1 #X2 #_ #_ #H destruct
-]
-qed.
-
-lemma cnh_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄.
-#h #G #L #l1 #n #X #H
-elim (cpm_inv_gref1 … H) -H #H #_ destruct //
-qed.
-
-lemma cnh_abst (h) (p) (G) (L): ∀W,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄.
-#h #p #G #L #W1 #T1 #n #X #H
-elim (cpm_inv_abst1 … H) -H #W2 #T2 #_ #_ #H destruct
-/1 width=1 by theq_pair/
-qed.
-
-lemma cnh_abbr_neg (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄.
-#h #G #L #V1 #T1 #n #X #H
-elim (cpm_inv_abbr1 … H) -H *
-[ #W2 #T2 #_ #_ #H destruct /1 width=1 by theq_pair/
-| #X1 #_ #_ #H destruct
-]
-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/cpm.ma".
-include "basic_2/rt_transition/cnh.ma".
-
-(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
-
-(* Advanced properties ******************************************************)
-
-axiom cnh_cpm_trans (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
-(*
-#h #n #G #L #T1 #T2 #HT1 #n #T2 #HT12 #k #X #HX
-*)
+++ /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/lifts_theq.ma".
-include "basic_2/rt_transition/cpm_drops.ma".
-include "basic_2/rt_transition/cnh.ma".
-
-(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cnh_atom_drops (h) (b) (G) (L):
- ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #b #G #L #i #Hi #n #X #H
-elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK
-lapply (drops_gen b … HLK) -HLK #HLK
-lapply (drops_mono … Hi … HLK) -L #H destruct
-qed.
-
-lemma cnh_unit_drops (h) (I) (G) (L):
- ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #I #G #L #K #i #HLK #n #X #H
-elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY
-lapply (drops_mono … HLK … HLY) -L #H destruct
-qed.
-
-(* Properties with generic relocation ***************************************)
-
-lemma cnh_lifts (h) (G): d_liftable1 … (cnh h G).
-#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H
-elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
-lapply (HT … HT0) -G -K /2 width=6 by theq_lifts_bi/
-qed-.
-
-(* Inversion lemmas with generic relocation *********************************)
-
-lemma cnh_inv_lifts (h) (G): d_deliftable1 … (cnh h G).
-#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
-elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
-lapply (HU … HU0) -G -L /2 width=6 by theq_inv_lifts_bi/
-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/lifts.ma".
-include "basic_2/rt_transition/cnh.ma".
-
-(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
-
-(* Advanced properties with uniform relocation for terms ********************)
-
-lemma cnh_lref (h) (I) (G) (L):
- ∀i. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄ → ⦃G,L.ⓘ{I}⦄ ⊢ ⥲[h] 𝐍⦃#↑i⦄.
-#h #I #G #L #i #Hi #n #X #H
-elim (cpm_inv_lref1 … H) -H *
-[ #H #_ destruct //
-| #J #K #V #HV #HVX #H destruct
- lapply (Hi … HV) -Hi -HV #HV
- lapply (theq_inv_lref1 … HV) -HV #H destruct
- lapply (lifts_inv_lref1_uni … HVX) -HVX #H destruct //
-]
-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/cpm_simple.ma".
-include "basic_2/rt_transition/cnh.ma".
-
-(* NORMAL TERMS HEAD FOR T-UNUNBOUND RT-TRANSITION **************************)
-
-(* Advanced properties with simple terms ************************************)
-
-lemma cnh_appl_simple (h) (G) (L): ∀V,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄.
-#h #G #L #V1 #T1 #HT1 #n #X #H
-elim (cpm_inv_appl1_simple … H HT1) -H -HT1 #V2 #T2 #_ #_ #H destruct
-/1 width=1 by theq_pair/
-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/cpr_tdeq.ma".
-include "basic_2/rt_transition/cnh_simple.ma".
-include "basic_2/rt_transition/cnh_drops.ma".
-
-(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
-
-(* Properties with context-free sort-irrelevant equivalence for terms *******)
-
-lemma cnh_dec_tdeq (h) (G) (L):
- ∀T1. ∨∨ ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄
- | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
-#h #G #L * *
-[ #s /3 width=5 by cnh_sort, or_introl/
-| #i elim (drops_F_uni L i)
- [ /3 width=7 by cnh_atom_drops, or_introl/
- | * * [ #I | * #V ] #K #HLK
- [ /3 width=8 by cnh_unit_drops, or_introl/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- ]
- ]
-| #l /3 width=5 by cnh_gref, or_introl/
-| #p * [ cases p ] #V1 #T1
- [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2
- elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
- [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
- @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
- /2 width=7 by tdeq_lifts_inv_pair_sn/
- | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- | /3 width=5 by cnh_abbr_neg, or_introl/
- | /3 width=5 by cnh_abst, or_introl/
- ]
-| * #V1 #T1
- [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
- [ /3 width=5 by cnh_appl_simple, or_introl/
- | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
- @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- ]
- | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
- /2 width=4 by tdeq_inv_pair_xy_y/
- ]
-]
-qed-.
(* Properties with context-free sort-irrelevant equivalence *****************)
-lemma cpr_abbr_pos (h) (G) (L) (V) (T1):
- ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛ T2 → ⊥).
+lemma cpr_abbr_pos_tdneq (h) (G) (L) (V) (T1):
+ ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛ T2 → ⊥).
#h #G #L #V #U1
elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
elim (tdeq_dec U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ]
]
[ { "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_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_cpmhe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "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_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
}
]
}
[ [ "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" * ]
[ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
- [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ]
+ [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_tweq" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
- [ [ "t-unbound head evaluation for terms" ] "cpmhe ( ⦃?,?⦄ ⊢ ? ⬌*[?] 𝐍*⦃?⦄ )" "cpmhe_csx" * ]
+ [ [ "t-unbound whd evaluation for terms" ] "cpmuwe ( ⦃?,?⦄ ⊢ ? ⬌*𝐍𝐖*[?,?] ? )" "cpmuwe_csx" + "cpmuwe_cpmuwe" * ]
+ [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_tdeq" + "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ]
+
[ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
- [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnh" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
[ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_toeq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
[ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_rdeq" + "lpxs_fdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
- [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_toeq" + "cpxs_toeq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
]
class "cyan"
[ { "rt-transition" * } {
- [ { "t-unbound context-sensitive parallel rt-transition" * } {
- [ [ "head normal form for terms" ] "cnh ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnh_tdeq" + "cnh_lifts" + "cnh_drops" + "cnh_cnr" + "cnh_cnr_simple" + "cnh_cnh" * ]
- }
- ]
[ { "context-sensitive parallel r-transition" * } {
[ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ]
[ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
[ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
}
]
- [ { "tail sort-irrelevant equivalence" * } {
- [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ]
- }
- ]
*)
+++ /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( T1 ≅ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'ApproxEq $T1 $T2 }.
--- /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( T1 ≅ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'ApproxEq $T1 $T2 }.
+++ /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/syntax/theq.ma".
-include "static_2/relocation/lifts_lifts.ma".
-
-(* GENERIC RELOCATION FOR TERMS *********************************************)
-
-(* Properties with tail sort-irrelevant head equivalence for terms **********)
-
-lemma theq_lifts_bi: liftable2_bi theq.
-#T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X1 #H1 #X2 #H2
- >(lifts_inv_sort1 … H1) -H1 >(lifts_inv_sort1 … H2) -H2
- /1 width=1 by theq_sort/
-| #i #f #X1 #H1 #X2 #H2
- elim (lifts_inv_lref1 … H1) -H1 #j1 #Hj1 #H destruct
- elim (lifts_inv_lref1 … H2) -H2 #j2 #Hj2 #H destruct
- <(at_mono … Hj2 … Hj1) -i -f -j2
- /1 width=1 by theq_lref/
-| #l #f #X1 #H1 #X2 #H2
- >(lifts_inv_gref1 … H1) -H1 >(lifts_inv_gref1 … H2) -H2
- /1 width=1 by theq_gref/
-| #p #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
- elim (lifts_inv_bind1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
- elim (lifts_inv_bind1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
- /1 width=1 by theq_pair/
-| #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
- elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
- elim (lifts_inv_flat1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
- /1 width=1 by theq_pair/
-]
-qed-.
-
-(* Inversion lemmas with tail sort-irrelevant head equivalence for terms ****)
-
-lemma theq_inv_lifts_bi: deliftable2_bi theq.
-#U1 #U2 #H elim H -U1 -U2 [||| * ]
-[ #s1 #s2 #f #X1 #H1 #X2 #H2
- >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
- /1 width=1 by theq_sort/
-| #j #f #X1 #H1 #X2 #H2
- elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
- elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
- <(at_inj … Hj2 … Hj1) -j -f -i1
- /1 width=1 by theq_lref/
-| #l #f #X1 #H1 #X2 #H2
- >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
- /1 width=1 by theq_gref/
-| #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
- elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
- elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
- /1 width=1 by theq_pair/
-| #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
- elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
- elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
- /1 width=1 by theq_pair/
-]
-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/syntax/toeq.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with sort-irrelevant outer equivalence for terms **************)
+
+lemma toeq_lifts_sn: liftable2_sn toeq.
+#T1 #T2 #H elim H -T1 -T2 [||| * ]
+[ #s1 #s2 #f #X #H
+ >(lifts_inv_sort1 … H) -H
+ /2 width=3 by toeq_sort, ex2_intro/
+| #i #f #X #H
+ elim (lifts_inv_lref1 … H) -H #j #Hj #H destruct
+ /3 width=3 by toeq_lref, lifts_lref, ex2_intro/
+| #l #f #X #H
+ >(lifts_inv_gref1 … H) -H
+ /2 width=3 by toeq_gref, ex2_intro/
+| #p #I #V1 #V2 #T1 #T2 #f #X #H
+ elim (lifts_inv_bind1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
+ elim (lifts_total V2 f) #W2 #HVW2
+ elim (lifts_total T2 (⫯f)) #U2 #HTU2
+ /3 width=3 by toeq_pair, lifts_bind, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #f #X #H
+ elim (lifts_inv_flat1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
+ elim (lifts_total V2 f) #W2 #HVW2
+ elim (lifts_total T2 f) #U2 #HTU2
+ /3 width=3 by toeq_pair, lifts_flat, ex2_intro/
+]
+qed-.
+
+lemma toeq_lifts_dx: liftable2_dx toeq.
+/3 width=3 by toeq_lifts_sn, liftable2_sn_dx, toeq_sym/ qed-.
+
+lemma toeq_lifts_bi: liftable2_bi toeq.
+/3 width=6 by toeq_lifts_sn, liftable2_sn_bi/ qed-.
+
+(* Inversion lemmas with sort-irrelevant outer equivalence for terms ********)
+
+lemma toeq_inv_lifts_bi: deliftable2_bi toeq.
+#U1 #U2 #H elim H -U1 -U2 [||| * ]
+[ #s1 #s2 #f #X1 #H1 #X2 #H2
+ >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
+ /1 width=1 by toeq_sort/
+| #j #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
+ elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
+ <(at_inj … Hj2 … Hj1) -j -f -i1
+ /1 width=1 by toeq_lref/
+| #l #f #X1 #H1 #X2 #H2
+ >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
+ /1 width=1 by toeq_gref/
+| #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
+ elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
+ /1 width=1 by toeq_pair/
+| #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
+ elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
+ /1 width=1 by toeq_pair/
+]
+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/syntax/tweq.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with sort-irrelevant whd equivalence for terms ****************)
+
+lemma tweq_lifts_sn: liftable2_sn tweq.
+#T1 #T2 #H elim H -T1 -T2
+[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H
+ /3 width=3 by lifts_sort, tweq_sort, ex2_intro/
+| #i #f #X #H elim (lifts_inv_lref1 … H) -H
+ /3 width=3 by lifts_lref, tweq_lref, ex2_intro/
+| #l #f #X #H >(lifts_inv_gref1 … H) -H
+ /2 width=3 by lifts_gref, tweq_gref, ex2_intro/
+| #p #V1 #V2 #T1 #T2 #_ #IHT #f #X #H
+ elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (lifts_total V2 f) #W2 #HVW2
+ elim (true_or_false p) #H destruct
+ [ elim (IHT … HTU1) -T1 [| // ] #U2 #HTU2 #HU12
+ | elim (lifts_total T2 (⫯f)) #U2 #HTU2
+ ]
+ /3 width=4 by tweq_abbr_pos, lifts_bind, ex2_intro/
+| #p #V1 #V2 #T1 #T2 #f #X #H
+ elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (lifts_total V2 f) #W2 #HVW2
+ elim (lifts_total T2 (⫯f)) #U2 #HTU2
+ /3 width=3 by lifts_bind, ex2_intro/
+| #V1 #V2 #T1 #T2 #_ #IHT #f #X #H
+ elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (lifts_total V2 f) #W2 #HVW2
+ elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12
+ /3 width=4 by lifts_flat, tweq_appl, ex2_intro/
+| #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H
+ elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV … HVW1) -V1 #W2 #HVW2 #HW12
+ elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12
+ /3 width=5 by lifts_flat, tweq_cast, ex2_intro/
+]
+qed-.
+
+lemma tweq_lifts_dx: liftable2_dx tweq.
+/3 width=3 by tweq_lifts_sn, liftable2_sn_dx, tweq_sym/ qed-.
+
+lemma tweq_lifts_bi: liftable2_bi tweq.
+/3 width=6 by tweq_lifts_sn, liftable2_sn_bi/ qed-.
+
+(* Inversion lemmas with sort-irrelevant whd equivalence for terms **********)
+
+lemma tweq_inv_lifts_bi: deliftable2_bi tweq.
+#U1 #U2 #H elim H -U1 -U2
+[ #s1 #s2 #f #X1 #H1 #X2 #H2
+ >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
+ /1 width=1 by tweq_sort/
+| #j #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
+ elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
+ <(at_inj … Hj2 … Hj1) -j -f -i1
+ /1 width=1 by tweq_lref/
+| #l #f #X1 #H1 #X2 #H2
+ >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
+ /1 width=1 by tweq_gref/
+| #p #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1
+ elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2
+ elim (true_or_false p) #H destruct
+ [ /3 width=3 by tweq_abbr_pos/
+ | /1 width=1 by tweq_abbr_neg/
+ ]
+| #p #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
+ elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
+ /1 width=1 by tweq_abst/
+| #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1
+ elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2
+ /3 width=3 by tweq_appl/
+| #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #HVW2 #HTU2 #H destruct
+ /3 width=3 by tweq_cast/
+]
+qed-.
+
+lemma tweq_inv_abbr_pos_sn_X_lifts_Y_Y (T) (f:rtmap):
+ ∀V,U. +ⓓV.U ≅ T → ⬆*[f]T ≘ U → ⊥.
+@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
+elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
+elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct
+/2 width=7 by/
+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/notation/relations/topiso_2.ma".
-include "static_2/syntax/term.ma".
-
-(* HEAD EQUIVALENCE FOR TERMS ***********************************************)
-
-(* Basic_2A1: includes: tsts_atom tsts_pair *)
-inductive theq: relation term ≝
-| theq_sort: ∀s1,s2. theq (⋆s1) (⋆s2)
-| theq_lref: ∀i. theq (#i) (#i)
-| theq_gref: ∀l. theq (§l) (§l)
-| theq_pair: ∀I,V1,V2,T1,T2. theq (②{I}V1.T1) (②{I}V2.T2)
-.
-
-interpretation "head equivalence (term)" 'TopIso T1 T2 = (theq T1 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact theq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
- ∃s2. Y = ⋆s2.
-#X #Y * -X -Y
-[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
-| #i #s #H destruct
-| #l #s #H destruct
-| #I #V1 #V2 #T1 #T2 #s #H destruct
-]
-qed-.
-
-(* Basic_1: was just: iso_gen_sort *)
-lemma theq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
- ∃s2. Y = ⋆s2.
-/2 width=4 by theq_inv_sort1_aux/ qed-.
-
-fact theq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
-#X #Y * -X -Y //
-[ #s1 #s2 #j #H destruct
-| #I #V1 #V2 #T1 #T2 #j #H destruct
-]
-qed-.
-
-(* Basic_1: was: iso_gen_lref *)
-lemma theq_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
-/2 width=5 by theq_inv_lref1_aux/ qed-.
-
-fact theq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l.
-#X #Y * -X -Y //
-[ #s1 #s2 #k #H destruct
-| #I #V1 #V2 #T1 #T2 #k #H destruct
-]
-qed-.
-
-lemma theq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
-/2 width=5 by theq_inv_gref1_aux/ qed-.
-
-fact theq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 →
- ∀J,W1,U1. T1 = ②{J}W1.U1 →
- ∃∃W2,U2. T2 = ②{J}W2.U2.
-#T1 #T2 * -T1 -T2
-[ #s1 #s2 #J #W1 #U1 #H destruct
-| #i #J #W1 #U1 #H destruct
-| #l #J #W1 #U1 #H destruct
-| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-(* Basic_1: was: iso_gen_head *)
-(* Basic_2A1: was: tsts_inv_pair1 *)
-lemma theq_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 →
- ∃∃W2,U2. T2 = ②{J}W2. U2.
-/2 width=7 by theq_inv_pair1_aux/ qed-.
-
-fact theq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
- ∀J,W2,U2. T2 = ②{J}W2.U2 →
- ∃∃W1,U1. T1 = ②{J}W1.U1.
-#T1 #T2 * -T1 -T2
-[ #s1 #s2 #J #W2 #U2 #H destruct
-| #i #J #W2 #U2 #H destruct
-| #l #J #W2 #U2 #H destruct
-| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: tsts_inv_pair2 *)
-lemma theq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
- ∃∃W1,U1. T1 = ②{J}W1.U1.
-/2 width=7 by theq_inv_pair2_aux/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma theq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
- I1 = I2.
-#I1 #I2 #V1 #V2 #T1 #T2 #H elim (theq_inv_pair1 … H) -H
-#V0 #T0 #H destruct //
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: iso_refl *)
-(* Basic_2A1: was: tsts_refl *)
-lemma theq_refl: reflexive … theq.
-* //
-* /2 width=1 by theq_lref, theq_gref/
-qed.
-
-(* Basic_2A1: was: tsts_sym *)
-lemma theq_sym: symmetric … theq.
-#T1 #T2 * -T1 -T2 /2 width=3 by theq_sort/
-qed-.
-
-(* Basic_2A1: was: tsts_dec *)
-lemma theq_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
-* [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
-[ /3 width=1 by theq_sort, or_introl/
-|2,3,13:
- @or_intror #H
- elim (theq_inv_sort1 … H) -H #x #H destruct
-|4,6,14:
- @or_intror #H
- lapply (theq_inv_lref1 … H) -H #H destruct
-|5:
- elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
- @or_intror #H
- lapply (theq_inv_lref1 … H) -H #H destruct /2 width=1 by/
-|7,8,15:
- @or_intror #H
- lapply (theq_inv_gref1 … H) -H #H destruct
-|9:
- elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
- @or_intror #H
- lapply (theq_inv_gref1 … H) -H #H destruct /2 width=1 by/
-|10,11,12:
- @or_intror #H
- elim (theq_inv_pair1 … H) -H #X1 #X2 #H destruct
-|16:
- elim (eq_item2_dec I1 I2) #HI12 destruct
- [ /3 width=1 by theq_pair, or_introl/ ]
- @or_intror #H
- lapply (theq_inv_pair … H) -H /2 width=1 by/
-]
-qed-.
-
-(* Basic_2A1: removed theorems 2:
- tsts_inv_atom1 tsts_inv_atom2
-*)
+++ /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/syntax/term_simple.ma".
-include "static_2/syntax/theq.ma".
-
-(* HEAD EQUIVALENCE FOR TERMS ***********************************************)
-
-(* Properies with simple (neutral) terms ************************************)
-
-(* Basic_2A1: was: simple_tsts_repl_dx *)
-lemma simple_theq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 * -T1 -T2 //
-#I #V1 #V2 #T1 #T2 #H
-elim (simple_inv_pair … H) -H #J #H destruct //
-qed-.
-
-(* Basic_2A1: was: simple_tsts_repl_sn *)
-lemma simple_theq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-/3 width=3 by simple_theq_repl_dx, theq_sym/ 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/syntax/term_vector.ma".
-include "static_2/syntax/theq_simple.ma".
-
-(* HEAD EQUIVALENCE FOR TERMS ***********************************************)
-
-(* Advanced inversion lemmas with simple (neutral) terms ********************)
-
-(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
-lemma theq_inv_applv_bind_simple (p) (I):
- ∀Vs,V2,T1,T2. ⒶVs.T1 ⩳ ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥.
-#p #I #Vs #V2 #T1 #T2 #H elim (theq_inv_pair2 … H) -H
-#V0 #T0 elim Vs -Vs normalize
-[ #H destruct #H /2 width=5 by simple_inv_bind/
-| #V #Vs #_ #H destruct
-]
-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/syntax/tdeq.ma".
-include "static_2/syntax/theq.ma".
-
-(* HEAD EQUIVALENCE FOR TERMS ***********************************************)
-
-(* Properties with sort-irrelevant equivalence for terms ********************)
-
-lemma tdeq_theq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
-#T1 #T2 * -T1 -T2 /2 width=1 by theq_sort, theq_pair/
-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/syntax/theq.ma".
-
-(* HEAD EQUIVALENCE FOR TERMS ***********************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: iso_trans *)
-(* Basic_2A1: was: tsts_trans *)
-theorem theq_trans: Transitive … theq.
-#T1 #T * -T1 -T
-[ #s1 #s #X #H
- elim (theq_inv_sort1 … H) -s /2 width=1 by theq_sort/
-| #i1 #i #H <(theq_inv_lref1 … H) -H //
-| #l1 #l #H <(theq_inv_gref1 … H) -H //
-| #I #V1 #V #T1 #T #X #H
- elim (theq_inv_pair1 … H) -H #V2 #T2 #H destruct //
-]
-qed-.
-
-(* Basic_2A1: was: tsts_canc_sn *)
-theorem theq_canc_sn: left_cancellable … theq.
-/3 width=3 by theq_trans, theq_sym/ qed-.
-
-(* Basic_2A1: was: tsts_canc_dx *)
-theorem theq_canc_dx: right_cancellable … theq.
-/3 width=3 by theq_trans, theq_sym/ 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/notation/relations/topiso_2.ma".
+include "static_2/syntax/term.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Basic_2A1: includes: tsts_atom tsts_pair *)
+inductive toeq: relation term ≝
+| toeq_sort: ∀s1,s2. toeq (⋆s1) (⋆s2)
+| toeq_lref: ∀i. toeq (#i) (#i)
+| toeq_gref: ∀l. toeq (§l) (§l)
+| toeq_pair: ∀I,V1,V2,T1,T2. toeq (②{I}V1.T1) (②{I}V2.T2)
+.
+
+interpretation
+ "sort-irrelevant outer equivalence (term)"
+ 'TopIso T1 T2 = (toeq T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact toeq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
+ ∃s2. Y = ⋆s2.
+#X #Y * -X -Y
+[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
+| #i #s #H destruct
+| #l #s #H destruct
+| #I #V1 #V2 #T1 #T2 #s #H destruct
+]
+qed-.
+
+(* Basic_1: was just: iso_gen_sort *)
+lemma toeq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
+ ∃s2. Y = ⋆s2.
+/2 width=4 by toeq_inv_sort1_aux/ qed-.
+
+fact toeq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
+#X #Y * -X -Y //
+[ #s1 #s2 #j #H destruct
+| #I #V1 #V2 #T1 #T2 #j #H destruct
+]
+qed-.
+
+(* Basic_1: was: iso_gen_lref *)
+lemma toeq_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
+/2 width=5 by toeq_inv_lref1_aux/ qed-.
+
+fact toeq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l.
+#X #Y * -X -Y //
+[ #s1 #s2 #k #H destruct
+| #I #V1 #V2 #T1 #T2 #k #H destruct
+]
+qed-.
+
+lemma toeq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
+/2 width=5 by toeq_inv_gref1_aux/ qed-.
+
+fact toeq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 →
+ ∀J,W1,U1. T1 = ②{J}W1.U1 →
+ ∃∃W2,U2. T2 = ②{J}W2.U2.
+#T1 #T2 * -T1 -T2
+[ #s1 #s2 #J #W1 #U1 #H destruct
+| #i #J #W1 #U1 #H destruct
+| #l #J #W1 #U1 #H destruct
+| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+(* Basic_1: was: iso_gen_head *)
+(* Basic_2A1: was: tsts_inv_pair1 *)
+lemma toeq_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 →
+ ∃∃W2,U2. T2 = ②{J}W2. U2.
+/2 width=7 by toeq_inv_pair1_aux/ qed-.
+
+fact toeq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
+ ∀J,W2,U2. T2 = ②{J}W2.U2 →
+ ∃∃W1,U1. T1 = ②{J}W1.U1.
+#T1 #T2 * -T1 -T2
+[ #s1 #s2 #J #W2 #U2 #H destruct
+| #i #J #W2 #U2 #H destruct
+| #l #J #W2 #U2 #H destruct
+| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: tsts_inv_pair2 *)
+lemma toeq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
+ ∃∃W1,U1. T1 = ②{J}W1.U1.
+/2 width=7 by toeq_inv_pair2_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma toeq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
+ I1 = I2.
+#I1 #I2 #V1 #V2 #T1 #T2 #H elim (toeq_inv_pair1 … H) -H
+#V0 #T0 #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+(* Basic_2A1: was: tsts_refl *)
+lemma toeq_refl: reflexive … toeq.
+* //
+* /2 width=1 by toeq_lref, toeq_gref/
+qed.
+
+(* Basic_2A1: was: tsts_sym *)
+lemma toeq_sym: symmetric … toeq.
+#T1 #T2 * -T1 -T2 /2 width=3 by toeq_sort/
+qed-.
+
+(* Basic_2A1: was: tsts_dec *)
+lemma toeq_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
+* [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
+[ /3 width=1 by toeq_sort, or_introl/
+|2,3,13:
+ @or_intror #H
+ elim (toeq_inv_sort1 … H) -H #x #H destruct
+|4,6,14:
+ @or_intror #H
+ lapply (toeq_inv_lref1 … H) -H #H destruct
+|5:
+ elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+ @or_intror #H
+ lapply (toeq_inv_lref1 … H) -H #H destruct /2 width=1 by/
+|7,8,15:
+ @or_intror #H
+ lapply (toeq_inv_gref1 … H) -H #H destruct
+|9:
+ elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+ @or_intror #H
+ lapply (toeq_inv_gref1 … H) -H #H destruct /2 width=1 by/
+|10,11,12:
+ @or_intror #H
+ elim (toeq_inv_pair1 … H) -H #X1 #X2 #H destruct
+|16:
+ elim (eq_item2_dec I1 I2) #HI12 destruct
+ [ /3 width=1 by toeq_pair, or_introl/ ]
+ @or_intror #H
+ lapply (toeq_inv_pair … H) -H /2 width=1 by/
+]
+qed-.
+
+(* Basic_2A1: removed theorems 2:
+ tsts_inv_atom1 tsts_inv_atom2
+*)
--- /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/syntax/term_simple.ma".
+include "static_2/syntax/toeq.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properies with simple (neutral) terms ************************************)
+
+(* Basic_2A1: was: simple_tsts_repl_dx *)
+lemma simple_toeq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 * -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #H
+elim (simple_inv_pair … H) -H #J #H destruct //
+qed-.
+
+(* Basic_2A1: was: simple_tsts_repl_sn *)
+lemma simple_toeq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+/3 width=3 by simple_toeq_repl_dx, toeq_sym/ 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/syntax/term_vector.ma".
+include "static_2/syntax/toeq_simple.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Advanced inversion lemmas with simple (neutral) terms ********************)
+
+(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
+(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
+lemma toeq_inv_applv_bind_simple (p) (I):
+ ∀Vs,V2,T1,T2. ⒶVs.T1 ⩳ ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥.
+#p #I #Vs #V2 #T1 #T2 #H elim (toeq_inv_pair2 … H) -H
+#V0 #T0 elim Vs -Vs normalize
+[ #H destruct #H /2 width=5 by simple_inv_bind/
+| #V #Vs #_ #H destruct
+]
+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/syntax/tdeq.ma".
+include "static_2/syntax/toeq.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properties with sort-irrelevant equivalence for terms ********************)
+
+lemma tdeq_toeq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
+#T1 #T2 * -T1 -T2 /2 width=1 by toeq_sort, toeq_pair/
+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/syntax/toeq.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: iso_trans *)
+(* Basic_2A1: was: tsts_trans *)
+theorem toeq_trans: Transitive … toeq.
+#T1 #T * -T1 -T
+[ #s1 #s #X #H
+ elim (toeq_inv_sort1 … H) -s /2 width=1 by toeq_sort/
+| #i1 #i #H <(toeq_inv_lref1 … H) -H //
+| #l1 #l #H <(toeq_inv_gref1 … H) -H //
+| #I #V1 #V #T1 #T #X #H
+ elim (toeq_inv_pair1 … H) -H #V2 #T2 #H destruct //
+]
+qed-.
+
+(* Basic_2A1: was: tsts_canc_sn *)
+theorem toeq_canc_sn: left_cancellable … toeq.
+/3 width=3 by toeq_trans, toeq_sym/ qed-.
+
+(* Basic_2A1: was: tsts_canc_dx *)
+theorem toeq_canc_dx: right_cancellable … toeq.
+/3 width=3 by toeq_trans, toeq_sym/ 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/notation/relations/approxeq_2.ma".
+include "static_2/syntax/term_weight.ma".
+
+lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
+#I #V #T /2 width=1 by le_S_S/
+qed.
+
+(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
+
+inductive tweq: relation term ≝
+| tweq_sort: ∀s1,s2. tweq (⋆s1) (⋆s2)
+| tweq_lref: ∀i. tweq (#i) (#i)
+| tweq_gref: ∀l. tweq (§l) (§l)
+| tweq_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→tweq T1 T2) → tweq (ⓓ{p}V1.T1) (ⓓ{p}V2.T2)
+| tweq_abst: ∀p,V1,V2,T1,T2. tweq (ⓛ{p}V1.T1) (ⓛ{p}V2.T2)
+| tweq_appl: ∀V1,V2,T1,T2. tweq T1 T2 → tweq (ⓐV1.T1) (ⓐV2.T2)
+| tweq_cast: ∀V1,V2,T1,T2. tweq V1 V2 → tweq T1 T2 → tweq (ⓝV1.T1) (ⓝV2.T2)
+.
+
+interpretation
+ "context-free tail sort-irrelevant equivalence (term)"
+ 'ApproxEq T1 T2 = (tweq T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tweq_abbr_pos: ∀V1,V2,T1,T2. T1 ≅ T2 → +ⓓV1.T1 ≅ +ⓓV2.T2.
+/3 width=1 by tweq_abbr/ qed.
+
+lemma tweq_abbr_neg: ∀V1,V2,T1,T2. -ⓓV1.T1 ≅ -ⓓV2.T2.
+#V1 #V2 #T1 #T2
+@tweq_abbr #H destruct
+qed.
+
+lemma tweq_refl: reflexive … tweq.
+#T elim T -T * [||| #p * | * ]
+/2 width=1 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/
+qed.
+
+lemma tweq_sym: symmetric … tweq.
+#T1 #T2 #H elim H -T1 -T2
+/3 width=3 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/
+qed-.
+
+(* Left basic inversion lemmas **********************************************)
+
+fact tweq_inv_sort_sn_aux:
+ ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 → ∃s2. Y = ⋆s2.
+#X #Y * -X -Y
+[1 : #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
+|2,3: #i #s #H destruct
+|4 : #p #V1 #V2 #T1 #T2 #_ #s #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #s #H destruct
+|6 : #V1 #V2 #T1 #T2 #_ #s #H destruct
+|7 : #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
+]
+qed-.
+
+lemma tweq_inv_sort_sn:
+ ∀Y,s1. ⋆s1 ≅ Y → ∃s2. Y = ⋆s2.
+/2 width=4 by tweq_inv_sort_sn_aux/ qed-.
+
+fact tweq_inv_lref_sn_aux:
+ ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
+#X #Y * -X -Y
+[1 : #s1 #s2 #j #H destruct
+|2,3: //
+|4 : #p #V1 #V2 #T1 #T2 #_ #j #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #j #H destruct
+|6 : #V1 #V2 #T1 #T2 #_ #j #H destruct
+|7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
+]
+qed-.
+
+lemma tweq_inv_lref_sn: ∀Y,i. #i ≅ Y → Y = #i.
+/2 width=5 by tweq_inv_lref_sn_aux/ qed-.
+
+fact tweq_inv_gref_sn_aux:
+ ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
+#X #Y * -X -Y
+[1 : #s1 #s2 #k #H destruct
+|2,3: //
+|4 : #p #V1 #V2 #T1 #T2 #_ #k #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #k #H destruct
+|6 : #V1 #V2 #T1 #T2 #_ #k #H destruct
+|7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
+]
+qed-.
+
+lemma tweq_inv_gref_sn:
+ ∀Y,l. §l ≅ Y → Y = §l.
+/2 width=5 by tweq_inv_gref_sn_aux/ qed-.
+
+fact tweq_inv_abbr_sn_aux:
+ ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓓ{p}V1.T1 →
+ ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2.
+#X #Y * -X -Y
+[1 : #s1 #s2 #q #W1 #U1 #H destruct
+|2,3: #i #q #W1 #U1 #H destruct
+|4 : #p #V1 #V2 #T1 #T2 #HT #q #W1 #U1 #H destruct /3 width=4 by ex2_2_intro/
+|5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct
+|6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
+|7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
+]
+qed-.
+
+lemma tweq_inv_abbr_sn:
+ ∀p,V1,T1,Y. ⓓ{p}V1.T1 ≅ Y →
+ ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2.
+/2 width=4 by tweq_inv_abbr_sn_aux/ qed-.
+
+fact tweq_inv_abst_sn_aux:
+ ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓛ{p}V1.T1 →
+ ∃∃V2,T2. Y = ⓛ{p}V2.T2.
+#X #Y * -X -Y
+[1 : #s1 #s2 #q #W1 #U1 #H destruct
+|2,3: #i #q #W1 #U1 #H destruct
+|4 : #p #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
+|6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
+|7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
+]
+qed-.
+
+lemma tweq_inv_abst_sn:
+ ∀p,V1,T1,Y. ⓛ{p}V1.T1 ≅ Y →
+ ∃∃V2,T2. Y = ⓛ{p}V2.T2.
+/2 width=5 by tweq_inv_abst_sn_aux/ qed-.
+
+fact tweq_inv_appl_sn_aux:
+ ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓐV1.T1 →
+ ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2.
+#X #Y * -X -Y
+[1 : #s1 #s2 #W1 #U1 #H destruct
+|2,3: #i #W1 #U1 #H destruct
+|4 : #p #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
+|6 : #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct /2 width=4 by ex2_2_intro/
+|7 : #V1 #V2 #T1 #T2 #_ #_ #W1 #U1 #H destruct
+]
+qed-.
+
+lemma tweq_inv_appl_sn:
+ ∀V1,T1,Y. ⓐV1.T1 ≅ Y →
+ ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2.
+/2 width=4 by tweq_inv_appl_sn_aux/ qed-.
+
+fact tweq_inv_cast_sn_aux:
+ ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
+ ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
+#X #Y * -X -Y
+[1 : #s1 #s2 #W1 #U1 #H destruct
+|2,3: #i #W1 #U1 #H destruct
+|4 : #p #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
+|5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
+|6 : #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
+|7 : #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma tweq_inv_cast_sn:
+ ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
+ ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
+/2 width=3 by tweq_inv_cast_sn_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tweq_inv_abbr_pos_sn:
+ ∀V1,T1,Y. +ⓓV1.T1 ≅ Y → ∃∃V2,T2. T1 ≅ T2 & Y = +ⓓV2.T2.
+#V1 #V2 #Y #H
+elim (tweq_inv_abbr_sn … H) -H #V2 #T2
+/3 width=4 by ex2_2_intro/
+qed-.
+
+lemma tweq_inv_abbr_neg_sn:
+ ∀V1,T1,Y. -ⓓV1.T1 ≅ Y → ∃∃V2,T2. Y = -ⓓV2.T2.
+#V1 #V2 #Y #H
+elim (tweq_inv_abbr_sn … H) -H #V2 #T2 #_
+/2 width=3 by ex1_2_intro/
+qed-.
+
+lemma tweq_inv_abbr_pos_bi:
+ ∀V1,V2,T1,T2. +ⓓV1.T1 ≅ +ⓓV2.T2 → T1 ≅ T2.
+#V1 #V2 #T1 #T2 #H
+elim (tweq_inv_abbr_pos_sn … H) -H #W2 #U2 #HTU #H destruct //
+qed-.
+
+lemma tweq_inv_appl_bi:
+ ∀V1,V2,T1,T2. ⓐV1.T1 ≅ ⓐV2.T2 → T1 ≅ T2.
+#V1 #V2 #T1 #T2 #H
+elim (tweq_inv_appl_sn … H) -H #W2 #U2 #HTU #H destruct //
+qed-.
+
+lemma tweq_inv_cast_bi:
+ ∀V1,V2,T1,T2. ⓝV1.T1 ≅ ⓝV2.T2 → ∧∧ V1 ≅ V2 & T1 ≅ T2.
+#V1 #V2 #T1 #T2 #H
+elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
+/2 width=1 by conj/
+qed-.
+
+lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥.
+@(f_ind … tw) #n #IH #T #Hn #V #H destruct
+elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
+/2 width=4 by/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma tweq_fwd_pair_sn (I):
+ ∀V1,T1,X2. ②{I}V1.T1 ≅ X2 → ∃∃V2,T2. X2 = ②{I}V2.T2.
+* [ #p ] * [ cases p -p ] #V1 #T1 #X2 #H
+[ elim (tweq_inv_abbr_pos_sn … H) -H #V2 #T2 #_ #H
+| elim (tweq_inv_abbr_neg_sn … H) -H #V2 #T2 #H
+| elim (tweq_inv_abst_sn … H) -H #V2 #T2 #H
+| elim (tweq_inv_appl_sn … H) -H #V2 #T2 #_ #H
+| elim (tweq_inv_cast_sn … H) -H #V2 #T2 #_ #_ #H
+] /2 width=3 by ex1_2_intro/
+qed-.
+
+lemma tweq_fwd_pair_bi (I1) (I2):
+ ∀V1,V2,T1,T2. ②{I1}V1.T1 ≅ ②{I2}V2.T2 → I1 = I2.
+#I1 #I2 #V1 #V2 #T1 #T2 #H
+elim (tweq_fwd_pair_sn … H) -H #W2 #U2 #H destruct //
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma tweq_dec: ∀T1,T2. Decidable (T1 ≅ T2).
+#T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
+[ /3 width=1 by tweq_sort, or_introl/
+|2,3,13:
+ @or_intror #H
+ elim (tweq_inv_sort_sn … H) -H #x #H destruct
+|4,6,14:
+ @or_intror #H
+ lapply (tweq_inv_lref_sn … H) -H #H destruct
+|5:
+ elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+ @or_intror #H
+ lapply (tweq_inv_lref_sn … H) -H #H destruct /2 width=1 by/
+|7,8,15:
+ @or_intror #H
+ lapply (tweq_inv_gref_sn … H) -H #H destruct
+|9:
+ elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+ @or_intror #H
+ lapply (tweq_inv_gref_sn … H) -H #H destruct /2 width=1 by/
+|10,11,12:
+ @or_intror #H
+ elim (tweq_fwd_pair_sn … H) -H #X1 #X2 #H destruct
+|16:
+ elim (eq_item2_dec I1 I2) #HI12 destruct
+ [ cases I2 -I2 [ #p ] * [ cases p -p ]
+ [ elim (IHT T2) -IHT #HT12
+ [ /3 width=1 by tweq_abbr_pos, or_introl/
+ | /4 width=3 by tweq_inv_abbr_pos_bi, or_intror/
+ ]
+ | /3 width=1 by tweq_abbr_neg, or_introl/
+ | /3 width=1 by tweq_abst, or_introl/
+ | elim (IHT T2) -IHT #HT12
+ [ /3 width=1 by tweq_appl, or_introl/
+ | /4 width=3 by tweq_inv_appl_bi, or_intror/
+ ]
+ | elim (IHV V2) -IHV #HV12
+ elim (IHT T2) -IHT #HT12
+ [1: /3 width=1 by tweq_cast, or_introl/
+ |*: @or_intror #H
+ elim (tweq_inv_cast_bi … H) -H #HV12 #HT12
+ /2 width=1 by/
+ ]
+ ]
+ | /4 width=5 by tweq_fwd_pair_bi, 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/syntax/term_simple.ma".
+include "static_2/syntax/tweq.ma".
+
+(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
+
+(* Properties with simple terms *********************************************)
+
+lemma tweq_simple_trans:
+ ∀T1,T2. T1 ≅ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 * -T1 -T2
+[4,5: #p #V1 #V2 #T1 #T2 [ #_ ] #H
+ elim (simple_inv_bind … H)
+|* : /1 width=1 by simple_atom, simple_flat/
+]
+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/syntax/tweq.ma".
+
+(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
+
+(* Main properties **********************************************************)
+
+theorem tweq_trans: Transitive … tweq.
+#T1 #T #H elim H -T1 -T
+[ #s1 #s #X #H
+ elim (tweq_inv_sort_sn … H) -s #s2 destruct
+ /2 width=1 by tweq_sort/
+| #i1 #i #H //
+| #l1 #l #H //
+| #p #V1 #V #T1 #T #_ #IHT #X #H
+ elim (tweq_inv_abbr_sn … H) -H #V2 #T2 #HT #H destruct
+ /4 width=1 by tweq_abbr/
+| #p #V1 #V #T1 #T #X #H
+ elim (tweq_inv_abst_sn … H) -H #V2 #T2 #H destruct
+ /2 width=1 by tweq_abst/
+| #V1 #V #T1 #T #_ #IHT #X #H
+ elim (tweq_inv_appl_sn … H) -H #V2 #T2 #HT #H destruct
+ /3 width=1 by tweq_appl/
+| #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H
+ elim (tweq_inv_cast_sn … H) -H #V2 #T2 #HV #HT #H destruct
+ /3 width=1 by tweq_cast/
+]
+qed-.
+
+theorem tweq_canc_sn: left_cancellable … tweq.
+/3 width=3 by tweq_trans, tweq_sym/ qed-.
+
+theorem tweq_canc_dx: right_cancellable … tweq.
+/3 width=3 by tweq_trans, tweq_sym/ qed-.
+
+theorem tweq_repl:
+ ∀T1,T2. T1 ≅ T2 → ∀U1. T1 ≅ U1 → ∀U2. T2 ≅ U2 → U1 ≅ U2.
+/3 width=3 by tweq_canc_sn, tweq_trans/ qed-.
[ { "generic and uniform relocation" * } {
[ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
[ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≘ ? )" "lifts_lifts_vector" * ]
- [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tueq" + "lifts_lifts" * ]
+ [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_toeq" + "lifts_lifts" * ]
}
]
[ { "syntactic equivalence" * } {
[ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
}
]
- [ { "sort-irrelevant head equivalence" * } {
- [ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
+ [ { "sort-irrelevant outer equivalence" * } {
+ [ [ "for terms" ] "toeq" + "( ? ⩳ ? )" "toeq_simple" + "toeq_tdeq" + "toeq_toeq" + "toeq_simple_vector" * ]
+ }
+ ]
+ [ { "sort-irrelevant whd equivalence" * } {
+ [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tueq" * ]
}
]
[ { "sort-irrelevant equivalence" * } {
projects / helm.git / commitdiff