From f7296f9cf2ee73465a374942c46b138f35c42ccb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Mar 2018 22:47:16 +0100 Subject: [PATCH] update in basic_2 + improved version of lfxs_trans_gen, now lfxs_trans_fsle based on an improved version of lexs_trans_gen + refactoring --- .../basic_2/i_static/tc_lfxs_lex.ma | 5 +- .../basic_2/i_static/tc_lfxs_tc_lfxs.ma | 2 +- .../lambdadelta/basic_2/relocation/lexs.ma | 20 +++---- .../basic_2/relocation/lexs_lexs.ma | 35 +++++++----- .../basic_2/rt_computation/lfpxs_lpxs.ma | 2 +- .../basic_2/rt_computation/lfsx_csx.ma | 45 +++++++++------- .../basic_2/rt_transition/cpm_fsle.ma | 8 +-- .../basic_2/rt_transition/lfpr_lfpr.ma | 2 +- .../basic_2/rt_transition/lfpx_fsle.ma | 12 ++--- .../basic_2/rt_transition/lfpx_lfdeq.ma | 10 ++-- .../lambdadelta/basic_2/static/fsle_fsle.ma | 9 ++++ .../basic_2/static/lfdeq_length.ma | 2 +- .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 2 +- .../lambdadelta/basic_2/static/lfeq.ma | 7 +-- .../static/{lfeq_lfeq.ma => lfeq_fsle.ma} | 21 +++++--- .../lambdadelta/basic_2/static/lfxs.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 18 +++++++ .../lambdadelta/basic_2/static/lfxs_fsle.ma | 38 ++++++++----- .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 53 ------------------- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 20 files changed, 153 insertions(+), 142 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/static/{lfeq_lfeq.ma => lfeq_fsle.ma} (63%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma index ea91a9578..e38f9f796 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma @@ -13,9 +13,8 @@ (**************************************************************************) 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/static/lfeq_fsle.ma". include "basic_2/i_static/tc_lfxs_fqup.ma". (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) @@ -37,7 +36,7 @@ lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R → (* 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 → - lfxs_fsle_compatible R → + lfxs_fsge_compatible R → s_rs_transitive … R (λ_.lex R) → lfeq_transitive R → ∀L1,L2,T. L1 ⪤**[R, T] L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma index 5e4a93933..dbcc54a3a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma @@ -19,7 +19,7 @@ include "basic_2/i_static/tc_lfxs.ma". (* Advanced properties ******************************************************) -lemma tc_lfxs_sym: ∀R. lfxs_fsle_compatible R → +lemma tc_lfxs_sym: ∀R. lfxs_fsge_compatible R → (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → ∀T. symmetric … (tc_lfxs R T). #R #H1R #H2R #T #L1 #L2 #H elim H -L2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index a58966696..291892f71 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -36,16 +36,18 @@ definition R_pw_confluent2_lexs: relation3 lenv bind bind → relation3 lenv bin relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 rtmap lenv bind ≝ - λR1,R2,RN1,RP1,RN2,RP2,f,L0,T0. - ∀T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. + ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → ∀L1. L0 ⪤*[RN1, RP1, f] L1 → ∀L2. L0 ⪤*[RN2, RP2, f] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. - -definition lexs_transitive: relation5 (relation3 lenv bind bind) - (relation3 lenv bind bind) … ≝ - λR1,R2,R3,RN,RP. - ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⪤*[RN, RP, f] L2 → - ∀T2. R2 L2 T T2 → R3 L1 T1 T2. + ∃∃I. R2 L1 I1 I & R1 L2 I2 I. + +definition lexs_transitive: relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,R3,RN,RP,f,L1,I1. + ∀I. R1 L1 I1 I → ∀L2. L1 ⪤*[RN, RP, f] L2 → + ∀I2. R2 L2 I I2 → R3 L1 I1 I2. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index 3ec8b4164..d4c2272f9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -19,24 +19,35 @@ include "basic_2/relocation/drops.ma". (* Main properties **********************************************************) -theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP) (f): - lexs_transitive RN1 RN2 RN RN1 RP1 → - lexs_transitive RP1 RP2 RP RN1 RP1 → - ∀L1,L0. L1 ⪤*[RN1, RP1, f] L0 → +theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP): + ∀L1,f. + (∀g,I,K,n. ⬇*[n] L1 ≡ K.ⓘ{I} → ⫯g = ⫱*[n] f → lexs_transitive RN1 RN2 RN RN1 RP1 g K I) → + (∀g,I,K,n. ⬇*[n] L1 ≡ K.ⓘ{I} → ↑g = ⫱*[n] f → lexs_transitive RP1 RP2 RP RN1 RP1 g K I) → + ∀L0. L1 ⪤*[RN1, RP1, f] L0 → ∀L2. L0 ⪤*[RN2, RP2, f] L2 → L1 ⪤*[RN, RP, f] L2. -#RN1 #RP1 #RN2 #RP2 #RN #RP #f #HN #HP #L1 #L0 #H elim H -f -L1 -L0 -[ #f #L2 #H >(lexs_inv_atom1 … H) -L2 // -| #f #I1 #I #K1 #K #HK1 #HI1 #IH #L2 #H elim (lexs_inv_next1 … H) -H - #I2 #K2 #HK2 #HI2 #H destruct /4 width=6 by lexs_next/ -| #f #I1 #I #K1 #K #HK1 #HI1 #IH #L2 #H elim (lexs_inv_push1 … H) -H - #I2 #K2 #HK2 #HI2 #H destruct /4 width=6 by lexs_push/ +#RN1 #RP1 #RN2 #RP2 #RN #RP #L1 elim L1 -L1 +[ #f #_ #_ #L0 #H1 #L2 #H2 + lapply (lexs_inv_atom1 … H1) -H1 #H destruct + lapply (lexs_inv_atom1 … H2) -H2 #H destruct + /2 width=1 by lexs_atom/ +| #K1 #I1 #IH #f elim (pn_split f) * #g #H destruct + #HN #HP #L0 #H1 #L2 #H2 + [ elim (lexs_inv_push1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct + elim (lexs_inv_push1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct + lapply (HP … 0 … HI10 … HK10 … HI02) -HI10 -HI02 /2 width=2 by drops_refl/ #HI12 + lapply (IH … HK10 … HK02) -IH -K0 /3 width=3 by lexs_push, drops_drop/ + | elim (lexs_inv_next1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct + elim (lexs_inv_next1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct + lapply (HN … 0 … HI10 … HK10 … HI02) -HI10 -HI02 /2 width=2 by drops_refl/ #HI12 + lapply (IH … HK10 … HK02) -IH -K0 /3 width=3 by lexs_next, drops_drop/ + ] ] qed-. (* Basic_2A1: includes: lpx_sn_trans *) -theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP → - lexs_transitive RP RP RP RN RP → +theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K I) → + (∀g,I,K. lexs_transitive RP RP RP RN RP g K I) → Transitive … (lexs RN RP f). /2 width=9 by lexs_trans_gen/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma index 746bc369e..79b41f785 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -33,4 +33,4 @@ lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. -/3 width=5 by lfpx_fsle_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. +/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma index 862858c4a..eb4418777 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma @@ -11,37 +11,46 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) - +(* include "basic_2/rt_computation/csx_cpxs.ma". include "basic_2/rt_computation/csx_lsubr.ma". +include "basic_2/rt_computation/lfsx_lpxs.ma". +*) include "basic_2/rt_computation/lsubsx_lfsx.ma". (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) +(* +axiom lpxs_trans: ∀h,G. Transitive … (lpxs h G). +*) (* Advanced properties ******************************************************) (* Basic_2A1: uses: lsx_lref_be_lpxs *) -lemma lfsx_pair_lfpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → - ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h, V] K2 → - ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄. +lemma lfsx_pair_lpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → + ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 → + ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄. #h #o #G #K1 #V #H @(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H -@(lfsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I -@lfsx_intro #Y #HY #HnY -elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct +@(lfsx_ind_lpxs … H) -K2 #K0 #HK0 #IHK0 #HK10 #I +@lfsx_intro_lpxs #Y #HY #HnY +elim (lpxs_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ] -[ /5 width=5 by lfsx_lfdeq_trans, lfpxs_step_dx, lfdeq_pair/ -| @lfsx_lfpx_trans - [2: @(IHV0 … HnV02 K0 … I) -IHV0 -HnV02 - [ /2 width=3 by lfpxs_cpx_trans/ - | /2 width=3 by lfsx_cpx_trans/ - | - ] - |1: skip - |3: @lfpx_pair /2 width=3 by lfpx_cpx_conf/ +[ /5 width=5 by lfsx_lfdeq_trans, lpxs_trans, lfdeq_pair/ +| @(IHV0 … HnV02) -IHV0 -HnV02 + [ + | /3 width=3 by lfsx_lpxs_trans, lfsx_cpxs_trans/ + | /2 width=3 by lpxs_trans/ ] -] -qed. + +(* + @(lfsx_lpxs_trans … (K0.ⓑ{I}V2)) + [ @(IHV0 … HnV02 … HK10) -IHV0 -HnV02 + [ + | /2 width=3 by lfsx_cpxs_trans/ + ] + | + ] +*) (* Basic_2A1: uses: lsx_lref_be *) lemma lfsx_lref_pair: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma index 604d922c7..32aeee69b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma @@ -19,11 +19,11 @@ include "basic_2/rt_transition/cpm_cpx.ma". (* 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 cpm_fsge_comp: ∀n,h,G. R_fsge_compatible (cpm n h G). +/3 width=6 by cpm_fwd_cpx, cpx_fsge_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-. +lemma lfpr_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpm 0 h G). +/4 width=5 by cpm_fwd_cpx, lfpx_fsge_comp, lfxs_co/ qed-. (* Properties with generic extension on referred entries ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index 8be2aa641..976060440 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -379,7 +379,7 @@ qed-. (* Main properties **********************************************************) theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T). -/3 width=6 by cpr_conf_lfpr, lfpr_fsle_comp, lfxs_conf/ qed-. +/3 width=6 by cpr_conf_lfpr, lfpr_fsge_comp, lfxs_conf/ qed-. theorem lfpr_bind: ∀h,G,L1,L2,V1. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → ∀I,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, T] L2.ⓑ{I}V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma index 47f8eb859..71f1c41d4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma @@ -26,7 +26,7 @@ include "basic_2/rt_transition/lfpx_fqup.ma". (* 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 → +lemma lfpx_cpx_conf_fsge: ∀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 * * @@ -114,19 +114,19 @@ lemma lfpx_cpx_conf_fsle: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → 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-. +lemma cpx_fsge_comp: ∀h,G. R_fsge_compatible (cpx h G). +/2 width=4 by lfpx_cpx_conf_fsge/ 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-. +lemma lfpx_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpx h G). +/2 width=4 by lfpx_cpx_conf_fsge/ 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-. +/3 width=3 by fsge_lfxs_trans, cpx_fsge_comp/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index c20039612..9dc71abaf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -22,19 +22,19 @@ include "basic_2/rt_transition/lfpx_fsle.ma". lemma lfpx_pair_sn_split: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ∀o,I,T. ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≛[h, o, V] L2. -/3 width=5 by lfpx_fsle_comp, lfxs_pair_sn_split/ qed-. +/3 width=5 by lfpx_fsge_comp, lfxs_pair_sn_split/ qed-. lemma lfpx_flat_dx_split: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∀o,I,V. ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≛[h, o, T] L2. -/3 width=5 by lfpx_fsle_comp, lfxs_flat_dx_split/ qed-. +/3 width=5 by lfpx_fsge_comp, lfxs_flat_dx_split/ qed-. lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p. ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V. -/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split/ qed-. +/3 width=5 by lfpx_fsge_comp, lfxs_bind_dx_split/ qed-. lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V. ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2. -/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split_void/ qed-. +/3 width=5 by lfpx_fsge_comp, lfxs_bind_dx_split_void/ qed-. lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). #h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ @@ -150,7 +150,7 @@ elim (cpx_lfdeq_conf … o … HT01 L2) -HT01 qed-. lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T). -/3 width=6 by lfpx_fsle_comp, lfdeq_fsle_comp, cpx_tdeq_conf_lexs, lfxs_conf/ qed-. +/3 width=6 by lfpx_fsge_comp, lfdeq_fsge_comp, cpx_tdeq_conf_lexs, lfxs_conf/ qed-. (* Basic_2A1: uses: lleq_lpx_trans *) lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma index deadd5cdc..9468fe1c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma @@ -39,6 +39,15 @@ elim (lveq_inj_length … H2L) // -L2 #H1 #H2 destruct /2 width=3 by ex2_intro/ qed-. +lemma fsle_inv_frees_eq: ∀L1,L2. |L1| = |L2| → + ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → + ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 → + f1 ⊆ f2. +#L1 #L2 #H1L #T1 #T2 #H2L #f1 #Hf1 #f2 #Hf2 +elim (fsle_frees_trans_eq … H2L … Hf2) // -L2 -T2 +/3 width=6 by frees_mono, sle_eq_repl_back1/ +qed-. + (* Main properties **********************************************************) theorem fsle_trans_sn: ∀L1,L2,T1,T. ⦃L1, T1⦄ ⊆ ⦃L2, T⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index 06fa93f19..02bdda0ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -21,7 +21,7 @@ include "basic_2/static/lfdeq.ma". (* Advanved properties with free variables inclusion ************************) -lemma lfdeq_fsle_comp: ∀h,o. lfxs_fsle_compatible (cdeq h o). +lemma lfdeq_fsge_comp: ∀h,o. lfxs_fsge_compatible (cdeq h o). #h #o #L1 #L2 #T * #f1 #Hf1 #HL12 lapply (frees_lfdeq_conf h o … Hf1 … HL12) lapply (lexs_fwd_length … HL12) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index 7326b418c..3dab077cf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -22,7 +22,7 @@ include "basic_2/static/lfdeq_length.ma". (* Basic_2A1: uses: lleq_sym *) lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). -/3 width=3 by lfdeq_fsle_comp, lfxs_sym, tdeq_sym/ qed-. +/3 width=3 by lfdeq_fsge_comp, lfxs_sym, tdeq_sym/ qed-. (* Basic_2A1: uses: lleq_dec *) lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma index 1ad709c9e..684e57370 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -25,15 +25,13 @@ interpretation "syntactic equivalence on referred entries (local environment)" 'LazyEqSn T L1 L2 = (lfeq T L1 L2). +(* Note: "lfeq_transitive R" is equivalent to "lfxs_transitive ceq R R" *) (* Basic_2A1: uses: lleq_transitive *) definition lfeq_transitive: predicate (relation3 lenv term term) ≝ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. (* Basic inversion lemmas ***************************************************) -lemma 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-. @@ -78,9 +76,6 @@ qed-. (* Basic_properties *********************************************************) -lemma lfxs_transitive_lfeq: ∀R. lfxs_transitive ceq R R → lfeq_transitive R. -/2 width=5 by/ qed. - lemma frees_lfeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. #f #L1 #T #H elim H -f -L1 -T diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma similarity index 63% rename from matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma index 8fd1f2f4f..0f80c9772 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma @@ -12,15 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/static/lfxs_lfxs.ma". +include "basic_2/static/lfxs_length.ma". +include "basic_2/static/lfxs_fsle.ma". include "basic_2/static/lfeq.ma". (* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) -(* Advanced forward lemmas **************************************************) +(* Properties with free variables inclusion for restricted closures *********) -(* Note: the proof should may invoke lfeq_transitive_inv_lfxs *) -lemma lfeq_lfxs_trans: ∀R. c_reflexive … R → lfeq_transitive R → - ∀L1,L,T. L1 ≡[T] L → - ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. -/3 width=9 by lfxs_trans_gen/ qed-. +lemma lfeq_fsle_comp: lfxs_fsle_compatible ceq. +#L1 #L2 #T #HL12 +elim (frees_total L1 T) +/4 width=8 by frees_lfeq_conf, lfxs_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/ +qed. + +(* Forward lemmas with free variables inclusion for restricted closures *****) + +lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R → + ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. +/4 width=16 by lfeq_fsle_comp, lfxs_trans_fsle, lfxs_trans_next/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index f3f64b5ff..f2ab35f91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -38,7 +38,7 @@ definition lfxs_confluent: relation … ≝ ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V → ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2. -definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝ +definition lfxs_transitive: relation3 ? (relation3 ?? term) … ≝ λR1,R2,R3. ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 99b1ece94..03772d98c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -34,6 +34,11 @@ definition dropable_dx: predicate (relation3 lenv term term) ≝ ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⪤*[R, T] K2. +definition lfxs_transitive_next: relation3 … ≝ λR1,R2,R3. + ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → + ∀g,I,K,n. ⬇*[n] L ≡ K.ⓘ{I} → ⫯g = ⫱*[n] f → + lexs_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I. + (* Properties with generic slicing for local environments *******************) lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) → @@ -45,6 +50,19 @@ elim (lexs_liftable_co_dedropable_sn … HLK1 … HK12 … Hf) -f1 -K1 /3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, ex3_intro, ex2_intro/ qed-. +lemma lfxs_trans_next: ∀R1,R2,R3. lfxs_transitive R1 R2 R3 → lfxs_transitive_next R1 R2 R3. +#R1 #R2 #R3 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H +generalize in match HLK; -HLK elim H -I1 -I +[ #I #_ #L2 #_ #I2 #H + lapply (ext2_inv_unit_sn … H) -H #H destruct + /2 width=1 by ext2_unit/ +| #I #V1 #V #HV1 #HLK1 #L2 #HL12 #I2 #H + elim (ext2_inv_pair_sn … H) -H #V2 #HV2 #H destruct + elim (frees_inv_drops_next … Hf … HLK1 … Hgf) -f -HLK1 #f #Hf #Hfg + /5 width=5 by ext2_pair, sle_lexs_trans, ex2_intro/ +] +qed. + (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma index cc7218982..011748dbf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma @@ -13,21 +13,24 @@ (**************************************************************************) 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_drops.ma". include "basic_2/static/lfxs_lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) -definition R_fsle_compatible: predicate (relation3 …) ≝ λRN. +definition R_fsge_compatible: predicate (relation3 …) ≝ λRN. ∀L,T1,T2. RN L T1 T2 → ⦃L, T2⦄ ⊆ ⦃L, T1⦄. -definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN. +definition lfxs_fsge_compatible: predicate (relation3 …) ≝ λRN. ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄. +definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN. + ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L1, T⦄ ⊆ ⦃L2, T⦄. + (* Basic inversions with free variables inclusion for restricted closures ***) -lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R → +lemma frees_lexs_conf: ∀R. lfxs_fsge_compatible R → ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 → ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. @@ -39,14 +42,14 @@ 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⦄ → +lemma fsge_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 → +lemma lfxs_sym: ∀R. lfxs_fsge_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 @@ -56,7 +59,7 @@ elim (frees_lexs_conf … Hf1 … HL12) -Hf1 // qed-. lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → + lfxs_fsge_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 @@ -75,7 +78,7 @@ elim (frees_lexs_conf … Hf … H) -Hf -H qed-. lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → + lfxs_fsge_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 @@ -91,7 +94,7 @@ elim (frees_lexs_conf … Hf … H) -Hf -H qed-. lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → + lfxs_fsge_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 @@ -111,7 +114,7 @@ elim (frees_lexs_conf … Hf … H0) -Hf -H0 qed-. lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → + lfxs_fsge_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 @@ -133,8 +136,8 @@ qed-. (* Main properties with free variables inclusion for restricted closures ****) theorem lfxs_conf: ∀R1,R2. - lfxs_fsle_compatible R1 → - lfxs_fsle_compatible R2 → + lfxs_fsge_compatible R1 → + lfxs_fsge_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 @@ -160,3 +163,14 @@ elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] ] ] qed-. + +theorem lfxs_trans_fsle: ∀R1,R2,R3. + lfxs_fsle_compatible R1 → lfxs_transitive_next R1 R2 R3 → + ∀L1,L,T. L1 ⪤*[R1, T] L → + ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2. +#R1 #R2 #R3 #H1R #H2R #L1 #L #T #H +lapply (H1R … H) -H1R #H0 +cases H -H #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 +lapply (fsle_inv_frees_eq … H0 … Hf1 … Hf2) -H0 -Hf2 +/4 width=14 by lexs_trans_gen, lexs_fwd_length, sle_lexs_trans, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 115d509ba..3b5982899 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -63,59 +63,6 @@ lapply (lexs_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2)) /3 width=7 by frees_fwd_isfin, frees_bind_void, lexs_join, isfin_tl, 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 → - ∀L1,T,L. L1 ⪤*[R1, T] L → - ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2. -#R1 #R2 #R3 #H1R #H2R #H3R #H4R #L1 #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L1 T) -L1 -T -#G0 #L0 #T0 #IH #G #L1 * * -[ #s #HG #HL #HT #L #H1 #L2 #H2 destruct - elim (lfxs_inv_sort … H1) -H1 * - [ #H1 #H0 destruct - >(lfxs_inv_atom_sn … H2) -L2 // - | #I1 #I #K1 #K #HK1 #H1 #H0 destruct - elim (lfxs_inv_sort_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct - /4 width=3 by lfxs_sort, fqu_fqup/ - ] -| * [ | #i ] #HG #HL #HT #L #H1 #L2 #H2 destruct - [ elim (lfxs_inv_zero … H1) -H1 * - [ #H1 #H0 destruct - >(lfxs_inv_atom_sn … H2) -L2 // - | #I #K1 #K #V1 #V #HK1 #H1 #H0 #H destruct - elim (lfxs_inv_zero_pair_sn … H2) -H2 #K2 #V2 #HK2 #HV2 #H destruct - /4 width=7 by lfxs_pair, fqu_fqup, fqu_lref_O/ - | #f1 #I #K1 #K #Hf1 #HK1 #H1 #H0 destruct - elim (lfxs_inv_zero_unit_sn … H2) -H2 #f2 #K2 #Hf2 #HK2 #H destruct - /5 width=8 by lfxs_unit, lexs_trans_id_cfull, lexs_eq_repl_back, isid_inv_eq_repl/ - ] - | elim (lfxs_inv_lref … H1) -H1 * - [ #H1 #H0 destruct - >(lfxs_inv_atom_sn … H2) -L2 // - | #I1 #I #K1 #K #HK1 #H1 #H0 destruct - elim (lfxs_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct - /4 width=3 by lfxs_lref, fqu_fqup/ - ] - ] -| #l #HG #HL #HT #L #H1 #L2 #H2 destruct - elim (lfxs_inv_gref … H1) -H1 * - [ #H1 #H0 destruct - >(lfxs_inv_atom_sn … H2) -L2 // - | #I1 #I #K1 #K #HK1 #H1 #H0 destruct - elim (lfxs_inv_gref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct - /4 width=3 by lfxs_gref, fqu_fqup/ - ] -| #p #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct - elim (lfxs_inv_bind … V1 V1 … H1) -H1 // #H1V #H1T - elim (lfxs_inv_bind … V1 V1 … H2) -H2 // #H2V #H2T - /3 width=4 by lfxs_bind/ -| #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct - elim (lfxs_inv_flat … H1) -H1 #H1V #H1T - elim (lfxs_inv_flat … H2) -H2 #H2V #H2T - /3 width=3 by lfxs_flat/ -] -qed-. - (* Negated inversion lemmas *************************************************) (* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 3a40bb09a..f35756078 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -177,7 +177,7 @@ table { } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] + [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ] } ] [ { "generic extension of a context-sensitive relation" * } { -- 2.39.2