--- /dev/null
+(* Basic inversion lemmas ***************************************************)
+
+fact fle_inv_voids_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+ ∀K1,K2,n1,n2. |K1| = |K2| → L1 = ⓧ*[n1]K1 → L2 = ⓧ*[n2]K2 →
+ ∃∃f1,f2. ⓧ*[n1]K1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & ⓧ*[n2]K2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
+#L1 #L2 #T1 #T2 * -L1 -L2
+#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #HL12 #Hf12 #Y1 #Y2 #x1 #x2 #HY12 #H1 #H2 destruct
+>H1 in Hf1; >H2 in Hf2; #Hf2 #Hf1
+@(ex3_2_intro … Hf1 Hf2) -Hf1 -Hf2
+
+elim (voids_inj_length … H1) // -H -HL12 -HY #H1 #H2 destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma fle_inv_voids_sn: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ → |L1| = |L2| →
+ ∃∃f1,f2. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2.
+/2 width=3 by fle_inv_voids_sn_aux/ qed-.
#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_gen … HT12 … H) -HT12 -H // #_ #HT21 #_
+elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_
@(lfpxs_lpxs_lfeq … HL1) -HL1
@(fle_lfxs_trans … HL2) //
qed-.
include "basic_2/static/fle_drops.ma".
include "basic_2/static/fle_fqup.ma".
+include "basic_2/static/fle_lsubf.ma".
include "basic_2/static/fle_fle.ma".
-include "basic_2/static/lfxs.ma".
+include "basic_2/static/lfxs_length.ma".
include "basic_2/rt_transition/cpx.ma".
-axiom fle_pair_sn: ∀L,V1,V2. ⦃L, V1⦄ ⊆ ⦃L, V2⦄ →
- ∀I1,I2,T. ⦃L.ⓑ{I1}V1, T⦄ ⊆ ⦃L.ⓑ{I2}V2, T⦄.
-(*
-axiom fle_elim_flat: ∀L1,L2,V1,T2. ⦃L1, V1⦄ ⊆ ⦃L2, T2⦄ → ∀T1. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
- ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⊆ ⦃L2, T2⦄.
-
-axiom fle_elim_bind:
- ∀p,I1,I2,J1,J2,L,V,W,T. ⦃L, ⓑ{p,I1}ⓕ{J1}V.W.T⦄ ⊆ ⦃L, ⓕ{J2}V.ⓑ{p,I2}W.T⦄.
-*)
(* 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_gen: ∀R. c_reflexive … R →
+axiom cpx_lfxs_conf_fle: ∀R. c_reflexive … R →
∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
∀L2. L0 ⪤*[R, T0] L2 →
∧∧ ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄ & ⦃L2, T1⦄ ⊆ ⦃L2, T0⦄
(*
#R #HR #h #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 #_ destruct -IH
+[ #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
- /2 width=1 by and3_intro/
-|
-| #l #HG #HL #HT #X #HX #Y #_ destruct -IH
+ /3 width=1 by fle_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
+ elim (IH … HK02) [4,5: /2 width=2 by fqu_fqup, fqu_lref_O/ ]
+
+ lapply (lfxs_fwd_length … HY) -HY #H0
+ /3 width=1 by fle_lref_length, and3_intro/
+ | * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HX
+
+ elim (lfxs_inv_lref … HY) -HY // #HV0 #HT0
+
+| #l #HG #HL #HT #X #HX #Y #HY destruct -IH
+ lapply (lfxs_fwd_length … HY) -HY #H0
>(cpx_inv_gref1 … HX) -X
- /2 width=1 by and3_intro/
+ /3 width=1 by fle_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
- /5 width=4 by fle_pair_sn, fle_trans, fle_bind, and3_intro/
+ /4 width=3 by fle_bind_eq, fle_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
- /4 width=7 by fle_bind_dx, fle_trans, fle_bind, and3_intro/
+ /3 width=5 by fle_bind, fle_inv_lifts_sn, and3_intro/
]
| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
| #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=4 by fle_trans, fle_flat, and3_intro/
+ /4 width=3 by fle_flat_sn, fle_flat_dx_dx, fle_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=4 by fle_trans, fle_flat, and3_intro/
+ /4 width=3 by fle_flat_sn, fle_flat_dx_dx, fle_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
- @and3_intro
- [ /3 width=5 by fle_flat, fle_bind/
- | @(fle_trans)
- [4: @(fle_flat … H2V) [2: @(fle_bind … H2T) // | skip | @Appl ]
- |1,2: skip
- | @(fle_trans) [3: @fle_elim_bind
-
- … H2T) //
-
- // |1,2: skip
- | /2 width=1 by fle_bind_dx/
-*)
+ lapply (fle_fwd_pair_sn … H2T) -H2T #H2T
+ lapply (fle_fwd_pair_sn … H3T) -H3T #H3T
+ @and3_intro [ /3 width=5 by fle_flat, fle_bind/ ] (**) (* full auto too slow *)
+ @fle_bind_sn_ge /4 width=1 by fle_shift, fle_flat_sn, fle_flat_dx_dx, fle_flat_dx_sn, fle_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 (fle_fwd_pair_sn … H2T) -H2T #H2T
+ lapply (fle_fwd_pair_sn … H3T) -H3T #H3T
+ @and3_intro[ /3 width=5 by fle_flat, fle_bind/ ] (**) (* full auto too slow *)
+ @fle_bind_sn_ge //
+ [1,3: /3 width=1 by fle_flat_dx_dx, fle_bind_dx_sn/
+ |2,4: /4 width=3 by fle_flat_sn, fle_flat_dx_sn, fle_flat_dx_dx, fle_shift, fle_lifts_sn/
+ ]
+ ]
+]
+*)
\ No newline at end of file
lemma fle_gref: ∀L,l1,l2. ⦃L, §l1⦄ ⊆ ⦃L, §l2⦄.
/3 width=8 by frees_gref, sle_refl, ex4_4_intro/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-(*
-fact fle_inv_voids_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
- ∀K1,K2,n1,n2. |K1| = |K2| → L1 = ⓧ*[n1]K1 → L2 = ⓧ*[n2]K2 →
- ∃∃f1,f2. ⓧ*[n1]K1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & ⓧ*[n2]K2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
-#L1 #L2 #T1 #T2 * -L1 -L2
-#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #HL12 #Hf12 #Y1 #Y2 #x1 #x2 #HY12 #H1 #H2 destruct
->H1 in Hf1; >H2 in Hf2; #Hf2 #Hf1
-@(ex3_2_intro … Hf1 Hf2) -Hf1 -Hf2
-
-elim (voids_inj_length … H1) // -H -HL12 -HY #H1 #H2 destruct
-/2 width=5 by ex3_2_intro/
-qed-.
-
-lemma fle_inv_voids_sn: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ → |L1| = |L2| →
- ∃∃f1,f2. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2.
-/2 width=3 by fle_inv_voids_sn_aux/ qed-.
-*)
\ No newline at end of file
(* *)
(**************************************************************************)
+include "basic_2/syntax/lveq_length.ma".
include "basic_2/static/frees_drops.ma".
include "basic_2/static/fle.ma".
(* Advanced properties ******************************************************)
-lemma fle_bind_dx: ∀T,U. ⬆*[1] T ≡ U →
- ∀p,I,L,V. ⦃L, T⦄ ⊆ ⦃L, ⓑ{p,I}V.U⦄.
-#T #U #HTU #p #I #L #V
-elim (frees_total L V) #f1 #Hf1
-elim (frees_total L T) #f2 #Hf2
-elim (sor_isfin_ex f1 f2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-lapply (sor_inv_sle_dx … Hf) #Hf0
-/6 width=8 by frees_lifts_SO, frees_bind, drops_refl, drops_drop, sle_tls, ex4_4_intro/
-qed.
+lemma fle_lifts_sn: ∀T1,U1. ⬆*[1] T1 ≡ U1 → ∀L1,L2. |L2| ≤ |L1| →
+ ∀T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → ⦃L1.ⓧ, U1⦄ ⊆ ⦃L2, T2⦄.
+#T1 #U1 #HTU1 #L1 #L2 #H1L #T2
+* #n #m #f #g #Hf #Hg #H2L #Hfg
+lapply (lveq_length_fwd_dx … H2L ?) // -H1L #H destruct
+lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf)
+[ /3 width=4 by drops_refl, drops_drop/ ] -T1 #Hf
+@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *)
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fle_inv_lifts_sn: ∀T1,U1. ⬆*[1] T1 ≡ U1 →
+ ∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2, U2⦄ →
+ ∀p. ⦃L1, T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.U2⦄.
+#T1 #U1 #HTU1 #I1 #I2 #L1 #L2 #V1 #V2 #U2
+* #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p
+elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct
+elim (frees_total L2 V2) #g1 #Hg1
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1)
+[1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2
+lapply (sor_inv_sle_dx … Hg) #H0g
+/5 width=10 by frees_bind, sle_tl, sle_trans, ex4_4_intro/
+qed-.
elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
/4 width=12 by frees_flat, sor_inv_sle, sor_tls, ex4_4_intro/
qed.
-(*
+
+theorem fle_bind_eq: ∀L1,L2. |L1| = |L2| → ∀V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+ ∀I2,T1,T2. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
+ ∀p,I1. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
+#L1 #L2 #HL #V1 #V2
+* #n1 #m1 #f1 #g1 #Hf1 #Hg1 #H1L #Hfg1 #I2 #T1 #T2
+* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1
+elim (lveq_inj_length … H1L) // #H1 #H2 destruct
+elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct
+elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
+qed.
+
theorem fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
-#L1 #L2 #V1 #V2 #HV #I1 #I2 #T1 #T2 #HT #p
-@fle_bind_sn
-[ @fle_bind_dx_sn //
-| @fle_bind_dx_dx
-
-
+#L1 #L2 #V1 #V2
+* #n1 #m1 #f1 #g1 #Hf1 #Hg1 #H1L #Hfg1 #I1 #I2 #T1 #T2
+* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
+elim (lveq_inv_pair_pair … H2L) -H2L #H2L #H1 #H2 destruct
+elim (lveq_inj … H2L … H1L) -H1L #H1 #H2 destruct
elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/
+/4 width=15 by frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
qed.
-*)
+
theorem fle_flat: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
∀I1,I2. ⦃L1, ⓕ{I1}V1.T1⦄ ⊆ ⦃L2, ⓕ{I2}V2.T2⦄.
/2 width=8 by sle_refl, ex4_4_intro/
qed.
+lemma fle_sort_length: ∀L1,L2,s1,s2. |L1| = |L2| → ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄.
+/3 width=8 by lveq_length_eq, frees_sort, sle_refl, ex4_4_intro/ qed.
+
+lemma fle_gref_length: ∀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 fle_shift: ∀L1,L2. |L1| = |L2| →
+ ∀I,T1,T2,V. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I}V, T2⦄ →
+ ∀p. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2, ⓑ{p,I}V.T2⦄.
+#L1 #L2 #H1L #I #T1 #T2 #V
+* #n #m #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
+elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
+lapply (lveq_inv_bind … H2L) -H2L #HL
+elim (frees_total L2 V) #g1 #Hg1
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+lapply (sor_inv_sle_dx … Hg) #H0g
+/4 width=10 by frees_bind, lveq_void_sn, sle_tl, sle_trans, ex4_4_intro/
+qed.
+
lemma fle_bind_dx_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
∀p,I,T2. ⦃L1, V1⦄ ⊆ ⦃L2, ⓑ{p,I}V2.T2⦄.
#L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/lsubf_lsubr.ma".
+include "basic_2/static/fle.ma".
+
+(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
+
+(* Advanced forward lemmas ***************************************************)
+
+lemma fle_fwd_pair_sn: ∀I1,I2,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
+ ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄.
+#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 *
+#n1 #n2 #f1 #f2 #Hf1 #Hf2 #HL12 #Hf12
+elim (lveq_inv_pair_pair … HL12) -HL12 #HL12 #H1 #H2 destruct
+elim (frees_total (L1.ⓧ) T1) #g1 #Hg1
+lapply (lsubr_lsubf … Hg1 … Hf1) -Hf1 /2 width=1 by lsubr_unit/ #Hfg1
+/5 width=10 by lsubf_fwd_sle, lveq_bind, sle_trans, ex4_4_intro/ (**) (* full auto too slow *)
+qed-.
(* Advanced inversion lemmas ************************************************)
+lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ{I1} ≋ⓧ*[0, 0] K2.ⓘ{I2} → K1 ≋ⓧ*[0, 0] K2.
+#I1 #I2 #K1 #K2 #H
+elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct //
+qed-.
+
lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1, n2] ⋆ → ∧∧ 0 = n1 & 0 = n2.
* [2: #n1 ] * [2,4: #n2 ] #H
[ elim (lveq_inv_succ … H)
#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/
qed-.
+lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L1| ≤ |L2| → 0 = n1.
+#L1 #L2 #n1 #n2 #H #HL
+elim (lveq_fwd_length … H) -H
+>(eq_minus_O … HL) //
+qed-.
+
+lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| → 0 = n2.
+#L1 #L2 #n1 #n2 #H #HL
+elim (lveq_fwd_length … H) -H
+>(eq_minus_O … HL) //
+qed-.
+
lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
|L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
#L1 #L2 #n1 #n2 #H #HL
}
]
[ { "context-sensitive free variables" * } {
- [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ]
+ [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_lsubf" + "fle_fle" * ]
[ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
[ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ;
["c"; "𝕔"; "𝐜"; "ⓒ"; ] ;
- ["C"; "ℭ"; "∁"; "𝐂"; "Ⓒ"; ] ;
+ ["C"; "â\84"; "â\88\81"; "ð\9d\90\82"; "â\84\82"; "â\92¸"; ] ;
["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ;
["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ;
["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ;
projects / helm.git / commitdiff