--- /dev/null
+(* 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
+*)
--- /dev/null
+(* req_req is missing, with req_sym *)
+
+(* Basic_2A1: was: cpx_lleq_conf *)
+lemma cpx_req_conf (h) (G):
+ ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L1. L2 ≡[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
+/3 width=3 by req_cpx_trans, req_sym/ qed-.
+
+(* Basic_2A1: was: cpx_lleq_conf_dx *)
+lemma cpx_req_conf_dx (h) (G):
+ ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2.
+/4 width=6 by cpx_req_conf_sn, req_sym/ qed-.
--- /dev/null
+lapply (nta_ntas … H) -H #H
+elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
+[ elim (eq_or_gt n) #H destruct
+ [ <minus_n_O in HU; #HU -Hn
+ /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
+ | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
+ <minus_n_n in HU; #HU
+ @or_intror
+ @(ex6_5_intro … Ha … HUX HX) -Ha -X
+ [2,4: /2 width=2 by ntas_inv_nta/
+ |6: @ntas_refl
∨∨ ∃∃p,W,U,U0. ad a 0 & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 & ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a]
| ∃∃n,p,W,U,U0. ad a (↑n) & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :[h,a] U & ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a].
#h #a #G #L #V #T #X #H
-(*
-lapply (nta_ntas … H) -H #H
-elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
-[ elim (eq_or_gt n) #H destruct
- [ <minus_n_O in HU; #HU -Hn
- /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
- | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
- <minus_n_n in HU; #HU
- @or_intror
- @(ex6_5_intro … Ha … HUX HX) -Ha -X
- [2,4: /2 width=2 by ntas_inv_nta/
- |6: @ntas_refl
-*)
+(* Note: insert here: alternate proof in ntas_nta.etc *)
elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
elim (eq_or_gt n) #Hn destruct
(* 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):
--- /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/teqo_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 teqo_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 teqo_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 teqo_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_teqo/ 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/teqo_simple_vector.ma".
+include "static_2/relocation/lifts_vector.ma".
+include "basic_2/rt_computation/cpxs_teqo.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 teqo_pair/
+| #p #W1 #T1 #HT1 #HU
+ lapply (IHVs … HT1) -IHVs -HT1 #HT1
+ elim (teqo_inv_applv_bind_simple … HT1) //
+| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ lapply (IHVs … HT1) -IHVs -HT1 #HT1
+ elim (teqo_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 teqo_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (teqo_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 (teqo_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 teqo_pair, or_introl/
+| #q #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (teqo_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 (teqo_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 teqo_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+ elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
+ [ -HV12a -HV12b -HU
+ elim (teqo_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 (teqo_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 teqo_pair, or3_intro0/
+| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (teqo_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 (teqo_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 teqo_pair/
+| #p #W0 #T0 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (teqo_inv_applv_bind_simple … HT0) //
+| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (teqo_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_toeq_vector.ma".
-include "basic_2/rt_computation/csx_simple_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo_vector.ma".
+include "basic_2/rt_computation/csx_simple_teqo.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".
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
- @csx_appl_simple_toeq /2 width=1 by applv_simple/ -IHV -HV -HVs
+ @csx_appl_simple_teqo /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 //
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cpxs_toeq_vector.ma".
-include "basic_2/rt_computation/csx_simple_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo_vector.ma".
+include "basic_2/rt_computation/csx_simple_teqo.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_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
+@csx_appl_simple_teqo /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_toeq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
+ @csx_appl_simple_teqo /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_toeq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
+@csx_appl_simple_teqo /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_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T
+@csx_appl_simple_teqo /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/teqo_simple.ma".
+include "static_2/syntax/teqo_teqo.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_teqo (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 (teqo_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, teqo_canc_sn, simple_teqo_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.
(* Properties with syntactic equivalence for lenvs on referred entries ******)
(* Basic_2A1: was: lleq_cpx_trans *)
-lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G).
+lemma req_cpx_trans (h) (G): req_transitive (cpx h G).
#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_ess/
[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct
elim (req_inv_bind … H) -H /3 width=3 by cpx_theta/
]
qed-.
-(*
-(* Basic_2A1: was: cpx_lleq_conf *)
-lemma cpx_req_conf: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
- ∀L1. L2 ≘[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
-/3 width=3 by req_cpx_trans, req_sym/ qed-.
-*)
+
(* Basic_2A1: was: cpx_lleq_conf_sn *)
-lemma cpx_req_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) req.
+lemma cpx_req_conf_sn (h) (G): s_r_confluent1 … (cpx h G) req.
/2 width=5 by cpx_rex_conf/ qed-.
-(*
-(* Basic_2A1: was: cpx_lleq_conf_dx *)
-lemma cpx_req_conf_dx: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
- ∀L1. L1 ≘[T1] L2 → L1 ≘[T2] L2.
-/4 width=6 by cpx_req_conf_sn, req_sym/ qed-.
-*)
[ [ "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_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" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_teqo" + "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_toeq" + "cpxs_toeq_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_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
--- /dev/null
+#!/bin/sh
+for SRC in `find ground_2 static_2 basic_2 apps_2 -name "*.ma"`; do
+ if [ ! -e ${SRC//$1/$2} ];
+ then echo ${SRC//$1/$2}; git mv $SRC ${SRC//$1/$2};
+ fi
+done
+
+unset SRC
--- /dev/null
+lemma frees_sort_pushs:
+ ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
+ ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
+#f #K #s #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
+]
+qed.
+
+lemma frees_gref_pushs:
+ ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
+ ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
+#f #K #l #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
+]
+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/teqo.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with sort-irrelevant outer equivalence for terms **************)
+
+lemma teqo_lifts_sn: liftable2_sn teqo.
+#T1 #T2 #H elim H -T1 -T2 [||| * ]
+[ #s1 #s2 #f #X #H
+ >(lifts_inv_sort1 … H) -H
+ /2 width=3 by teqo_sort, ex2_intro/
+| #i #f #X #H
+ elim (lifts_inv_lref1 … H) -H #j #Hj #H destruct
+ /3 width=3 by teqo_lref, lifts_lref, ex2_intro/
+| #l #f #X #H
+ >(lifts_inv_gref1 … H) -H
+ /2 width=3 by teqo_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 teqo_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 teqo_pair, lifts_flat, ex2_intro/
+]
+qed-.
+
+lemma teqo_lifts_dx: liftable2_dx teqo.
+/3 width=3 by teqo_lifts_sn, liftable2_sn_dx, teqo_sym/ qed-.
+
+lemma teqo_lifts_bi: liftable2_bi teqo.
+/3 width=6 by teqo_lifts_sn, liftable2_sn_bi/ qed-.
+
+(* Inversion lemmas with sort-irrelevant outer equivalence for terms ********)
+
+lemma teqo_inv_lifts_bi: deliftable2_bi teqo.
+#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 teqo_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 teqo_lref/
+| #l #f #X1 #H1 #X2 #H2
+ >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
+ /1 width=1 by teqo_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 teqo_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 teqo_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-.
#J #L #HLK #H destruct /3 width=1 by frees_lref/
]
qed.
-(*
-lemma frees_sort_pushs:
- ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
- ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
-#f #K #s #Hf #i elim i -i
-[ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
-]
-qed.
-*)
+
lemma frees_lref_pushs:
∀f,K,j. K ⊢ 𝐅+⦃#j⦄ ≘ f →
∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃#(i+j)⦄ ≘ ⫯*[i] f.
#I #Y #HYK #H destruct /3 width=1 by frees_lref/
]
qed.
-(*
-lemma frees_gref_pushs:
- ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
- ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
-#f #K #l #Hf #i elim i -i
-[ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
-]
-qed.
-*)
+
(* Advanced inversion lemmas ************************************************)
lemma frees_inv_lref_drops:
lemma rdeq_pair: ∀I,L1,L2,V1,V2.
L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ{I}V1 ≛[#0] L2.ⓑ{I}V2.
/2 width=1 by rex_pair/ qed.
-(*
-lemma rdeq_unit: â\88\80f,I,L1,L2. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L1 ⪤[cdeq_ext,cfull,f] L2 →
+
+lemma rdeq_unit: â\88\80f,I,L1,L2. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L1 â\89\9b[f] L2 →
L1.ⓤ{I} ≛[#0] L2.ⓤ{I}.
/2 width=3 by rex_unit/ qed.
-*)
+
lemma rdeq_lref: ∀I1,I2,L1,L2,i.
L1 ≛[#i] L2 → L1.ⓘ{I1} ≛[#↑i] L2.ⓘ{I2}.
/2 width=1 by rex_lref/ qed.
lemma rdeq_inv_atom_dx: ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆.
/2 width=3 by rex_inv_atom_dx/ qed-.
-(*
-lemma rdeq_inv_zero: ∀Y1,Y2. Y1 ≛[#0] Y2 →
- ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
- | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
- | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤[cdeq_ext h o,cfull,f] L2 &
- Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+
+lemma rdeq_inv_zero:
+ ∀Y1,Y2. Y1 ≛[#0] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ≛[f] L2 & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
#Y1 #Y2 #H elim (rex_inv_zero … H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.
-*)
+
lemma rdeq_inv_lref: ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 →
∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
| ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 &
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "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 teqo: relation term ≝
+| teqo_sort: ∀s1,s2. teqo (⋆s1) (⋆s2)
+| teqo_lref: ∀i. teqo (#i) (#i)
+| teqo_gref: ∀l. teqo (§l) (§l)
+| teqo_pair: ∀I,V1,V2,T1,T2. teqo (②{I}V1.T1) (②{I}V2.T2)
+.
+
+interpretation
+ "sort-irrelevant outer equivalence (term)"
+ 'TopIso T1 T2 = (teqo T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact teqo_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 teqo_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
+ ∃s2. Y = ⋆s2.
+/2 width=4 by teqo_inv_sort1_aux/ qed-.
+
+fact teqo_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 teqo_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
+/2 width=5 by teqo_inv_lref1_aux/ qed-.
+
+fact teqo_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 teqo_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
+/2 width=5 by teqo_inv_gref1_aux/ qed-.
+
+fact teqo_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 teqo_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 →
+ ∃∃W2,U2. T2 = ②{J}W2. U2.
+/2 width=7 by teqo_inv_pair1_aux/ qed-.
+
+fact teqo_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 teqo_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
+ ∃∃W1,U1. T1 = ②{J}W1.U1.
+/2 width=7 by teqo_inv_pair2_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma teqo_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
+ I1 = I2.
+#I1 #I2 #V1 #V2 #T1 #T2 #H elim (teqo_inv_pair1 … H) -H
+#V0 #T0 #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+(* Basic_2A1: was: tsts_refl *)
+lemma teqo_refl: reflexive … teqo.
+* //
+* /2 width=1 by teqo_lref, teqo_gref/
+qed.
+
+(* Basic_2A1: was: tsts_sym *)
+lemma teqo_sym: symmetric … teqo.
+#T1 #T2 * -T1 -T2 /2 width=3 by teqo_sort/
+qed-.
+
+(* Basic_2A1: was: tsts_dec *)
+lemma teqo_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
+* [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
+[ /3 width=1 by teqo_sort, or_introl/
+|2,3,13:
+ @or_intror #H
+ elim (teqo_inv_sort1 … H) -H #x #H destruct
+|4,6,14:
+ @or_intror #H
+ lapply (teqo_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 (teqo_inv_lref1 … H) -H #H destruct /2 width=1 by/
+|7,8,15:
+ @or_intror #H
+ lapply (teqo_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 (teqo_inv_gref1 … H) -H #H destruct /2 width=1 by/
+|10,11,12:
+ @or_intror #H
+ elim (teqo_inv_pair1 … H) -H #X1 #X2 #H destruct
+|16:
+ elim (eq_item2_dec I1 I2) #HI12 destruct
+ [ /3 width=1 by teqo_pair, or_introl/ ]
+ @or_intror #H
+ lapply (teqo_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/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properies with simple (neutral) terms ************************************)
+
+(* Basic_2A1: was: simple_tsts_repl_dx *)
+lemma simple_teqo_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_teqo_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+/3 width=3 by simple_teqo_repl_dx, teqo_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/teqo_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 teqo_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 (teqo_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/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properties with sort-irrelevant equivalence for terms ********************)
+
+lemma tdeq_teqo: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
+#T1 #T2 * -T1 -T2 /2 width=1 by teqo_sort, teqo_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/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: iso_trans *)
+(* Basic_2A1: was: tsts_trans *)
+theorem teqo_trans: Transitive … teqo.
+#T1 #T * -T1 -T
+[ #s1 #s #X #H
+ elim (teqo_inv_sort1 … H) -s /2 width=1 by teqo_sort/
+| #i1 #i #H <(teqo_inv_lref1 … H) -H //
+| #l1 #l #H <(teqo_inv_gref1 … H) -H //
+| #I #V1 #V #T1 #T #X #H
+ elim (teqo_inv_pair1 … H) -H #V2 #T2 #H destruct //
+]
+qed-.
+
+(* Basic_2A1: was: tsts_canc_sn *)
+theorem teqo_canc_sn: left_cancellable … teqo.
+/3 width=3 by teqo_trans, teqo_sym/ qed-.
+
+(* Basic_2A1: was: tsts_canc_dx *)
+theorem teqo_canc_dx: right_cancellable … teqo.
+/3 width=3 by teqo_trans, teqo_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-.
[ { "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_tweq" + "lifts_toeq" + "lifts_lifts" * ]
+ [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_teqo" + "lifts_lifts" * ]
}
]
[ { "syntactic equivalence" * } {
}
]
[ { "sort-irrelevant outer equivalence" * } {
- [ [ "for terms" ] "toeq" + "( ? ⩳ ? )" "toeq_simple" + "toeq_tdeq" + "toeq_toeq" + "toeq_simple_vector" * ]
+ [ [ "for terms" ] "teqo" + "( ? ⩳ ? )" "teqo_simple" + "teqo_tdeq" + "teqo_teqo" + "teqo_simple_vector" * ]
}
]
[ { "sort-irrelevant whd equivalence" * } {
projects / helm.git / commitdiff