+++ /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/cpxs_reqx.ma".
-include "basic_2/rt_computation/cpms_cpxs.ma".
-
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-lemma cpms_reqx_conf_sn (h) (n) (G) (L1) (L2):
- ∀T1,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 →
- L1 ≛[T1] L2 → L1 ≛[T2] L2.
-/3 width=5 by cpms_fwd_cpxs, cpxs_reqx_conf_sn/ qed-.
-
-lemma cpms_reqx_conf_dx (h) (n) (G) (L1) (L2):
- ∀T1,T2. ❪G,L2❫ ⊢ T1 ➡*[h,n] T2 →
- L1 ≛[T1] L2 → L1 ≛[T2] L2.
-/3 width=5 by cpms_fwd_cpxs, cpxs_reqx_conf_dx/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/relocation/lifts_teqx.ma".
-include "basic_2/rt_transition/cpr_drops_basic.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
-
-(* Properties with context-free sort-irrelevant equivalence *****************)
-
-lemma cpr_abbr_pos_tneqx (h) (G) (L) (V) (T1):
- ∃∃T2. ❪G,L❫ ⊢ +ⓓV.T1 ➡[h,0] 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 (teqx_dec U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ]
-[ elim (teqx_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
- /3 width=9 by cpm_zeta, teqx_lifts_inv_pair_sn, ex2_intro/
-| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H
- elim (teqx_inv_pair … H) -H #_ #_ /2 width=1 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/static/feqx.ma".
-include "basic_2/rt_transition/cpx_reqx.ma".
-include "basic_2/rt_transition/rpx_reqx.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
-
-(* Properties with sort-irrelevant equivalence for closures *****************)
-
-(**) (* to update *)
-lemma feqx_cpx_trans:
- ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛ ❪G2,L2,T❫ →
- ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 →
- ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈ T0 & ❪G1,L1,T0❫ ≛ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2
-elim (feqx_inv_gen_dx … H) -H #H #HL12 #HT1 destruct
-lapply (reqx_cpx_trans … HL12 … HT2) #H
-lapply (cpx_reqx_conf_dx … HT2 … HL12) -HT2 -HL12 #HL12
-lapply (teqx_cpx_trans … HT1 … H) -T #HT12
-/3 width=3 by feqx_intro_dx, 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/static/req_length.ma".
-include "static_2/static/req_drops.ma".
-include "basic_2/rt_transition/rpx_fsle.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
-
-(* Properties with syntactic equivalence for lenvs on referred entries ******)
-
-(* Basic_2A1: was: lleq_cpx_trans *)
-lemma req_cpx_trans (G): R_transitive_req (cpx G).
-#G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/
-[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
- elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct
- /3 width=3 by cpx_delta/
-| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
- elim (req_inv_lref_bind_dx … H) -H #I1 #K1 #HK12 #H destruct
- /3 width=3 by cpx_lref/
-| #p #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H
- elim (req_inv_bind … H) -H /3 width=1 by cpx_bind/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H
- elim (req_inv_flat … H) -H /3 width=1 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #HT1 #_ #IH #L1 #H
- elim (req_inv_bind … H) -H #HV2 #H
- lapply (req_inv_lifts_bi … H (Ⓣ) … HT1) -H [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT
- /3 width=3 by cpx_zeta/
-| #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H
- elim (req_inv_flat … H) -H /3 width=1 by cpx_eps/
-| #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H
- elim (req_inv_flat … H) -H /3 width=1 by cpx_ee/
-| #p #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H
- elim (req_inv_flat … H) -H #HV1 #H
- elim (req_inv_bind … H) -H /3 width=1 by cpx_beta/
-| #p #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV1 #IHW12 #IHT12 #HV2 #L1 #H
- elim (req_inv_flat … H) -H #HV1 #H
- elim (req_inv_bind … H) -H /3 width=3 by cpx_theta/
-]
-qed-.
-
-lemma cpx_req_conf (G): R_confluent1_rex (cpx G) ceq.
-/3 width=3 by req_cpx_trans, req_sym/ qed-.
-
-(* Basic_2A1: was: cpx_lleq_conf_sn *)
-lemma cpx_req_conf_sn (G): s_r_confluent1 … (cpx G) req.
-/2 width=5 by cpx_rex_conf_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/static/reqx_reqx.ma".
-include "basic_2/rt_transition/rpx_fsle.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-(* Basic_2A1: was just: cpx_lleq_conf_sn *)
-lemma cpx_reqx_conf_sn (G):
- s_r_confluent1 … (cpx G) reqx.
-/3 width=6 by cpx_rex_conf_sn/ qed-.
-
-(* Basic_2A1: was just: cpx_lleq_conf_dx *)
-lemma cpx_reqx_conf_dx (G) (L2):
- ∀T1,T2. ❪G,L2❫ ⊢ T1 ⬈ T2 →
- ∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2.
-/4 width=5 by cpx_reqx_conf_sn, reqx_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/static/feqx.ma".
-include "basic_2/rt_computation/cpxs_reqx.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
-
-(* Properties with sort-irrelevant equivalence for closures *****************)
-
-(* to be updated *)
-lemma feqx_cpxs_trans:
- ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛ ❪G2,L2,T❫ →
- ∀T2. ❪G2,L2❫ ⊢ T ⬈* T2 →
- ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈* T0 & ❪G1,L1,T0❫ ≛ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T #H #T2 #H2T2
-elim (feqx_inv_gen_dx … H) -H #H #HL12 #HT1 destruct
-lapply (reqx_cpxs_trans … H2T2 … HL12) #H1T2
-lapply (cpxs_reqx_conf_dx … H2T2 … HL12) -HL12 #HL12
-lapply (teqx_cpxs_trans … HT1 … H1T2) -T #HT12
-/3 width=3 by feqx_intro_dx, ex2_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/cpx_reqx.ma".
-include "basic_2/rt_computation/cpxs_teqx.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-(* Basic_2A1: was just: lleq_cpxs_trans *)
-lemma reqx_cpxs_trans (G):
- ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈* T1 → ∀L2. L2 ≛[T0] L0 → ❪G,L2❫ ⊢ T0 ⬈* T1.
-#G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 //
-#T0 #T #H0T0 #_ #IH #L2 #HL2
-lapply (reqx_cpx_trans … HL2 … H0T0) #H2T0
-lapply (IH L2 ?) -IH /2 width=5 by cpx_reqx_conf_dx/ -L0 #H2T1
-/2 width=3 by cpxs_strap2/
-qed-.
-
-(* Basic_2A1: was just: cpxs_lleq_conf *)
-lemma cpxs_reqx_conf (G):
- ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈* T1 → ∀L2. L0 ≛[T0] L2 → ❪G,L2❫ ⊢ T0 ⬈* T1.
-/3 width=3 by reqx_cpxs_trans, reqx_sym/ qed-.
-
-(* Basic_2A1: was just: cpxs_lleq_conf_dx *)
-lemma cpxs_reqx_conf_dx (G):
- ∀L2,T1,T2. ❪G,L2❫ ⊢ T1 ⬈* T2 →
- ∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2.
-#G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_reqx_conf_dx/
-qed-.
-
-(* Basic_2A1: was just: lleq_conf_sn *)
-lemma cpxs_reqx_conf_sn (G):
- ∀L1,T1,T2. ❪G,L1❫ ⊢ T1 ⬈* T2 →
- ∀L2. L1 ≛[T1] L2 → L1 ≛[T2] L2.
-/4 width=6 by cpxs_reqx_conf_dx, reqx_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 "basic_2/rt_transition/rpx_reqx.ma".
-include "basic_2/rt_computation/cpxs.ma".
-
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
-
-(* Properties with sort-irrelevant equivalence for terms ********************)
-
-lemma teqx_cpxs_trans (G) (L) (T):
- ∀T1. T1 ≛ T → ∀T2. ❪G,L❫ ⊢ T ⬈* T2 → ❪G,L❫ ⊢ T1 ⬈* T2.
-#G #L #T #T1 #HT1 #T2 #HT2 @(cpxs_ind … HT2) -T2
-[ /3 width=1 by teqx_cpx, cpx_cpxs/
-| /2 width=3 by cpxs_strap1/
-]
-qed-.
-
-(* Note: this requires teqx to be symmetric *)
-(* Nasic_2A1: uses: cpxs_neq_inv_step_sn *)
-lemma cpxs_tneqx_fwd_step_sn (G) (L):
- ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≛ T2 → ⊥) →
- ∃∃T. ❪G,L❫ ⊢ T1 ⬈ T & T1 ≛ T → ⊥ & ❪G,L❫ ⊢ T ⬈* T2.
-#G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
-[ #H elim H -H //
-| #T1 #T0 #HT10 #HT02 #IH #HnT12
- elim (teqx_dec T1 T0) [ -HT10 -HT02 #HT10 | -IH #HnT10 ]
- [ elim IH -IH /3 width=3 by teqx_trans/ -HnT12
- #T #HT0 #HnT0 #HT2
- lapply (teqx_cpx_trans … HT10 … HT0) -HT0 #HT1
- /4 width=4 by teqx_canc_sn, ex3_intro/
- | /3 width=4 by ex3_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/static/feqx.ma".
-include "basic_2/rt_computation/csx_reqx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
-
-(* Properties with sort-irrelevant equivalence for closures *****************)
-
-lemma csx_feqx_conf:
- ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2.
-#G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
-/3 width=3 by csx_reqx_conf, csx_teqx_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/rt_transition/cpx_reqx.ma".
-include "basic_2/rt_computation/csx_csx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-(* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_reqx_conf (G) (L1):
- ∀T. ❪G,L1❫ ⊢ ⬈*𝐒 T →
- ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T.
-#G #L1 #T #H
-@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
-@csx_intro #T2 #HT12 #HnT12
-lapply (reqx_cpx_trans … HL12 … HT12) -HT12
-/3 width=4 by cpx_reqx_conf_sn/
-qed-.
-
-(* Basic_2A1: uses: csx_lleq_trans *)
-lemma csx_reqx_trans (G) (L2):
- ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T → ❪G,L1❫ ⊢ ⬈*𝐒 T.
-/3 width=3 by csx_reqx_conf, reqx_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/s_transition/fqu_teqx.ma".
-include "static_2/static/feqx.ma".
-include "basic_2/rt_transition/fpb_reqx.ma".
-
-(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
-
-(* Properties with degree-based equivalence for closures ********************)
-
-(* Basic_2A1: uses: fleq_fpb_trans *)
-lemma feqx_fpb_trans:
- ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≛ ❪F2,K2,T2❫ →
- ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ →
- ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫.
-#F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
-#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12
-elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0
-elim (reqx_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0
-@(ex2_3_intro … H) -H (**) (* full auto too slow *)
-/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf_sn, teqx_trans/
-qed-.
-
-(* Inversion lemmas with degree-based equivalence for closures **************)
-
-(* Basic_2A1: uses: fpb_inv_fleq *)
-lemma fpb_inv_feqx:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ⊥.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #H elim (feqx_inv_gen_sn … H) -H
- /3 width=11 by reqx_fwd_length, fqu_inv_teqx/
-| #T2 #_ #HnT #H elim (feqx_inv_gen_sn … H) -H /2 width=1 by/
-| #L2 #_ #HnL #H elim (feqx_inv_gen_sn … H) -H /2 width=1 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/static/reqx_fqus.ma".
-include "basic_2/rt_transition/cpx_reqx.ma".
-include "basic_2/rt_transition/lpx_reqx.ma".
-include "basic_2/rt_transition/fpb.ma".
-
-(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-lemma teqx_fpb_trans:
- ∀U2,U1. U2 ≛ U1 →
- ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ →
- ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
-#U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1
-[ #G2 #L2 #T1 #H
- elim (teqx_fqu_trans … H … HU21) -H
- /3 width=5 by fpb_fqu, ex3_2_intro/
-| #T1 #HUT1 #HnUT1
- lapply (teqx_cpx_trans … HU21 … HUT1) -HUT1
- /6 width=5 by fpb_cpx, teqx_canc_sn, teqx_trans, ex3_2_intro/
-| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf_sn, ex3_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was just: lleq_fpb_trans *)
-lemma reqx_fpb_trans:
- ∀F,K1,K2,T. K1 ≛[T] K2 →
- ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ →
- ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛ U & L1 ≛[U] L2.
-#F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
-[ #G #L2 #U #H2 elim (reqx_fqu_trans … H2 … HT) -K2
- /3 width=5 by fpb_fqu, ex3_2_intro/
-| #U #HTU #HnTU lapply (reqx_cpx_trans … HT … HTU) -HTU
- /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf_sn, ex3_2_intro/ (**) (* time: 36s on dev *)
-| #L2 #HKL2 #HnKL2 elim (reqx_lpx_trans … HKL2 … HT) -HKL2
- /6 width=5 by fpb_lpx, (* 2x *) reqx_canc_sn, ex3_2_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/static/feqx.ma".
-include "basic_2/rt_transition/rpx_reqx.ma".
-include "basic_2/rt_transition/fpbq.ma".
-
-(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-
-(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *)
-lemma fpbq_feqx (G1) (G2):
- ∀L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H
-elim (feqx_inv_gen_sn … H) #H #HL12 #HT12 destruct
-/3 width=3 by fpbq_rcpx, reqx_rpx_trans, teqx_cpx_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/rt_transition/fpb_feqx.ma".
-include "basic_2/rt_computation/fsb.ma".
-
-(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
-
-(* Properties with sort-irrelevant equivalence for closures *****************)
-
-lemma fsb_feqx_trans:
- ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
-#G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
-#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12
-@fsb_intro #G #L #T #H2
-elim (feqx_fpb_trans … H12 … H2) -G2 -L2 -T2
-/2 width=5 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/static/reqx_req.ma".
-include "basic_2/rt_transition/rpx_reqx.ma".
-include "basic_2/rt_transition/rpx_lpx.ma".
-
-(* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************)
-
-(* Properties with sort-irrelevant equivalence for local environments *******)
-
-lemma reqx_lpx_trans_rpx (G) (L) (T:term):
- ∀L1. L1 ≛[T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2.
-/3 width=1 by lpx_rpx, reqx_rpx_trans/ qed.
-
-(* Basic_2A1: uses: lleq_lpx_trans *)
-lemma reqx_lpx_trans (G):
- ∀L2,K2. ❪G,L2❫ ⊢ ⬈ K2 → ∀L1. ∀T:term. L1 ≛[T] L2 →
- ∃∃K1. ❪G,L1❫ ⊢ ⬈ K1 & K1 ≛[T] K2.
-#G #L2 #K2 #HLK2 #L1 #T #HL12
-lapply (lpx_rpx … T … HLK2) -HLK2 #HLK2
-lapply (reqx_rpx_trans … HL12 … HLK2) -L2 #H
-elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12
-/3 width=3 by req_reqx, ex2_intro/
-qed-.
-
-(* Inversion lemmas with sort-irrelevant equivalence for local environments *)
-
-lemma rpx_inv_reqx_lpx (G) (T):
- ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
- ∃∃L. L1 ≛[T] L & ❪G,L❫ ⊢ ⬈ L2.
-#G #T #L1 #L2 #H
-elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2
-/3 width=3 by req_reqx, ex2_intro/
-qed-.
-
-(* Forward lemmas with sort-irrelevant equivalence for local environments ***)
-
-lemma rpx_fwd_lpx_reqx (G) (T):
- ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
- ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≛[T] L2.
-#G #T #L1 #L2 #H
-elim (rpx_fwd_lpx_req … H) -H #L #HL1 #HL2
-/3 width=3 by req_reqx, 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/static/feqx.ma".
-include "basic_2/rt_computation/lpxs_reqx.ma".
-
-(* EXTENDED PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
-
-(* Properties with sort-irrelevant equivalence on closures ******************)
-
-lemma feqx_lpxs_trans:
- ∀G1,G2,L1,L0,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L0,T2❫ →
- ∀L2. ❪G2,L0❫ ⊢⬈* L2 →
- ∃∃L. ❪G1,L1❫ ⊢⬈* L & ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02
-elim (feqx_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct
-elim (reqx_lpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02
-/3 width=3 by feqx_intro_dx, ex2_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/lpx_reqx.ma".
-include "basic_2/rt_computation/lpxs_lpx.ma".
-
-(* EXTENDED PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS *************)
-
-(* Properties with sort-irrelevant equivalence on referred entries **********)
-
-(* Basic_2A1: uses: lleq_lpxs_trans *)
-lemma reqx_lpxs_trans (G) (T:term):
- ∀L2,K2. ❪G,L2❫ ⊢ ⬈* K2 → ∀L1. L1 ≛[T] L2 →
- ∃∃K1. ❪G,L1❫ ⊢ ⬈* K1 & K1 ≛[T] K2.
-#G #T #L2 #K2 #H @(lpxs_ind_sn … H) -L2 /2 width=3 by ex2_intro/
-#L #L2 #HL2 #_ #IH #L1 #HT
-elim (reqx_lpx_trans … HL2 … HT) -L #L #HL1 #HT
-elim (IH … HT) -L2 #K #HLK #HT
-/3 width=3 by lpxs_step_sn, ex2_intro/
-qed-.
-
-(* Basic_2A1: uses: lpxs_nlleq_inv_step_sn *)
-lemma lpxs_rneqx_inv_step_sn (G) (T:term):
- ∀L1,L2. ❪G,L1❫ ⊢ ⬈* L2 → (L1 ≛[T] L2 → ⊥) →
- ∃∃L,L0. ❪G,L1❫ ⊢ ⬈ L & L1 ≛[T] L → ⊥ & ❪G,L❫ ⊢ ⬈* L0 & L0 ≛[T] L2.
-#G #T #L1 #L2 #H @(lpxs_ind_sn … H) -L1
-[ #H elim H -H //
-| #L1 #L #H1 #H2 #IH2 #H12 elim (reqx_dec L1 L T) #H
- [ -H1 -H2 elim IH2 -IH2 /3 width=3 by reqx_trans/ -H12
- #L0 #L3 #H1 #H2 #H3 #H4 lapply (reqx_rneqx_trans … H … H2) -H2
- #H2 elim (reqx_lpx_trans … H1 … H) -L
- #L #H1 #H lapply (rneqx_reqx_div … H … H2) -H2
- #H2 elim (reqx_lpxs_trans … H3 … H) -L0
- /3 width=8 by reqx_trans, ex4_2_intro/
- | -H12 -IH2 /3 width=6 by ex4_2_intro/
- ]
-]
-qed-.
(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
-inductive fsb: relation3 genv lenv term ≝
-| fsb_intro: ∀G1,L1,T1.
- (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → fsb G2 L2 T2) →
- fsb G1 L1 T1
-.
+definition fsb: relation3 genv lenv term ≝
+ SN3 … fpb (feqg sfull).
interpretation
"strong normalization for parallel rst-transition (closure)"
'PRedSubTyStrong G L T = (fsb G L T).
+(* Basic properties *********************************************************)
+
+lemma fsb_intro (G1) (L1) (T1):
+ (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) → ≥𝐒 ❪G1,L1,T1❫.
+/5 width=1 by fpbc_intro, SN3_intro/ qed.
+
(* Basic eliminators ********************************************************)
(* Note: eliminator with shorter ground hypothesis *)
-(* Note: to be named fsb_ind when fsb becomes a definition like csx, rsx ****)
-lemma fsb_ind_alt (Q:relation3 …):
+lemma fsb_ind (Q:relation3 …):
(∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
∀G,L,T. ≥𝐒 ❪G,L,T❫ → Q G L T.
#Q #IH #G #L #T #H elim H -G -L -T
-/4 width=1 by fsb_intro/
+#G1 #L1 #T1 #H1 #IH1
+@IH -IH [ /4 width=1 by SN3_intro/ ] -H1 #G2 #L2 #T2 #H
+elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12 /3 width=1 by/
qed-.
(* Basic_2A1: removed theorems 6:
lemma fsb_inv_csx:
∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
-#G #L #T #H @(fsb_ind_alt … H) -G -L -T
+#G #L #T #H @(fsb_ind … H) -G -L -T
/5 width=1 by csx_intro, cpx_fpbc/
qed-.
Q G1 L1 T1
) →
∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
-/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
+/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind/ qed-.
lemma csx_ind_fpbg (Q:relation3 …):
(∀G1,L1,T1.
reflexive … S → symmetric … S → Transitive … S →
∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
-#S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12
@fsb_intro #G #L #T #H2
elim (feqg_fpbc_trans … H12 … H2) -G2 -L2 -T2
lemma fsb_fpbs_trans:
∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
-#G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
elim (fpbs_inv_fpbg … H12) -H12
[ -IH /2 width=9 by fsb_feqg_trans/
) →
∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
-#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
@IH1 -IH1
[ -IH /2 width=5 by fsb_fpbs_trans/
<table name="basic_2_sum"/>
<news class="gamma" date="2020-09-25.">
- Improved rst-transition and related theory.
+ Improved theory of rst-transition.
</news>
<news class="gamma" date="2020-04-16.">
Sort hierarchy parameter removed from unbound rt-transition
definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
-interpretation "2-relation inclusion"
- 'subseteq R1 R2 = (subR2 ?? R1 R2).
+interpretation
+ "2-relation inclusion"
+ 'subseteq R1 R2 = (subR2 ?? R1 R2).
definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
-interpretation "3-relation inclusion"
- 'subseteq R1 R2 = (subR3 ??? R1 R2).
+interpretation
+ "3-relation inclusion"
+ 'subseteq R1 R2 = (subR3 ??? R1 R2).
(* Properties of relations **************************************************)
λR,S,a1. ∀a2. R a1 a2 → S a1 a2.
definition NF_dec (A): relation A → relation A → Prop ≝
- λR,S. ∀a1. NF A R S a1 ∨
+ λR,S. ∀a1. NF … R S a1 ∨
∃∃a2. R … a1 a2 & (S a1 a2 → ⊥).
inductive SN (A) (R,S:relation A): predicate A ≝
-| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN … R S a2) → SN … R S a1
.
lemma NF_to_SN (A) (R) (S): ∀a. NF A R S a → SN A R S a.
qed.
definition NF_sn (A): relation A → relation A → predicate A ≝
- λR,S,a2. ∀a1. R a1 a2 → S a1 a2.
+ λR,S,a2. ∀a1. R a1 a2 → S a1 a2.
inductive SN_sn (A) (R,S:relation A): predicate A ≝
-| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
+| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn … R S a1) → SN_sn … R S a2
.
lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a.
elim HSa12 -HSa12 /2 width=1 by/
qed.
+(* Normal form and strong normalization on unboxed triples ******************)
+
+inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝
+| SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1
+.
+
(* Relations on unboxed triples *********************************************)
definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/static/reqx_fqup.ma".
-include "static_2/static/feqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-
-(* Properties with sort-irrelevant equivalence for terms ********************)
-
-lemma teqx_feqx: ∀T1,T2. T1 ≛ T2 →
- ∀G,L. ❪G,L,T1❫ ≛ ❪G,L,T2❫.
-/2 width=1 by feqx_intro_sn/ qed.
-
-(* Advanced properties ******************************************************)
-
-lemma feqx_refl: tri_reflexive … feqx.
-/2 width=1 by feqx_intro_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/static/reqx_fqus.ma".
-include "static_2/static/feqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-
-(* Properties with star-iterated structural successor for closures **********)
-
-lemma feqx_fqus_trans (b):
- ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ →
- ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫.
-#b #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2
-elim(feqx_inv_gen_dx … H1) -H1 #HG #HL1 #HT1 destruct
-elim (reqx_fqus_trans … H2 … HL1) -L #L #T0 #H2 #HT02 #HL2
-elim (teqx_fqus_trans … H2 … HT1) -T #L0 #T #H2 #HT0 #HL0
-lapply (teqx_reqx_conf_sn … HT02 … HL0) -HL0 #HL0
-/4 width=7 by feqx_intro_dx, reqx_trans, teqx_trans, ex2_3_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/static/reqx_req.ma".
-include "static_2/static/feqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-
-(* Properties with syntactic equivalence on referred entries ****************)
-
-lemma req_feqx_trans: ∀L1,L,T1. L1 ≡[T1] L →
- ∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
-#L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H
-elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct
-/3 width=3 by feqx_intro_sn, req_reqx_trans/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/notation/relations/ideqsn_3.ma".
-include "static_2/static/rex.ma".
-
-(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
-
-(* Basic_2A1: was: lleq *)
-definition req: relation3 term lenv lenv ≝
- rex ceq.
-
-interpretation
- "syntactic equivalence on referred entries (local environment)"
- 'IdEqSn T L1 L2 = (req T L1 L2).
-
-(* Note: "R_transitive_req R" is equivalent to "R_transitive_rex ceq R R" *)
-(* Basic_2A1: uses: lleq_transitive *)
-definition R_transitive_req: predicate (relation3 lenv term term) ≝
- λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma req_inv_bind:
- ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 →
- ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V.
-/2 width=2 by rex_inv_bind/ qed-.
-
-lemma req_inv_flat:
- ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 →
- ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
-/2 width=2 by rex_inv_flat/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma req_inv_zero_pair_sn:
- ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 →
- ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V.
-#I #L2 #K1 #V #H
-elim (rex_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
-/2 width=3 by ex2_intro/
-qed-.
-
-lemma req_inv_zero_pair_dx:
- ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V →
- ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V.
-#I #L1 #K2 #V #H
-elim (rex_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
-/2 width=3 by ex2_intro/
-qed-.
-
-lemma req_inv_lref_bind_sn:
- ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 →
- ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2].
-/2 width=2 by rex_inv_lref_bind_sn/ qed-.
-
-lemma req_inv_lref_bind_dx:
- ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] →
- ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1].
-/2 width=2 by rex_inv_lref_bind_dx/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-(* Basic_2A1: was: llpx_sn_lrefl *)
-(* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
-lemma req_fwd_rex (R):
- c_reflexive … R →
- ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
-#R #HR #L1 #L2 #T * #f #Hf #HL12
-/4 width=7 by sex_co, cext2_co, ex2_intro/
-qed-.
-
-(* Basic_properties *********************************************************)
-
-lemma frees_req_conf:
- ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
- ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
-#f #L1 #T #H elim H -f -L1 -T
-[ /2 width=3 by frees_sort/
-| #f #i #Hf #L2 #H2
- >(rex_inv_atom_sn … H2) -L2
- /2 width=1 by frees_atom/
-| #f #I #L1 #V1 #_ #IH #Y #H2
- elim (req_inv_zero_pair_sn … H2) -H2 #L2 #HL12 #H destruct
- /3 width=1 by frees_pair/
-| #f #I #L1 #Hf #Y #H2
- elim (rex_inv_zero_unit_sn … H2) -H2 #g #L2 #_ #_ #H destruct
- /2 width=1 by frees_unit/
-| #f #I #L1 #i #_ #IH #Y #H2
- elim (req_inv_lref_bind_sn … H2) -H2 #J #L2 #HL12 #H destruct
- /3 width=1 by frees_lref/
-| /2 width=1 by frees_gref/
-| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
- elim (req_inv_bind … H2) -H2 /3 width=5 by frees_bind/
-| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
- elim (req_inv_flat … H2) -H2 /3 width=5 by frees_flat/
-]
-qed-.
-
-(* Basic_2A1: removed theorems 10:
- lleq_ind lleq_fwd_lref
- lleq_fwd_drop_sn lleq_fwd_drop_dx
- lleq_skip lleq_lref lleq_free
- lleq_Y lleq_ge_up lleq_ge
-
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/static/rex_drops.ma".
-include "static_2/static/req.ma".
-
-(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
-
-(* Note: req_inv_lifts_dx missing in basic_2A1 *)
-
-(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
-lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔❪f❫ →
- ∀K1,K2. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 →
- ∀T. ⇧*[f] T ≘ U → K1 ≡[T] K2.
-/2 width=10 by rex_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/static/rex_fqup.ma".
-include "static_2/static/req.ma".
-
-(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: was: lleq_refl *)
-lemma req_refl: ∀T. reflexive … (req T).
-/2 width=1 by rex_refl/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/static/rex_length.ma".
-include "static_2/static/rex_fsle.ma".
-include "static_2/static/req.ma".
-
-(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
-
-(* Advanved properties with free variables inclusion ************************)
-
-lemma req_fsge_comp:
- rex_fsge_compatible ceq.
-#L1 #L2 #T #H elim H #f1 #Hf1 #HL12
-lapply (frees_req_conf … Hf1 … H) -H
-lapply (sex_fwd_length … HL12)
-/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
-qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: uses: lleq_sym *)
-lemma req_sym (T):
- symmetric … (req T).
-/3 width=1 by req_fsge_comp, rex_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/relocation/lifts_teqx.ma".
-include "static_2/static/rex_drops.ma".
-include "static_2/static/reqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-
-(* Properties with generic slicing for local environments *******************)
-
-lemma reqx_lifts_sn: f_dedropable_sn cdeq.
-/3 width=5 by rex_liftable_dedropable_sn, teqx_lifts_sn/ qed-.
-
-(* Inversion lemmas with generic slicing for local environments *************)
-
-lemma reqx_inv_lifts_sn: f_dropable_sn cdeq.
-/2 width=5 by rex_dropable_sn/ qed-.
-
-lemma reqx_inv_lifts_dx: f_dropable_dx cdeq.
-/2 width=5 by rex_dropable_dx/ qed-.
-
-lemma reqx_inv_lifts_bi: ∀L1,L2,U. L1 ≛[U] L2 → ∀b,f. 𝐔❪f❫ →
- ∀K1,K2. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 →
- ∀T. ⇧*[f] T ≘ U → K1 ≛[T] K2.
-/2 width=10 by rex_inv_lifts_bi/ qed-.
-
-lemma reqx_inv_lref_pair_sn: ∀L1,L2,i. L1 ≛[#i] L2 → ∀I,K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I]V1 →
- ∃∃K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I]V2 & K1 ≛[V1] K2 & V1 ≛ V2.
-/2 width=3 by rex_inv_lref_pair_sn/ qed-.
-
-lemma reqx_inv_lref_pair_dx: ∀L1,L2,i. L1 ≛[#i] L2 → ∀I,K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I]V2 →
- ∃∃K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I]V1 & K1 ≛[V1] K2 & V1 ≛ V2.
-/2 width=3 by rex_inv_lref_pair_dx/ qed-.
-
-lemma reqx_inv_lref_pair_bi (L1) (L2) (i):
- L1 ≛[#i] L2 →
- ∀I1,K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I1]V1 →
- ∀I2,K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I2]V2 →
- ∧∧ K1 ≛[V1] K2 & V1 ≛ V2 & I1 = I2.
-/2 width=6 by rex_inv_lref_pair_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/static/rex_fqup.ma".
-include "static_2/static/reqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-
-(* Advanced properties ******************************************************)
-
-lemma reqx_refl: ∀T. reflexive … (reqx T).
-/2 width=1 by rex_refl/ qed.
-
-lemma reqx_pair_refl: ∀V1,V2. V1 ≛ V2 →
- ∀I,L. ∀T:term. L.ⓑ[I]V1 ≛[T] L.ⓑ[I]V2.
-/2 width=1 by rex_pair_refl/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma reqx_inv_bind_void: ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 →
- L1 ≛[V] L2 ∧ L1.ⓧ ≛[T] L2.ⓧ.
-/2 width=3 by rex_inv_bind_void/ qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma reqx_fwd_bind_dx_void: ∀p,I,L1,L2,V,T.
- L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓧ ≛[T] L2.ⓧ.
-/2 width=4 by rex_fwd_bind_dx_void/ 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/s_computation/fqus_fqup.ma".
-include "static_2/static/reqx_drops.ma".
-include "static_2/static/reqx_fqup.ma".
-include "static_2/static/reqx_reqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-
-(* Properties with extended structural successor for closures ***************)
-
-lemma fqu_teqx_conf (b):
- ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
- ∀U2. U1 ≛ U2 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2.
-#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
-[ #I #G #L #W #X #H >(teqx_inv_lref1 … H) -X
- /2 width=5 by fqu_lref_O, ex3_2_intro/
-| #I #G #L #W1 #U1 #X #H
- elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct
- /2 width=5 by fqu_pair_sn, ex3_2_intro/
-| #p #I #G #L #W1 #U1 #Hb #X #H
- elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
- /3 width=5 by reqx_pair_refl, fqu_bind_dx, ex3_2_intro/
-| #p #I #G #L #W1 #U1 #Hb #X #H
- elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
- /3 width=5 by fqu_clear, ex3_2_intro/
-| #I #G #L #W1 #U1 #X #H
- elim (teqx_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
- /2 width=5 by fqu_flat_dx, ex3_2_intro/
-| #I #G #L #T1 #U1 #HTU1 #U2 #HU12
- elim (teqx_inv_lifts_sn … HU12 … HTU1) -U1
- /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma teqx_fqu_trans (b):
- ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
-#b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
-elim (fqu_teqx_conf … H12 U2) -H12
-/3 width=5 by reqx_sym, teqx_sym, ex3_2_intro/
-qed-.
-
-(* Basic_2A1: uses: lleq_fqu_trans *)
-lemma reqx_fqu_trans (b):
- ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
-#b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
-[ #I #G #L2 #V2 #L1 #H elim (reqx_inv_zero_pair_dx … H) -H
- #K1 #V1 #HV1 #HV12 #H destruct
- /3 width=7 by teqx_reqx_conf_sn, fqu_lref_O, ex3_2_intro/
-| * [ #p ] #I #G #L2 #V #T #L1 #H
- [ elim (reqx_inv_bind … H)
- | elim (reqx_inv_flat … H)
- ] -H
- /2 width=5 by fqu_pair_sn, ex3_2_intro/
-| #p #I #G #L2 #V #T #Hb #L1 #H elim (reqx_inv_bind … H) -H
- /3 width=5 by fqu_bind_dx, ex3_2_intro/
-| #p #I #G #L2 #V #T #Hb #L1 #H elim (reqx_inv_bind_void … H) -H
- /3 width=5 by fqu_clear, ex3_2_intro/
-| #I #G #L2 #V #T #L1 #H elim (reqx_inv_flat … H) -H
- /2 width=5 by fqu_flat_dx, ex3_2_intro/
-| #I #G #L2 #T #U #HTU #Y #HU
- elim (reqx_fwd_dx … HU) #L1 #V1 #H destruct
- /5 width=14 by reqx_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
-]
-qed-.
-
-(* Properties with optional structural successor for closures ***************)
-
-lemma teqx_fquq_trans (b):
- ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
-#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H
-[ #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1
- /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was just: lleq_fquq_trans *)
-lemma reqx_fquq_trans (b):
- ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
-#b #G1 #G2 #L2 #K2 #T #U #H elim H -H
-[ #H #L1 #HL12 elim (reqx_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-(* Properties with plus-iterated structural successor for closures **********)
-
-(* Basic_2A1: was just: lleq_fqup_trans *)
-lemma reqx_fqup_trans (b):
- ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
-#b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
-[ #G2 #K2 #U #HTU #L1 #HL12 elim (reqx_fqu_trans … HTU … HL12) -L2
- /3 width=5 by fqu_fqup, ex3_2_intro/
-| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12
- elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0
- elim (reqx_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
- elim (teqx_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
- @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
- /3 width=5 by reqx_trans, teqx_reqx_conf_sn, fqup_strap1, teqx_trans/
-]
-qed-.
-
-lemma teqx_fqup_trans (b):
- ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
-#b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1
-[ #G1 #L1 #U1 #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1
- /3 width=5 by fqu_fqup, ex3_2_intro/
-| #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21
- elim (teqx_fqu_trans … H … HU21) -U1 #L0 #T #H1 #HTU #HL0
- lapply (teqx_reqx_div … HTU … HL0) -HL0 #HL0
- elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2
- elim (reqx_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2
- lapply (teqx_reqx_conf_sn … HUT1 … HK2) -HK2 #HK2
- /3 width=7 by reqx_trans, fqup_strap2, teqx_trans, ex3_2_intro/
-]
-qed-.
-
-(* Properties with star-iterated structural successor for closures **********)
-
-lemma teqx_fqus_trans (b):
- ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
-#b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H
-[ #H elim (teqx_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/
-| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was just: lleq_fqus_trans *)
-lemma reqx_fqus_trans (b):
- ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
-#b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
-[ #H elim (reqx_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
-| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/relocation/lifts_teqx.ma".
-include "static_2/static/rex_length.ma".
-include "static_2/static/rex_fsle.ma".
-include "static_2/static/reqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-
-(* Advanved properties with free variables inclusion ************************)
-
-lemma reqx_fsge_comp: rex_fsge_compatible cdeq.
-#L1 #L2 #T * #f1 #Hf1 #HL12
-lapply (frees_reqx_conf … Hf1 … HL12)
-lapply (sex_fwd_length … HL12)
-/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
-qed-.
-
-(* Properties with length for local environments ****************************)
-
-(* Basic_2A1: uses: lleq_sort *)
-lemma reqx_sort_length: ∀L1,L2. |L1| = |L2| → ∀s. L1 ≛[⋆s] L2.
-/2 width=1 by rex_sort_length/ qed.
-
-(* Basic_2A1: uses: lleq_gref *)
-lemma reqx_gref_length: ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[§l] L2.
-/2 width=1 by rex_gref_length/ qed.
-
-lemma reqx_unit_length: ∀L1,L2. |L1| = |L2| →
- ∀I. L1.ⓤ[I] ≛[#0] L2.ⓤ[I].
-/2 width=1 by rex_unit_length/ qed.
-
-(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)
-lemma reqx_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[T] K2 →
- ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 →
- ∀U. ⇧*[f] T ≘ U → L1 ≛[U] L2.
-/3 width=9 by rex_lifts_bi, teqx_lifts_sn/ qed-.
-
-(* Forward lemmas with length for local environments ************************)
-
-(* Basic_2A1: lleq_fwd_length *)
-lemma reqx_fwd_length: ∀L1,L2. ∀T:term. L1 ≛[T] L2 → |L1| = |L2|.
-/2 width=3 by rex_fwd_length/ qed-.
include "static_2/static/feqg.ma".
(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-(*
-definition feqx: relation6 genv lenv term genv lenv term ≝
- feqg sfull.
-*)
+
interpretation
"sort-irrelevant equivalence on referred entries (closure)"
'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqg sfull G1 L1 T1 G2 L2 T2).
projects / helm.git / commitdiff