(**************************************************************************)
include "basic_2/relocation/lex_tc.ma".
+include "basic_2/static/lfxs_fsle.ma".
include "basic_2/static/lfeq_fqup.ma".
include "basic_2/static/lfeq_lfeq.ma".
include "basic_2/i_static/tc_lfxs_fqup.ma".
(* *)
(**************************************************************************)
-include "basic_2/static/lfxs_lfxs.ma".
+include "basic_2/static/lfxs_fsle.ma".
include "basic_2/i_static/tc_lfxs.ma".
(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
--- /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/relocation/lexs_length.ma".
+include "basic_2/relocation/lex.ma".
+
+(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
+
+(* Forward lemmas with length for local environments ************************)
+
+(* Basic_2A1: was: lpx_sn_fwd_length *)
+lemma lex_fwd_length: ∀R,L1,L2. L1 ⪤[R] L2 → |L1| = |L2|.
+#R #L1 #L2 * /2 width=4 by lexs_fwd_length/
+qed-.
(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_id.ma".
include "basic_2/syntax/ext2_tc.ma".
include "basic_2/relocation/lexs_tc.ma".
include "basic_2/relocation/lex.ma".
(* Forward lemmas with length for local environments ************************)
-(* Basic_2A1: uses: lpx_sn_fwd_length *)
lemma lexs_fwd_length: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → |L1| = |L2|.
-#RM #RP #f #L1 #L2 #H elim H -f -L1 -L2 //
+#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2 //
#f #I1 #I2 #L1 #L2 >length_bind >length_bind //
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/syntax/cext2.ma".
+include "basic_2/rt_computation/cpxs.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR BINDERS **********)
+
+definition cpxs_ext (h) (G): relation3 lenv bind bind ≝
+ cext2 (cpxs h G).
+
+interpretation
+ "uncounted context-sensitive parallel rt-computation (binder)"
+ 'PRedTyStar h G L I1 I2 = (cpxs_ext h G L I1 I2).
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lfpx_fqup.ma".
-include "basic_2/rt_transition/lfpx_cpx.ma".
+include "basic_2/rt_transition/lfpx_fsle.ma".
include "basic_2/rt_computation/cpxs_drops.ma".
include "basic_2/rt_computation/cpxs_cpxs.ma".
(* *)
(**************************************************************************)
-include "basic_2/syntax/tdeq_tdeq.ma".
-include "basic_2/rt_transition/lfpx_fqup.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/cpxs.ma".
(* *)
(**************************************************************************)
-include "basic_2/syntax/tdeq_tdeq.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/csx_drops.ma".
+++ /dev/null
-
-include "basic_2/static/lfxs_lex.ma".
-include "basic_2/rt_transition/cpx_etc.ma".
-include "basic_2/rt_computation/lfpxs_lpxs.ma".
-
-lemma R_fle_comp_LTC: ∀R. R_fle_compatible R → R_fle_compatible (LTC … R).
-#R #HR #L #T1 #T2 #H elim H -T2
-/3 width=3 by fle_trans_dx/
-qed-.
-
-lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
-#h #G #L1 #T1 #T2 #HT12 #L2 #H
-elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
-lapply (lfxs_lex … HL1 T1) #H
-elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_
-@(lfpxs_lpxs_lfeq … HL1) -HL1
-@(fle_lfxs_trans … HL2) //
-qed-.
+++ /dev/null
-
-include "basic_2/static/lfxs_lex.ma".
-include "basic_2/rt_transition/cpx_etc.ma".
-include "basic_2/rt_computation/lfpxs_lpxs.ma".
-
-axiom fle_trans: ∀L1,L,T1,T. ⦃L1, T1⦄ ⊆ ⦃L, T⦄ →
- ∀L2,T2. ⦃L, T⦄ ⊆ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄.
-
-axiom pippo: ∀h,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → ∀L. ⦃G, L1⦄ ⊢⬈[h] L →
- ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄.
-(*
-lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
- ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄.
-#h #G #L1 #L #H
-lapply (lex_inv_ltc … H) -H // #H
-@(TC_star_ind ???????? H) -L //
-[ #T1 #T2 #H elim (pippo … H) -H /2 width=3 by conj/
-| #L #L0 #HL1 #HL0 #IH #T1 #T2 #HT12
- elim (IH … HT12) -IH #HT1 #HT21
- elim (pippo … T1 T1 … HL0) // #H1 #_ #_
- @conj
- [ @(fle_trans … H1) //
-
-*)(*
-lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
- ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄.
-#h #G #L1 #L #H
-lapply (lex_inv_ltc … H) -H // #H
-@(TC_star_ind_dx ???????? H) -L1 /2 width=5 by pippo/
-#L1 #L0 #HL10 #HL0 #IH #T1 #T2 #HT12
-elim (IH … HT12) -IH #HT1 #HT21 #H1T21
-@and3_intro
-[2:
-*)
-
-axiom pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & ⦃L, T2⦄ ⊆ ⦃L, T⦄.
-
-lemma fle_tc_lfxs_trans: ∀h,G,L1,L2,T1. ⦃G, L1⦄ ⊢⬈*[h, T1] L2 →
- ∀T2. ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄ → ⦃G, L1⦄ ⊢⬈* [h, T2] L2.
-#h #G #L1 #L2 #T1 #H
-@(TC_star_ind_dx ???????? H) -L1 /2 width=1 by tc_lfxs_refl, lfxs_refl/
-#L1 #L #HL1 #_ #IH #T2 #HT21
-lapply (fle_lfxs_trans … HT21 … HL1) -HL1 #HL1
-@(TC_strap … HL1) @IH -IH
-
-
-lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
-#h #G #L1 #T1 #T2 #HT12 #L2 #H
-lapply (cpx_fle_comp … HT12) -HT12 #HT21
-
-elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
-@(lfpxs_lpxs_lfeq … HL1) -HL1
-
-
-@(fle_lfxs_trans
-
-elim (pippos … HL1 … HT12) -HT12 #T #H #HT21
-@(lfpxs_lpxs_lfeq … HL1) -HL1
-@(fle_lfxs_trans … HL2) -HL2 //
-qed-.
-
-
(* Forward lemmas with length for local environments ************************)
-(* Basic_2A1: uses: lpxs_fwd_length *)
lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|.
/2 width=3 by tc_lfxs_fwd_length/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/lfdeq_lfdeq.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/lfpxs_fqup.ma".
(* *)
(**************************************************************************)
-include "basic_2/static/lfdeq_lfdeq.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/lfsx.ma".
include "basic_2/notation/relations/predtysnstar_4.ma".
include "basic_2/relocation/lex.ma".
-include "basic_2/rt_computation/cpxs.ma".
+include "basic_2/rt_computation/cpxs_ext.ma".
(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
interpretation
"uncounted parallel rt-computation (local environment)"
'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpxs_inv_bind_sn: ∀h,G,I1,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-.
+
+lemma lpxs_inv_pair_sn: ∀h,G,I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
+#h #G #I #L2 #K1 #V1 #H
+elim (lpxs_inv_bind_sn … H) -H #Y #K2 #HK12 #H0 #H destruct
+elim (ext2_inv_pair_sn … H0) -H0 #V2 #HV12 #H 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 "basic_2/relocation/lex_length.ma".
+include "basic_2/rt_computation/lpxs.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma lpxs_fwd_length: ∀h,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|.
+/2 width=2 by lex_fwd_length/ 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_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
-lpxs.ma
+cpxs_ext.ma
+lpxs.ma lpxs_length.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
(* *)
(**************************************************************************)
-include "basic_2/syntax/tdeq_tdeq.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_transition/cnx.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/rt_transition/lfpx_fsle.ma".
+include "basic_2/rt_transition/cpm_cpx.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Forward lemmas with free variables inclusion for restricted closures *****)
+
+lemma cpm_fsle_comp: ∀n,h,G. R_fsle_compatible (cpm n h G).
+/3 width=6 by cpm_fwd_cpx, cpx_fsle_comp/ qed-.
+
+lemma lfpr_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpm 0 h G).
+/4 width=5 by cpm_fwd_cpx, lfpx_fsle_comp, lfxs_co/ qed-.
+
+(* Properties with generic extension on referred entries ********************)
+
+(* Basic_2A1: was just: cpr_llpx_sn_conf *)
+lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R).
+/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ 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_lfxs.ma".
-include "basic_2/rt_transition/cpm_cpx.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Properties with context-sensitive free variables *************************)
-
-lemma cpm_fsle_comp: ∀n,h,G. R_fsle_compatible (cpm n h G).
-/3 width=6 by cpm_fwd_cpx, cpx_fsle_comp/ qed-.
-
-lemma lfpr_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpm 0 h G).
-/4 width=5 by cpm_fwd_cpx, lfpx_fsle_comp, lfxs_co/ qed-.
-
-(* Properties with generic extension on referred entries ********************)
-
-(* Basic_2A1: was just: cpr_llpx_sn_conf *)
-lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R).
-/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ 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/static/fsle_drops.ma".
-include "basic_2/static/fsle_fqup.ma".
-include "basic_2/static/fsle_fsle.ma".
-include "basic_2/static/lfxs_length.ma".
-include "basic_2/static/lfxs_fsle.ma".
-include "basic_2/rt_transition/cpx.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties with context-sensitive free variables *************************)
-
-(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *)
-axiom cpx_lfxs_conf_fsle: ∀R,h. c_reflexive … R →
- (∨∨ (∀G. (cpx h G) = R) | R_fsle_compatible R) →
- ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
- ∀L2. L0 ⪤*[R, T0] L2 →
- ∧∧ ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄ & ⦃L2, T1⦄ ⊆ ⦃L2, T0⦄
- & ⦃L0, T1⦄ ⊆ ⦃L0, T0⦄.
-(*
-#R #h #H1R #H2R #G #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G L0 T0) -G -L0 -T0
-#G #L #T #IH #G0 #L0 * *
-[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH
- lapply (lfxs_fwd_length … HY) -HY #H0
- elim (cpx_inv_sort1 … HX) -HX #H destruct
- /3 width=1 by fsle_sort_length, and3_intro/
-| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
- [ elim (cpx_inv_zero1 … HX) -HX
- [ #H destruct
- elim (lfxs_inv_zero … HY) -HY *
- [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/
- | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
- lapply (lfxs_fwd_length … HK02) #HK
- elim H2R -H2R #H2R
- [ <(H2R G0) in HV02; -H2R #HV02
- elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #_
- /4 width=1 by fsle_trans_tc, fsle_zero_bi, and3_intro/
- | lapply (H2R … HV02 … HK02) -H2R -HV02 -HK02 -IH #HKV20
- /3 width=1 by fsle_zero_bi, and3_intro/
- ]
- | #f #I #K0 #K2 #Hf #HK02 #H1 #H2 destruct
- ]
- | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
- elim (lfxs_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
- ]
- | elim (cpx_inv_lref1 … HX) -HX
- [ #H destruct
- elim (lfxs_inv_lref … HY) -HY *
- [ #H0 #H1 destruct /2 width=1 by and3_intro/
- | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
- lapply (lfxs_fwd_length … HK02) #HK
- elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HK02
- /3 width=5 by and3_intro, fsle_lifts_SO/
- ]
- | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
- elim (lfxs_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
- lapply (lfxs_fwd_length … HK02) #HK
- elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HV1 -HK02
- /3 width=5 by fsle_lifts_SO, and3_intro/
- ]
- ]
-| #l #HG #HL #HT #X #HX #Y #HY destruct -IH
- lapply (lfxs_fwd_length … HY) -HY #H0
- >(cpx_inv_gref1 … HX) -X
- /3 width=1 by fsle_gref_length, and3_intro/
-| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
- lapply (lfxs_fwd_length … HY) #H0
- elim (lfxs_inv_bind … V0 ? HY) -HY // #HV0 #HT0
- elim (cpx_inv_bind1 … HX) -HX *
- [ #V1 #T1 #HV01 #HT01 #H destruct
- elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
- elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
- /4 width=3 by fsle_bind_eq, fsle_fwd_pair_sn, and3_intro/
- | #T #HT #HXT #H1 #H2 destruct
- elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V
- elim (IH … HT … HT0) -HT -HT0 -IH // #H1T #H2T #H3T
- /3 width=5 by fsle_bind, fsle_inv_lifts_sn, and3_intro/
- ]
-| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
- elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
- elim (cpx_inv_flat1 … HX) -HX *
- [ #V1 #T1 #HV01 #HT01 #H destruct
- elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
- elim (IH … HT01 … HX0) -HT01 -HX0 -IH // #H1T #H2T #H3T
- /3 width=3 by fsle_flat, and3_intro/
- | #HX #H destruct
- elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V
- elim (IH … HX … HX0) -HX -HX0 -IH // #H1T #H2T #H3T
- /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/
- | #HX #H destruct
- elim (IH … HX … HV0) -HX -HV0 // #H1V #H2V #H3V
- elim (IH G0 … X0… X0 … HX0) -HX0 -IH // #H1T #H2T #H3T
- /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/
- | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
- elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0
- elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
- elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W
- elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
- lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T
- lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T
- @and3_intro [ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *)
- @fsle_bind_sn_ge /4 width=1 by fsle_shift, fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
- | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
- elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0
- elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
- elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W
- elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
- lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T
- lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T
- @and3_intro[ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *)
- @fsle_bind_sn_ge //
- [1,3: /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
- |2,4: /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
- ]
- ]
-]
-*)
(**************************************************************************)
include "basic_2/static/lfdeq_lfdeq.ma".
-include "basic_2/rt_transition/cpx_lfxs.ma".
+include "basic_2/rt_transition/lfpx_fsle.ma".
(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
(**************************************************************************)
include "basic_2/static/lfeq.ma".
-include "basic_2/rt_transition/cpx_lfxs.ma".
+include "basic_2/rt_transition/lfpx_fsle.ma".
(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+++ /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/lveq_length.ma".
-include "basic_2/relocation/lexs_length.ma".
-include "basic_2/relocation/drops_lexs.ma".
-include "basic_2/static/frees_drops.ma".
-include "basic_2/static/lsubf_frees.ma".
-include "basic_2/static/lfxs_fsle.ma".
-include "basic_2/rt_transition/cpx_drops.ma".
-include "basic_2/rt_transition/cpx_ext.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties with context-sensitive free variables *************************)
-
-(* Basic_2A1: uses: lpx_cpx_frees_trans *)
-lemma cpx_frees_conf_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
- ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
- ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
-#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
-#G0 #L0 #U0 #IH #G #L1 * *
-[ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
- lapply (frees_inv_sort … H1) -H1 #Hg1
- elim (cpx_inv_sort1 … H0) -H0 #H destruct
- /3 width=3 by frees_sort, sle_refl, ex2_intro/
-| #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
- elim (frees_inv_lref_drops … H1) -H1 *
- [ -IH #f1 #HL1 #Hf1 #H destruct
- elim (cpx_inv_lref1_drops … H0) -H0
- [ #H destruct
- /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/
- | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1
- lapply (drops_TF … HLK1) -HLK1 #HLK1
- lapply (drops_mono … HLK1 … HL1) -L1 #H destruct
- ]
- | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct
- elim (cpx_inv_lref1_drops … H0) -H0
- [ #H destruct
- elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H
- elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct
- elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21
- /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/
- | * #Z #Y #X #V2 #H #HV12 #HVU2
- lapply (drops_mono … H … HLK1) -H #H destruct
- elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H
- elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct
- lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2
- elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21
- lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/
- ]
- | #f1 #I #K1 #HLK1 #Hf1 #H destruct
- elim (cpx_inv_lref1_drops … H0) -H0
- [ -IH #H destruct
- elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H
- lapply (ext2_inv_unit_sn … H) -H #H destruct
- /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/
- | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1
- lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct
- ]
- ]
-| -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
- lapply (frees_inv_gref … H1) -H1 #Hg1
- lapply (cpx_inv_gref1 … H0) -H0 #H destruct
- /3 width=3 by frees_gref, sle_refl, ex2_intro/
-| #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
- elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1
- elim (cpx_inv_bind1 … H0) -H0 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
- lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T
- elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
- elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
- elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/
- /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
- | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1
- lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T
- elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21
- lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2
- /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/
- ]
-| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
- elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1
- elim (cpx_inv_flat1 … H0) -H0 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
- lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
- elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21
- elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/
- /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/
- | #HU2 #H destruct -HgV1
- lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1
- /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/
- | #HU2 #H destruct -HgT0
- lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V
- elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1
- /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/
- | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct
- elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
- lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
- lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
- lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
- lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T
- elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
- lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
- lapply (sor_comm … Hg0) -Hg0 #Hg0
- elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
- elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
- elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
- elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_
- elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02
- lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0
- lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *)
- elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
- elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
- @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2
- @(sor_inv_sle … Hg2) -Hg2
- [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/
- | @(sle_trans … HgT02) -HgT02
- /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/
- ] (**) (* full auto too slow *)
- | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct
- elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
- lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
- lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
- lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
- lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T
- elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
- lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
- elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
- elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
- elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
- elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H
- elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
- elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
- lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2
- lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??)
- [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *)
- /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
- ]
-]
-qed-.
-
-(* Basic_2A1: uses: cpx_frees_trans *)
-lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G).
-#h #G #L #T1 #T2 #HT12
-elim (frees_total L T1) #f1 #Hf1
-elim (cpx_frees_conf_lexs … Hf1 L … HT12) -HT12
-/3 width=8 by lexs_refl, ext2_refl, ex4_4_intro/
-qed-.
-
-(* Basic_2A1: uses: lpx_frees_trans *)
-lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G).
-#h #G #L1 #L2 #T * #f1 #Hf1 #HL12
-elim (cpx_frees_conf_lexs h … Hf1 … HL12 T) // #f2 #Hf2
-lapply (lexs_fwd_length … HL12)
-/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
-qed-.
-
-(* Properties with generic extension on referred entries ********************)
-
-(* Note: lemma 1000 *)
-(* Basic_2A1: uses: cpx_llpx_sn_conf *)
-lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R).
-#R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf_lexs … Hf1 L1 … H) -T1
-/3 width=5 by lexs_refl, ext2_refl, sle_lexs_trans, ex2_intro/
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/rt_transition/cpm_lsubr.ma".
-include "basic_2/rt_transition/cpm_lfxs.ma".
+include "basic_2/rt_transition/cpm_fsle.ma".
include "basic_2/rt_transition/cpr.ma".
include "basic_2/rt_transition/cpr_drops.ma".
include "basic_2/rt_transition/lfpr_drops.ma".
| ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 &
Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_sort/ qed-.
-(*
-lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 &
- ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
-/2 width=1 by lfxs_inv_zero/ qed-.
-*)
+
lemma lfpx_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] Y2 →
∨∨ Y1 = ⋆ ∧ Y2 = ⋆
| ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, #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 "basic_2/rt_transition/cpx_lfxs.ma".
-include "basic_2/rt_transition/lfpx.ma".
-
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
-
-(* Advanced properties ******************************************************)
-
-lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G).
-/2 width=5 by cpx_lfxs_conf/ 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/lfpx_fsle.ma".
+(*
+lemma R_fle_comp_LTC: ∀R. R_fle_compatible R → R_fle_compatible (LTC … R).
+#R #HR #L #T1 #T2 #H elim H -T2
+/3 width=3 by fle_trans_dx/
+qed-.
+*)
+
+(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *)
+axiom lfpx_cpx_conf_fsle4: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
+ ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T1⦄.
+(*
+#h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0
+#G #L #T #IH #G0 #L0 * *
+[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH
+ lapply (lfxs_fwd_length … HY) -HY #H0
+ elim (cpx_inv_sort1 … HX) -HX #H destruct
+ /3 width=1 by fsle_sort_length, and3_intro/
+| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
+ [ elim (cpx_inv_zero1 … HX) -HX
+ [ #H destruct
+ elim (lfxs_inv_zero … HY) -HY *
+ [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/
+ | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
+ lapply (lfxs_fwd_length … HK02) #HK
+ elim H2R -H2R #H2R
+ [ <(H2R G0) in HV02; -H2R #HV02
+ elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #_
+ /4 width=1 by fsle_trans_tc, fsle_zero_bi, and3_intro/
+ | lapply (H2R … HV02 … HK02) -H2R -HV02 -HK02 -IH #HKV20
+ /3 width=1 by fsle_zero_bi, and3_intro/
+ ]
+ | #f #I #K0 #K2 #Hf #HK02 #H1 #H2 destruct
+ ]
+ | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
+ elim (lfxs_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
+ ]
+ | elim (cpx_inv_lref1 … HX) -HX
+ [ #H destruct
+ elim (lfxs_inv_lref … HY) -HY *
+ [ #H0 #H1 destruct /2 width=1 by and3_intro/
+ | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
+ lapply (lfxs_fwd_length … HK02) #HK
+ elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HK02
+ /3 width=5 by and3_intro, fsle_lifts_SO/
+ ]
+ | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
+ elim (lfxs_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
+ lapply (lfxs_fwd_length … HK02) #HK
+ elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HV1 -HK02
+ /3 width=5 by fsle_lifts_SO, and3_intro/
+ ]
+ ]
+| #l #HG #HL #HT #X #HX #Y #HY destruct -IH
+ lapply (lfxs_fwd_length … HY) -HY #H0
+ >(cpx_inv_gref1 … HX) -X
+ /3 width=1 by fsle_gref_length, and3_intro/
+| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
+ lapply (lfxs_fwd_length … HY) #H0
+ elim (lfxs_inv_bind … V0 ? HY) -HY // #HV0 #HT0
+ elim (cpx_inv_bind1 … HX) -HX *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
+ elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
+ /4 width=3 by fsle_bind_eq, fsle_fwd_pair_sn, and3_intro/
+ | #T #HT #HXT #H1 #H2 destruct
+ elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V
+ elim (IH … HT … HT0) -HT -HT0 -IH // #H1T #H2T #H3T
+ /3 width=5 by fsle_bind, fsle_inv_lifts_sn, and3_intro/
+ ]
+| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
+ elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
+ elim (cpx_inv_flat1 … HX) -HX *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
+ elim (IH … HT01 … HX0) -HT01 -HX0 -IH // #H1T #H2T #H3T
+ /3 width=3 by fsle_flat, and3_intro/
+ | #HX #H destruct
+ elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V
+ elim (IH … HX … HX0) -HX -HX0 -IH // #H1T #H2T #H3T
+ /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/
+ | #HX #H destruct
+ elim (IH … HX … HV0) -HX -HV0 // #H1V #H2V #H3V
+ elim (IH G0 … X0… X0 … HX0) -HX0 -IH // #H1T #H2T #H3T
+ /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/
+ | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
+ elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0
+ elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
+ elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W
+ elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
+ lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T
+ lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T
+ @and3_intro [ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *)
+ @fsle_bind_sn_ge /4 width=1 by fsle_shift, fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
+ | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
+ elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0
+ elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V
+ elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W
+ elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T
+ lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T
+ lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T
+ @and3_intro[ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *)
+ @fsle_bind_sn_ge //
+ [1,3: /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
+ |2,4: /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
+ ]
+ ]
+]
+*)
--- /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/fsle_drops.ma".
+include "basic_2/static/lfxs_fsle.ma".
+include "basic_2/rt_transition/lfpx_length.ma".
+include "basic_2/rt_transition/lfpx_fqup.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Forward lemmas with free variables inclusion for restricted closures *****)
+
+(* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
+(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *)
+(* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)
+(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *)
+(* Basic_2A1: uses: lpx_cpx_frees_trans *)
+lemma lfpx_cpx_conf_fsle: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
+ ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
+#h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0
+#G #L #T #IH #G0 #L0 * *
+[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH
+ elim (cpx_inv_sort1 … HX) -HX #H destruct
+ lapply (lfpx_fwd_length … HY) -HY #H0
+ /2 width=1 by fsle_sort_bi/
+| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
+ [ elim (cpx_inv_zero1 … HX) -HX
+ [ #H destruct
+ elim (lfpx_inv_zero_length … HY) -HY *
+ [ #H1 #H2 destruct -IH //
+ | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
+ lapply (lfpx_fwd_length … HK02) #H0
+ /4 width=4 by fsle_pair_bi, fqu_fqup, fqu_lref_O/
+ | #I #K0 #K2 #HK02 #H1 #H2 destruct -IH
+ /2 width=1 by fsle_unit_bi/
+ ]
+ | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
+ elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
+ lapply (lfpx_fwd_length … HK02) #H0
+ /4 width=4 by fsle_lifts_SO_sn, fqu_fqup, fqu_lref_O/
+ ]
+ | elim (cpx_inv_lref1 … HX) -HX
+ [ #H destruct
+ elim (lfpx_inv_lref … HY) -HY *
+ [ #H0 #H1 destruct //
+ | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
+ lapply (lfpx_fwd_length … HK02) #H0
+ /4 width=5 by fsle_lifts_SO, fqu_fqup/
+ ]
+ | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
+ elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
+ lapply (lfpx_fwd_length … HK02) #H0
+ /4 width=5 by fsle_lifts_SO, fqu_fqup/
+ ]
+ ]
+| #l #HG #HL #HT #X #HX #Y #HY destruct -IH
+ >(cpx_inv_gref1 … HX) -X
+ lapply (lfpx_fwd_length … HY) -HY #H0
+ /2 width=1 by fsle_gref_bi/
+| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
+ elim (lfpx_inv_bind … V0 ? HY) -HY #HV0 #HT0
+ elim (cpx_inv_bind1 … HX) -HX *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ lapply (lfpx_fwd_length … HV0) #H0
+ /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/
+ | #T #HT #HXT #H1 #H2 destruct
+ lapply (lfpx_fwd_length … HV0) #H0
+ /3 width=8 by fsle_inv_lifts_sn/
+ ]
+| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
+ elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
+ elim (cpx_inv_flat1 … HX) -HX *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ /3 width=4 by fsle_flat/
+ | #HX #H destruct
+ /4 width=4 by fsle_flat_dx_dx/
+ | #HX #H destruct
+ /4 width=4 by fsle_flat_dx_sn/
+ | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
+ elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
+ lapply (lfpx_fwd_length … HV0) #H0
+ lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
+ lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
+ lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
+ lapply (fsle_fwd_pair_sn … HT) -HT #HT
+ @fsle_bind_sn_ge //
+ [ /4 width=1 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
+ | /3 width=1 by fsle_flat_dx_dx, fsle_shift/
+ ]
+ | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
+ elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
+ lapply (lfpx_fwd_length … HV0) #H0
+ lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
+ lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
+ lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
+ lapply (fsle_fwd_pair_sn … HT) -HT #HT
+ @fsle_bind_sn_ge //
+ [ /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
+ | /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
+ ]
+ ]
+]
+qed.
+
+(* Basic_2A1: uses: cpx_frees_trans *)
+lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G).
+/2 width=4 by lfpx_cpx_conf_fsle/ qed-.
+
+(* Basic_2A1: uses: lpx_frees_trans *)
+lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G).
+/2 width=4 by lfpx_cpx_conf_fsle/ qed-.
+
+(* Properties with generic extension on referred entries ********************)
+
+(* Note: lemma 1000 *)
+(* Basic_2A1: uses: cpx_llpx_sn_conf *)
+lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R).
+/3 width=3 by fsle_lfxs_trans, cpx_fsle_comp/ qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G).
+/2 width=5 by cpx_lfxs_conf/ qed-.
(* Basic_2A1: uses: lpx_fwd_length *)
lemma lfpx_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → |L1| = |L2|.
/2 width=3 by lfxs_fwd_length/ qed-.
+
+(* Inversion lemmas with length for local environments **********************)
+
+lemma lfpx_inv_zero_length: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 &
+ ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ |∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+/2 width=1 by lfxs_inv_zero_length/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/lifts_tdeq.ma".
-include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/static/lfdeq_fqup.ma".
include "basic_2/static/lfdeq_lfdeq.ma".
-include "basic_2/rt_transition/cpx_lfxs.ma".
-include "basic_2/rt_transition/lfpx.ma".
+include "basic_2/rt_transition/lfpx_fsle.ma".
(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+++ /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/fsle.ma".
-
-(* FREE VARIABLES INCLUSION FOR TERMS ***************************************)
-
-interpretation "free variables inclusion (term)"
- 'subseteq T1 T2 = (fsle LAtom T1 LAtom T2).
∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
/2 width=4 by frees_inv_flat_aux/ qed-.
-(* Advanced inversion lemmas ***********************************************)
-(*
-lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f →
- ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
-#f #I #K #V #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
-| #g #Z #Y #_ #H destruct
-]
-qed-.
-
-lemma frees_inv_zero_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
-#f #I #K #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #_ #H destruct
-| /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma frees_inv_lref_bind: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
- ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
-#f #I #K #i #H elim (frees_inv_lref … H) -H *
-[ #H destruct
-| #g #Z #Y #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
-]
-qed-.
-*)
(* Basic properties ********************************************************)
lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
qed-.
+lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≡ f → ⋆ ⊢ 𝐅*⦃#⫯i⦄ ≡ ↑f.
+#f #i #H
+elim (frees_inv_atom … H) -H #g #Hg #H destruct
+/2 width=1 by frees_atom/
+qed.
+
(* Forward lemmas with test for finite colength *****************************)
lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
--- /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/append.ma".
+include "basic_2/static/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties with append for local environments ****************************)
+
+lemma frees_append_void: ∀f,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f → ⓧ.K ⊢ 𝐅*⦃T⦄ ≡ f.
+#f #K #T #H elim H -f -K -T
+[ /2 width=1 by frees_sort/
+| #f * /3 width=1 by frees_atom, frees_unit, frees_lref/
+| /2 width=1 by frees_pair/
+| /2 width=1 by frees_unit/
+| /2 width=1 by frees_lref/
+| /2 width=1 by frees_gref/
+| /3 width=5 by frees_bind/
+| /3 width=5 by frees_flat/
+]
+qed.
+
+(* Inversion lemmas with append for local environments **********************)
+
+fact frees_inv_append_void_aux: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f →
+ ∀K. L = ⓧ.K → K ⊢ 𝐅*⦃T⦄ ≡ f.
+#f #L #T #H elim H -f -L -T
+[ /2 width=1 by frees_sort/
+| #f #i #_ #K #H
+ elim (append_inv_atom3_sn … H) -H #H1 #H2 destruct
+| #f #I #L #V #_ #IH #K #H
+ elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct
+ /3 width=1 by frees_pair/
+| #f #I #L #Hf #K #H
+ elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct
+ /2 width=1 by frees_atom, frees_unit/
+| #f #I #L #i #Hf #IH #K #H
+ elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct
+ /3 width=1 by frees_lref, frees_lref_push/
+| /2 width=1 by frees_gref/
+| /3 width=5 by frees_bind/
+| /3 width=5 by frees_flat/
+]
+qed-.
+
+lemma frees_inv_append_void: ∀f,K,T. ⓧ.K ⊢ 𝐅*⦃T⦄ ≡ f → K ⊢ 𝐅*⦃T⦄ ≡ f.
+/2 width=3 by frees_inv_append_void_aux/ qed-.
@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *)
qed-.
+lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
+ ∀W1. ⬆*[1] V1 ≡ W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
+#K1 #K2 #HK #V1 #V2
+* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
+#W1 #HVW1 #I1 #I2
+elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
+/5 width=12 by frees_lifts_SO, frees_pair, drops_refl, drops_drop, lveq_bind, sle_weak, ex4_4_intro/
+qed.
+
lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1, T1⦄ ⊆ ⦃K2, T2⦄ →
∀U1,U2. ⬆*[1] T1 ≡ U1 → ⬆*[1] T2 ≡ U2 →
∀I1,I2. ⦃K1.ⓘ{I1}, U1⦄ ⊆ ⦃K2.ⓘ{I2}, U2⦄.
lemma fsle_gref_bi: ∀L1,L2,l1,l2. |L1| = |L2| → ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄.
/3 width=8 by lveq_length_eq, frees_gref, sle_refl, ex4_4_intro/ qed.
-lemma fsle_zero_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
+lemma fsle_pair_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
∀I1,I2. ⦃K1.ⓑ{I1}V1, #O⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
#K1 #K2 #HK #V1 #V2
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
/3 width=12 by frees_pair, lveq_bind, sle_next, ex4_4_intro/
qed.
+
+lemma fsle_unit_bi: ∀K1,K2. |K1| = |K2| →
+ ∀I1,I2. ⦃K1.ⓤ{I1}, #O⦄ ⊆ ⦃K2.ⓤ{I2}, #O⦄.
+/3 width=8 by frees_unit, lveq_length_eq, sle_refl, ex4_4_intro/
+qed.
(* *)
(**************************************************************************)
-include "basic_2/syntax/lveq_length.ma".
include "basic_2/relocation/lifts_tdeq.ma".
include "basic_2/static/lfxs_length.ma".
include "basic_2/static/lfxs_fsle.ma".
include "basic_2/syntax/ext2_ext2.ma".
include "basic_2/syntax/tdeq_tdeq.ma".
-include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/static/lfdeq_length.ma".
(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
(* *)
(**************************************************************************)
-include "basic_2/static/fsle.ma".
-include "basic_2/static/lfxs.ma".
+include "basic_2/relocation/lexs_length.ma".
+include "basic_2/static/frees_drops.ma".
+include "basic_2/static/fsle_fsle.ma".
+include "basic_2/static/lfxs_lfxs.ma".
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN.
∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄.
+
+(* Basic inversions with free variables inclusion for restricted closures ***)
+
+lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R →
+ ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
+ ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 →
+ ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
+#R #HR #L1 #T #f1 #Hf1 #L2 #H1L
+lapply (HR L1 L2 T ?) /2 width=3 by ex2_intro/ #H2L
+@(fsle_frees_trans_eq … H2L … Hf1) /3 width=4 by lexs_fwd_length, sym_eq/
+qed-.
+
+(* Properties with free variables inclusion for restricted closures *********)
+
+(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *)
+lemma fsle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ →
+ ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2.
+#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12
+elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct
+/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/
+qed-.
+
+lemma lfxs_sym: ∀R. lfxs_fsle_compatible R →
+ (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
+ ∀T. symmetric … (lfxs R T).
+#R #H1R #H2R #T #L1 #L2
+* #f1 #Hf1 #HL12
+elim (frees_lexs_conf … Hf1 … HL12) -Hf1 //
+/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/
+qed-.
+
+lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ lfxs_fsle_compatible R1 →
+ ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T.
+ ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2.
+#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T
+[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
+ elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy
+| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
+ elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy
+]
+lapply(frees_mono … H … Hf) -H #H1
+lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy
+lapply (sor_inv_sle_sn … Hy) -y2 #Hfg
+elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
+lapply (sle_lexs_trans … HL1 … Hfg) // #H
+elim (frees_lexs_conf … Hf … H) -Hf -H
+/4 width=7 by sle_lexs_trans, ex2_intro/
+qed-.
+
+lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ lfxs_fsle_compatible R1 →
+ ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V.
+ ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2.
+#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V
+elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
+elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy
+lapply(frees_mono … H … Hf) -H #H2
+lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
+lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
+lapply (sle_lexs_trans … HL1 … Hfg) // #H
+elim (frees_lexs_conf … Hf … H) -Hf -H
+/4 width=7 by sle_lexs_trans, ex2_intro/
+qed-.
+
+lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ lfxs_fsle_compatible R1 →
+ ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p.
+ ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V.
+#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
+elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg
+elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
+lapply(frees_mono … H … Hf) -H #H2
+lapply (tl_eq_repl … H2) -H2 #H2
+lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
+lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
+lapply (sle_lexs_trans … H … Hfg) // #H0
+elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
+elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct
+elim (frees_lexs_conf … Hf … H0) -Hf -H0
+/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/
+qed-.
+
+lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ lfxs_fsle_compatible R1 →
+ ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V.
+ ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2.
+#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V
+elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
+elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy
+lapply(frees_mono … H … Hf) -H #H2
+lapply (tl_eq_repl … H2) -H2 #H2
+lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
+lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
+lapply (sle_lexs_trans … H … Hfg) // #H0
+elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
+elim (ext2_inv_unit_sn … H) -H #H destruct
+elim (frees_lexs_conf … Hf … H0) -Hf -H0
+/4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *)
+qed-.
+
+(* Main properties with free variables inclusion for restricted closures ****)
+
+theorem lfxs_conf: ∀R1,R2.
+ lfxs_fsle_compatible R1 →
+ lfxs_fsle_compatible R2 →
+ R_confluent2_lfxs R1 R2 R1 R2 →
+ ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T).
+#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
+lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
+lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
+elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
+[ #L #HL1 #HL2
+ elim (frees_lexs_conf … Hf … HL01) // -HR1 -HL01 #f1 #Hf1 #H1
+ elim (frees_lexs_conf … Hf … HL02) // -HR2 -HL02 #f2 #Hf2 #H2
+ lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
+ lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
+ /3 width=5 by ex2_intro/
+| #g * #I0 [2: #V0 ] #K0 #n #HLK0 #Hgf #Z1 #H1 #Z2 #H2 #K1 #HK01 #K2 #HK02
+ [ elim (ext2_inv_pair_sn … H1) -H1 #V1 #HV01 #H destruct
+ elim (ext2_inv_pair_sn … H2) -H2 #V2 #HV02 #H destruct
+ elim (frees_inv_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
+ lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
+ lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
+ elim (HR12 … HV01 … HV02 K1 … K2) /3 width=3 by ext2_pair, ex2_intro/
+ | lapply (ext2_inv_unit_sn … H1) -H1 #H destruct
+ lapply (ext2_inv_unit_sn … H2) -H2 #H destruct
+ /3 width=3 by ext2_unit, ex2_intro/
+ ]
+]
+qed-.
lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
/4 width=12 by lexs_length_cfull, lexs_liftable_co_dedropable_bi, cext2_d_liftable2_sn, cfull_lift_sn, ex2_intro/
qed-.
+
+(* Inversion lemmas with length for local environment ***********************)
+
+lemma lfxs_inv_zero_length: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 →
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+#R #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H *
+/4 width=9 by lexs_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/lexs_length.ma".
include "basic_2/relocation/lexs_lexs.ma".
-include "basic_2/static/frees_drops.ma".
-include "basic_2/static/fsle_fsle.ma".
-include "basic_2/static/lfxs_fsle.ma".
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/lfxs.ma".
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
#R #L1 #L2 #T * /3 width=6 by frees_mono, lexs_eq_repl_back/
qed-.
-lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R →
- ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
- ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 →
- ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
-#R #HR #L1 #T #f1 #Hf1 #L2 #H1L
-lapply (HR L1 L2 T ?) /2 width=3 by ex2_intro/ #H2L
-@(fsle_frees_trans_eq … H2L … Hf1) /3 width=4 by lexs_fwd_length, sym_eq/
-qed-.
-
-(* Properties with free variables inclusion for restricted closures *********)
-
-(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *)
-lemma fle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ →
- ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2.
-#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12
-elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct
-/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/
-qed-.
-
(* Advanced properties ******************************************************)
-lemma lfxs_sym: ∀R. lfxs_fsle_compatible R →
- (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
- ∀T. symmetric … (lfxs R T).
-#R #H1R #H2R #T #L1 #L2
-* #f1 #Hf1 #HL12
-elim (frees_lexs_conf … Hf1 … HL12) -Hf1 //
-/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/
-qed-.
-
(* Basic_2A1: uses: llpx_sn_dec *)
lemma lfxs_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀L1,L2,T. Decidable (L1 ⪤*[R, T] L2).
/4 width=3 by lfxs_inv_frees, cfull_dec, ext2_dec, ex2_intro, or_intror, or_introl/
qed-.
-lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
- ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T.
- ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T
-[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
- elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy
-| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
- elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy
-]
-lapply(frees_mono … H … Hf) -H #H1
-lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy
-lapply (sor_inv_sle_sn … Hy) -y2 #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
-lapply (sle_lexs_trans … HL1 … Hfg) // #H
-elim (frees_lexs_conf … Hf … H) -Hf -H
-/4 width=7 by sle_lexs_trans, ex2_intro/
-qed-.
-
-lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
- ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V.
- ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V
-elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
-elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
-lapply (sle_lexs_trans … HL1 … Hfg) // #H
-elim (frees_lexs_conf … Hf … H) -Hf -H
-/4 width=7 by sle_lexs_trans, ex2_intro/
-qed-.
-
-lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
- ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p.
- ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V.
-#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
-elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg
-elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
-lapply (sle_lexs_trans … H … Hfg) // #H0
-elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
-elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct
-elim (frees_lexs_conf … Hf … H0) -Hf -H0
-/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/
-qed-.
-
-lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
- ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V.
- ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V
-elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
-elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
-lapply (sle_lexs_trans … H … Hfg) // #H0
-elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
-elim (ext2_inv_unit_sn … H) -H #H destruct
-elim (frees_lexs_conf … Hf … H0) -Hf -H0
-/4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *)
-qed-.
-
(* Main properties **********************************************************)
(* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *)
/3 width=7 by frees_fwd_isfin, frees_bind_void, lexs_join, isfin_tl, ex2_intro/
qed.
-theorem lfxs_conf: ∀R1,R2.
- lfxs_fsle_compatible R1 →
- lfxs_fsle_compatible R2 →
- R_confluent2_lfxs R1 R2 R1 R2 →
- ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T).
-#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
-lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
-lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
-elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
-[ #L #HL1 #HL2
- elim (frees_lexs_conf … Hf … HL01) // -HR1 -HL01 #f1 #Hf1 #H1
- elim (frees_lexs_conf … Hf … HL02) // -HR2 -HL02 #f2 #Hf2 #H2
- lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
- lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
- /3 width=5 by ex2_intro/
-| #g * #I0 [2: #V0 ] #K0 #n #HLK0 #Hgf #Z1 #H1 #Z2 #H2 #K1 #HK01 #K2 #HK02
- [ elim (ext2_inv_pair_sn … H1) -H1 #V1 #HV01 #H destruct
- elim (ext2_inv_pair_sn … H2) -H2 #V2 #HV02 #H destruct
- elim (frees_inv_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
- lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
- lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
- elim (HR12 … HV01 … HV02 K1 … K2) /3 width=3 by ext2_pair, ex2_intro/
- | lapply (ext2_inv_unit_sn … H1) -H1 #H destruct
- lapply (ext2_inv_unit_sn … H2) -H2 #H destruct
- /3 width=3 by ext2_unit, ex2_intro/
- ]
-]
-qed-.
-
theorem lfxs_trans_gen: ∀R1,R2,R3.
c_reflexive … R1 → c_reflexive … R2 →
lfxs_confluent R1 R2 → lfxs_transitive R1 R2 R3 →
(* Basic inversion lemmas ***************************************************)
+lemma append_inv_atom3_sn: ∀L,K. ⋆ = L @@ K → ∧∧ ⋆ = L & ⋆ = K.
+#L * /2 width=1 by conj/
+#K #I >append_bind #H destruct
+qed-.
+
+lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L @@ K →
+ ∨∨ ∧∧ L0.ⓘ{I0} = L & ⋆ = K
+ | ∃∃K0. K = K0.ⓘ{I0} & L0 = L @@ K0.
+#I0 #L #L0 * /3 width=1 by or_introl, conj/
+#K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/
+qed-.
+
lemma append_inj_sn: ∀K,L1,L2. L1@@K = L2@@K → L1 = L2.
#K elim K -K //
#K #I #IH #L1 #L2 >append_bind #H
class "blue"
[ { "rt-conversion" * } {
[ { "context-sensitive parallel r-conversion" * } {
- [ [ "for terms" ] "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
+ [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
}
]
}
]
*)
[ { "uncounted context-sensitive parallel rt-computation" * } {
- [ [ "refinement for lenvs" ] "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
- [ [ "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_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_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
+ [ [ "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_lpxs" + "lfpxs_lfpxs" * ]
+ [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" * ]
+ [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
+ [ [ "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" * ]
}
]
}
class "cyan"
[ { "rt-transition" * } {
[ { "uncounted parallel rst-transition" * } {
- [ [ "for closures" ] "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ [ "proper for closures" ] "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+ [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
+ [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
}
]
[ { "context-sensitive parallel r-transition" * } {
- [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
- [ [ "for binders" ] "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
- [ [ "for terms" ] "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
+ [ [ "for lenvs on referred entries" ] "lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
+ [ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
+ [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
}
]
[ { "t-bound context-sensitive parallel rt-transition" * } {
- [ [ "for terms" ] "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
+ [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_cpx" * ]
}
]
[ { "uncounted context-sensitive parallel rt-transition" * } {
- [ [ "normal form for terms" ] "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
- [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "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" + "cpx_lfeq" * ]
+ [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
+ [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
+ [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
+ [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
+ [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ]
}
]
[ { "counted context-sensitive parallel rt-transition" * } {
- [ [ "for terms" ] "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
+ [ [ "for terms" ] "cpg" + "( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
}
]
}
class "water"
[ { "iterated static typing" * } {
[ { "iterated generic extension of a context-sensitive relation" * } {
- [ [ "for lenvs on referred entries" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+ [ [ "for lenvs on referred entries" ] "tc_lfxs" + "( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
}
]
}
class "green"
[ { "static typing" * } {
[ { "generic reducibility" * } {
- [ [ "restricted refinement for lenvs" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
- [ [ "candidates" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+ [ [ "restricted refinement for lenvs" ] "lsubc" + "( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
+ [ [ "candidates" ] "gcp_cr" + "( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
[ [ "computation properties" ] "gcp" *]
}
]
[ { "atomic arity assignment" * } {
- [ [ "restricted refinement for lenvs" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
- [ [ "for terms" ] "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
+ [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
+ [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
}
]
[ { "degree-based equivalence" * } {
- [ [ "for closures on referred entries" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- [ [ "for lenvs on referred entries" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+ [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+ [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on referred entries" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
+ [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
}
]
[ { "generic extension of a context-sensitive relation" * } {
- [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
+ [ [ "for lenvs on referred entries" ] "lfxs" + "( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "lfxs_fsle" + "lfxs_lfxs" * ]
}
]
[ { "context-sensitive free variables" * } {
- [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ]
- [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
- [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
+ [ [ "inclusion for restricted closures" ] "fsle" + "( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fsle_length" + "fsle_drops" + "fsle_fqup" + "fsle_fsle" * ]
+ [ [ "restricted refinement for lenvs" ] "lsubf" + "( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
+ [ [ "for terms" ] "frees" + "( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_append" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
[ { "local environments" * } {
- [ [ "restricted refinement" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
+ [ [ "restricted refinement" ] "lsubr" + "( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
}
]
}
class "grass"
[ { "s-computation" * } {
[ { "iterated structural successor" * } {
- [ [ "for closures" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ]
- [ [ "proper for closures" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ]
+ [ [ "for closures" ] "fqus" + "( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ]
+ [ [ "proper for closures" ] "fqup" + "( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ]
}
]
}
class "yellow"
[ { "s-transition" * } {
[ { "structural successor" * } {
- [ [ "for closures" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
- [ [ "proper for closures" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
+ [ [ "for closures" ] "fquq" + "( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
+ [ [ "proper for closures" ] "fqu" + "( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
}
]
}
class "orange"
[ { "relocation" * } {
[ { "generic slicing" * } {
- [ [ "for lenvs" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
+ [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≡ ? )" + "( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
}
]
[ { "generic 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_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" * ]
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on selected entries" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+ [ [ "for lenvs on selected entries" ] "lreq" + "( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
}
]
[ { "generic entrywise extension" * } {
- [ [ "for lenvs of one contex-sensitive relation" ] "lex ( ? ⦻[?] ? )" "lex_tc" * ]
- [ [ "for lenvs of two contex-sensitive relations" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
+ [ [ "for lenvs of one contex-sensitive relation" ] "lex" + "( ? ⦻[?] ? )" "lex_tc" + "lex_length" * ]
+ [ [ "for lenvs of two contex-sensitive relations" ] "lexs" + "( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
}
]
}
class "red"
[ { "syntax" * } {
[ { "equivalence up to exclusion binders" * } {
- [ [ "for lenvs" ] "lveq ( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ]
+ [ [ "for lenvs" ] "lveq" + "( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ]
}
]
[ { "append" * } {
- [ [ "for lenvs" ] "append ( ? @@ ? )" "append_length" * ]
+ [ [ "for lenvs" ] "append" + "( ? @@ ? )" "append_length" * ]
}
]
[ { "head equivalence" * } {
- [ [ "for terms" ] "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
+ [ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
}
]
[ { "degree-based equivalence" * } {
- [ [ "" ] "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ]
- [ [ "" ] "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
+ [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
+ [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
}
]
[ { "closures" * } {
- [ [ "" ] "cl_weight ( ♯{?,?,?} )" * ]
- [ [ "" ] "cl_restricted_weight ( ♯{?,?} )" * ]
+ [ [ "" ] "cl_weight" + "( ♯{?,?,?} )" * ]
+ [ [ "" ] "cl_restricted_weight" + "( ♯{?,?} )" * ]
}
]
[ { "global environments" * } {
[ { "local environments" * } {
[ [ "" ] "ceq_ext" "ceq_ext_ceq_ext" * ]
[ [ "" ] "cext2" * ]
- [ [ "" ] "lenv_length ( |?| )" * ]
- [ [ "" ] "lenv_weight ( ♯{?} )" * ]
+ [ [ "" ] "lenv_length" + "( |?| )" * ]
+ [ [ "" ] "lenv_weight" + "( ♯{?} )" * ]
[ [ "" ] "lenv" * ]
}
]
}
]
[ { "terms" * } {
- [ [ "" ] "term_vector ( Ⓐ?.? )" * ]
- [ [ "" ] "term_simple ( 𝐒⦃?⦄ )" * ]
- [ [ "" ] "term_weight ( ♯{?} )" * ]
+ [ [ "" ] "term_vector" + "( Ⓐ?.? )" * ]
+ [ [ "" ] "term_simple" + "( 𝐒⦃?⦄ )" * ]
+ [ [ "" ] "term_weight" + "( ♯{?} )" * ]
[ [ "" ] "term" * ]
}
]
projects / helm.git / commitdiff