(* *)
(**************************************************************************)
-include "basic_2/syntax/ext2_tc.ma".
-include "basic_2/relocation/lexs_tc.ma".
-include "basic_2/relocation/lex.ma".
+include "basic_2/relocation/lex_tc.ma".
include "basic_2/static/lfeq_fqup.ma".
include "basic_2/static/lfeq_lfeq.ma".
include "basic_2/i_static/tc_lfxs_fqup.ma".
(* Inversion lemmas with generic extension of a context sensitive relation **)
+(* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *)
lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
lexs_frees_confluent (cext2 R) cfull →
- s_rs_transitive_isid cfull (cext2 R) →
+ s_rs_transitive … R (λ_.lex R) →
lfeq_transitive R →
∀L1,L2,T. L1 ⪤**[R, T] L2 →
∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2.
#R #H1R #H2R #H3R #H4R #L1 #L2 #T #H
+lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R
@(tc_lfxs_ind_sn … H1R … H) -H -L2
[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/
| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
include "basic_2/syntax/cext2.ma".
include "basic_2/relocation/lexs.ma".
-(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************)
+(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
definition lex: (lenv → relation term) → relation lenv ≝
(* Basic properties *********************************************************)
+lemma lex_bind: ∀R,I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 →
+ K1.ⓘ{I1} ⪤[R] K2.ⓘ{I2}.
+#R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12
+/3 width=3 by lexs_push, isid_push, ex2_intro/
+qed.
+
(* Basic_2A1: was: lpx_sn_refl *)
lemma lex_refl: ∀R. c_reflexive … R → reflexive … (lex R).
/4 width=3 by lexs_refl, ext2_refl, ex2_intro/ qed.
+(* Advanced properties ******************************************************)
+
+lemma lex_bind_refl_dx: ∀R. c_reflexive … R →
+ ∀I,K1,K2. K1 ⪤[R] K2 → K1.ⓘ{I} ⪤[R] K2.ⓘ{I}.
+/3 width=3 by ext2_refl, lex_bind/ qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_2A1: was: lpx_sn_inv_atom1: *)
#R #L2 * #f #Hf #H >(lexs_inv_atom1 … H) -L2 //
qed-.
-(* Basic_2A1: was: lpx_sn_inv_pair1 *)
-lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 →
- ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
-#R #I #L2 #K1 #V1 * #f #Hf #H
+lemma lex_inv_bind_sn: ∀R,I1,L2,K1. K1.ⓘ{I1} ⪤[R] L2 →
+ ∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ{I2}.
+#R #I1 #L2 #K1 * #f #Hf #H
lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
-elim (lexs_inv_push1 … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct
-elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct
-/3 width=5 by ex3_2_intro, ex2_intro/
+elim (lexs_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+/3 width=5 by ex2_intro, ex3_2_intro/
qed-.
(* Basic_2A1: was: lpx_sn_inv_atom2 *)
#R #L1 * #f #Hf #H >(lexs_inv_atom2 … H) -L1 //
qed-.
-(* Basic_2A1: was: lpx_sn_inv_pair2 *)
-lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 →
- ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
-#R #I #L1 #K2 #V2 * #f #Hf #H
+lemma lex_inv_bind_dx: ∀R,I2,L1,K2. L1 ⪤[R] K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ{I1}.
+#R #I2 #L1 #K2 * #f #Hf #H
lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
-elim (lexs_inv_push2 … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct
-elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct
+elim (lexs_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct
/3 width=5 by ex3_2_intro, ex2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
+(* Basic_2A1: was: lpx_sn_inv_pair1 *)
+lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 →
+ ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+#R #I #L2 #K1 #V1 #H
+elim (lex_inv_bind_sn … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct
+elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+(* Basic_2A1: was: lpx_sn_inv_pair2 *)
+lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #I #L1 #K2 #V2 #H
+elim (lex_inv_bind_dx … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct
+elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
(* Basic_2A1: was: lpx_sn_inv_pair *)
lemma lex_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
L1.ⓑ{I1}V1 ⪤[R] L2.ⓑ{I2}V2 →
--- /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/syntax/ext2_tc.ma".
+include "basic_2/relocation/lexs_tc.ma".
+include "basic_2/relocation/lex.ma".
+
+(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
+
+(* Inversion lemmas with transitive closure *********************************)
+
+lemma s_rs_transitive_lex_inv_isid: ∀R. s_rs_transitive … R (λ_.lex R) →
+ s_rs_transitive_isid cfull (cext2 R).
+#R #HR #f #Hf #L2 #T1 #T2 #H #L1 #HL12
+elim (ext2_tc … H) -H
+[ /3 width=1 by ext2_inv_tc, ext2_unit/
+| #I #V1 #V2 #HV12
+ @ext2_inv_tc @ext2_pair
+ @(HR … HV12) -HV12 /2 width=3 by ex2_intro/ (**) (* auto fails *)
+]
+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.ma".
+include "basic_2/rt_computation/cpxs_drops.ma".
+include "basic_2/rt_computation/cpxs_cpxs.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+
+(* Properties with uncounted parallel rt-transition for local environments **)
+
+lemma lpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpx h G).
+#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2
+[ /2 width=3 by/
+| /3 width=2 by cpx_cpxs, cpx_ess/
+| #I #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
+ elim (lpx_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
+ /4 width=3 by cpxs_delta, cpxs_strap2/
+| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
+ elim (lpx_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct
+ /4 width=3 by cpxs_lref, cpxs_strap2/
+|5,10: /4 width=1 by cpxs_beta, cpxs_bind, lpx_bind_refl_dx/
+|6,8,9: /3 width=1 by cpxs_flat, cpxs_ee, cpxs_eps/
+| /4 width=3 by cpxs_zeta, lpx_bind_refl_dx/
+| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_bind_refl_dx/
+]
+qed-.
+
+lemma lpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpx h G).
+#h #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
+qed-.
(**************************************************************************)
include "basic_2/i_static/tc_lfxs_lex.ma".
-include "basic_2/rt_transition/lfpx_frees.ma".
+include "basic_2/rt_transition/cpx_lfeq.ma".
+include "basic_2/rt_computation/cpxs_lpx.ma".
include "basic_2/rt_computation/lpxs.ma".
include "basic_2/rt_computation/lfpxs.ma".
(* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
-lemma lpx_cpxs_ext_trans: ∀h,G. s_rs_transitive_isid cfull (cpx_ext h G).
-#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10
-
-
lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
-#h #G @tc_lfxs_inv_lex_lfeq //
-[ @lfpx_frees_conf
-| @lpx_cpxs_ext_trans
\ No newline at end of file
+/3 width=5 by lfpx_frees_conf, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lpxs.ma
-lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
+lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lfeq.ma".
+include "basic_2/rt_transition/cpx_lfxs.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Properties with syntactic equivalence for lenvs on referred entries ******)
+
+(* Basic_2A1: was: lleq_cpx_trans *)
+lemma lfeq_cpx_trans: ∀h,G. lfeq_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 (lfeq_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 (lfeq_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 (lfeq_inv_bind … H) -H /3 width=1 by cpx_bind/
+| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H
+ elim (lfeq_inv_flat … H) -H /3 width=1 by cpx_flat/
+| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IH #L1 #H
+ elim (lfeq_inv_bind … H) -H /3 width=3 by cpx_zeta/
+| #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H
+ elim (lfeq_inv_flat … H) -H /3 width=1 by cpx_eps/
+| #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H
+ elim (lfeq_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 (lfeq_inv_flat … H) -H #HV1 #H
+ elim (lfeq_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 (lfeq_inv_flat … H) -H #HV1 #H
+ elim (lfeq_inv_bind … H) -H /3 width=3 by cpx_theta/
+]
+qed-.
+(*
+(* Basic_2A1: was: cpx_lleq_conf *)
+lemma cpx_lfeq_conf: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L1. L2 ≡[T1] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h] T2.
+/3 width=3 by lfeq_cpx_trans, lfeq_sym/ qed-.
+*)
+(* Basic_2A1: was: cpx_lleq_conf_sn *)
+lemma cpx_lfeq_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) lfeq.
+/2 width=5 by cpx_lfxs_conf/ qed-.
+(*
+(* Basic_2A1: was: cpx_lleq_conf_dx *)
+lemma cpx_lfeq_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2.
+/4 width=6 by cpx_lfeq_conf_sn, lfeq_sym/ qed-.
+*)
\ No newline at end of file
include "basic_2/notation/relations/predtysn_4.ma".
include "basic_2/relocation/lex.ma".
-include "basic_2/rt_transition/cpx.ma".
+include "basic_2/rt_transition/cpx_ext.ma".
(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ******************)
(* Basic properties *********************************************************)
+lemma lpx_bind: ∀h,G,K1,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 →
+ ∀I1,I2. ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 → ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈[h] K2.ⓘ{I2}.
+/2 width=1 by lex_bind/ qed.
+
+lemma lpx_refl: ∀h,G. reflexive … (lpx h G).
+/2 width=1 by lex_refl/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma lpx_bind_refl_dx: ∀h,G,K1,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 →
+ ∀I. ⦃G, K1.ⓘ{I}⦄ ⊢ ⬈[h] K2.ⓘ{I}.
+/2 width=1 by lex_bind_refl_dx/ qed.
(*
lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 →
⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2.
/2 width=1 by lpx_sn_pair/ qed.
*)
-
-lemma lpx_refl: ∀h,G. reflexive … (lpx h G).
-/2 width=1 by lex_refl/ qed.
-
(* Basic inversion lemmas ***************************************************)
(* Basic_2A1: was: lpx_inv_atom1 *)
lemma lpx_inv_atom_sn: ∀h,G,L2. ⦃G, ⋆⦄ ⊢ ⬈[h] L2 → L2 = ⋆.
/2 width=2 by lex_inv_atom_sn/ qed-.
+lemma lpx_inv_bind_sn: ∀h,I1,G,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈[h] L2 →
+ ∃∃I2,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 &
+ L2 = K2.ⓘ{I2}.
+/2 width=1 by lex_inv_bind_sn/ qed-.
+
+(* Basic_2A1: was: lpx_inv_atom2 *)
+lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆.
+/2 width=2 by lex_inv_atom_dx/ qed-.
+
+lemma lpx_inv_bind_dx: ∀h,I2,G,L1,K2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓘ{I2} →
+ ∃∃I1,K1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 &
+ L1 = K1.ⓘ{I1}.
+/2 width=1 by lex_inv_bind_dx/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
(* Basic_2A1: was: lpx_inv_pair1 *)
lemma lpx_inv_pair_sn: ∀h,I,G,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] L2 →
∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 &
L2 = K2.ⓑ{I}V2.
/2 width=1 by lex_inv_pair_sn/ qed-.
-(* Basic_2A1: was: lpx_inv_atom2 *)
-lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆.
-/2 width=2 by lex_inv_atom_dx/ qed-.
-
(* Basic_2A1: was: lpx_inv_pair2 *)
-lemma lpx_inv_pair2_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 &
- L1 = K1.ⓑ{I}V1.
+lemma lpx_inv_pair_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 &
+ L1 = K1.ⓑ{I}V1.
/2 width=1 by lex_inv_pair_dx/ qed-.
-(* Advanced inversion lemmas ************************************************)
-
lemma lpx_inv_pair: ∀h,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ⬈[h] L2.ⓑ{I2}V2 →
∧∧ ⦃G, L1⦄ ⊢ ⬈[h] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & I1 = I2.
/2 width=1 by lex_inv_pair/ qed-.
lemma lfeq_transitive_inv_lfxs: ∀R. lfeq_transitive R → lfxs_transitive ceq R R.
/2 width=3 by/ qed-.
+lemma lfeq_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 lfxs_inv_bind/ qed-.
+
+lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 →
+ ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
+/2 width=2 by lfxs_inv_flat/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lfeq_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 (lfxs_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lfeq_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 (lfxs_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≡[#⫯i] L2 →
+ ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ{I2}.
+/2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
+
+lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ{I1}.
+/2 width=2 by lfxs_inv_lref_bind_dx/ qed-.
+
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: was: llpx_sn_lrefl *)
[ [ "strongly normalizing for lenvs on referred entries" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ [ "strongly normalizing for terms" ] "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
- [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
+ [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
[ [ "for lenvs on all entries" ] "lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )" * ]
- [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
[ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ]
[ [ "for lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
[ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
- [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
+ [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfeq" * ]
}
]
[ { "counted context-sensitive parallel rt-transition" * } {
]
class "orange"
[ { "relocation" * } {
- [ { "generic slicing for local environments" * } {
- [ [ "" ] "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
- [ [ "" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+ [ { "generic slicing" * } {
+ [ [ "for lenvs" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
}
]
[ { "generic relocation" * } {
- [ [ "" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
- [ [ "" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
- [ [ "" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
+ [ [ "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_lifts" * ]
}
]
- [ { "ranged equivalence for local environments" * } {
- [ [ "" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+ [ { "syntactic equivalence" * } {
+ [ [ "for lenvs on selected entries" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
}
]
[ { "generic entrywise extension" * } {
- [ [ "" ] "lex ( ? ⦻[?] ? )" * ]
- [ [ "" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
+ [ [ "for lenvs of one contex-sensitive relation" ] "lex ( ? ⦻[?] ? )" "lex_tc" * ]
+ [ [ "for lenvs of two contex-sensitive relations" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
}
]
}
projects / helm.git / commitdiff