From b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 24 Jan 2017 17:21:08 +0000 Subject: [PATCH] - updated equivalence on referred entries: it nust be degree-based - refactoring --- .../basic_2/{etc_new => etc}/ceq.etc | 0 .../basic_2/{etc_new => etc}/ceq_ceq.etc | 0 .../basic_2/{etc_new => etc}/cir/cir.etc | 0 .../basic_2/{etc_new => etc}/cir/cir_lift.etc | 0 .../cir/prednotreducible_3.etc | 0 .../basic_2/{etc_new => etc}/cix/cix.etc | 0 .../basic_2/{etc_new => etc}/cix/cix_lift.etc | 0 .../cix/prednotreducible_5.etc | 0 .../basic_2/{etc_new => etc}/cnr/cnr.etc | 0 .../basic_2/{etc_new => etc}/cnr/cnr_cir.etc | 0 .../basic_2/{etc_new => etc}/cnr/cnr_crr.etc | 0 .../basic_2/{etc_new => etc}/cnr/cnr_lift.etc | 0 .../{etc_new => etc}/cnr/prednormal_3.etc | 0 .../basic_2/{etc_new => etc}/cnx/cnx.etc | 0 .../basic_2/{etc_new => etc}/cnx/cnx_cix.etc | 0 .../basic_2/{etc_new => etc}/cnx/cnx_crx.etc | 0 .../basic_2/{etc_new => etc}/cnx/cnx_lift.etc | 0 .../{etc_new => etc}/cnx/prednormal_5.etc | 0 .../{etc_new => etc}/cpg/cpg_drops.etc | 0 .../{etc_new => etc}/cpg/cpg_length.etc | 0 .../basic_2/{etc_new => etc}/cpr/cpr.etc | 0 .../basic_2/{etc_new => etc}/cpr/cpr_cir.etc | 0 .../basic_2/{etc_new => etc}/cpx/cpx_cix.etc | 0 .../{etc_new => etc}/cpx/cpx_drops.etc | 0 .../{etc_new => etc}/cpx/cpx_length.etc | 0 .../basic_2/{etc_new => etc}/cpx/cpx_sta.etc | 0 .../basic_2/{etc_new => etc}/cpy/cpy.etc | 0 .../basic_2/{etc_new => etc}/cpy/cpy_cpy.etc | 0 .../basic_2/{etc_new => etc}/cpy/cpy_lift.etc | 0 .../{etc_new => etc}/cpy/cpy_nlift.etc | 0 .../basic_2/{etc_new => etc}/cpys/cpys.etc | 0 .../{etc_new => etc}/cpys/cpys_alt.etc | 0 .../{etc_new => etc}/cpys/cpys_cpys.etc | 0 .../{etc_new => etc}/cpys/cpys_lift.etc | 0 .../basic_2/{etc_new => etc}/crr/crr.etc | 0 .../basic_2/{etc_new => etc}/crr/crr_lift.etc | 0 .../{etc_new => etc}/crr/predreducible_3.etc | 0 .../basic_2/{etc_new => etc}/crx/crx.etc | 0 .../basic_2/{etc_new => etc}/crx/crx_lift.etc | 0 .../{etc_new => etc}/crx/predreducible_5.etc | 0 .../basic_2/{etc_new => etc}/da/da.etc | 0 .../basic_2/{etc_new => etc}/da/da_aaa.etc | 0 .../basic_2/{etc_new => etc}/da/da_da.etc | 0 .../basic_2/{etc_new => etc}/da/da_lift.etc | 0 .../basic_2/{etc_new => etc}/da/degree_6.etc | 0 .../basic_2/{etc_new => etc}/droppreds_3.etc | 0 .../basic_2/{etc_new => etc}/drops/drops.etc | 0 .../{etc_new => etc}/drops/drops_append.etc | 0 .../{etc_new => etc}/drops/drops_drops.etc | 0 .../{etc_new => etc}/drops/drops_length.etc | 0 .../basic_2/{etc_new => etc}/fqu/fqu.etc | 0 .../basic_2/{etc_new => etc}/fqu/fquq.etc | 0 .../basic_2/{etc_new => etc}/frees/frees.etc | 0 .../{etc_new => etc}/frees/frees_append.etc | 0 .../{etc_new => etc}/frees/frees_fqus.etc | 0 .../{etc_new => etc}/frees/frees_length.etc | 0 .../{etc_new => etc}/frees/frees_lift.etc | 0 .../basic_2/{etc_new => etc}/gget/gget.etc | 0 .../{etc_new => etc}/gget/gget_gget.etc | 0 .../basic_2/{etc_new => etc}/gget/rdrop_3.etc | 0 .../basic_2/{etc_new => etc}/lazyor_5.etc | 0 .../basic_2/{etc_new => etc}/lfpr_main.etc | 0 .../contribs/lambdadelta/basic_2/etc/lfxs.etc | 264 ++++++++++++++++++ .../lambdadelta/basic_2/etc/lfxs_drops.etc | 93 ++++++ .../lambdadelta/basic_2/etc/lfxs_fqup.etc | 24 ++ .../lambdadelta/basic_2/etc/lfxs_length.etc | 24 ++ .../lambdadelta/basic_2/etc/lfxs_lfxs.etc | 70 +++++ .../{etc_new => etc}/lifts/lifts_neg.etc | 0 .../basic_2/{etc_new => etc}/lleq/lleq.etc | 0 .../{etc_new => etc}/lleq/lleq_alt.etc | 0 .../{etc_new => etc}/lleq/lleq_alt_rec.etc | 0 .../{etc_new => etc}/lleq/lleq_drop.etc | 0 .../{etc_new => etc}/lleq/lleq_fqus.etc | 0 .../{etc_new => etc}/lleq/lleq_llor.etc | 0 .../{etc_new => etc}/lleq/lleq_lreq.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn_alt.etc | 0 .../llpx_sn/llpx_sn_alt_rec.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn_drop.etc | 0 .../llpx_sn/llpx_sn_frees.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn_llor.etc | 0 .../llpx_sn/llpx_sn_lpx_sn.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn_lreq.etc | 0 .../{etc_new => etc}/llpx_sn/llpx_sn_tc.etc | 0 .../basic_2/{etc_new => etc}/lpx/lpx_fquq.etc | 0 .../{etc_new => etc}/lpx_sn/lpx_sn_alt.etc | 0 .../{etc_new => etc}/lpx_sn/lpx_sn_tc.etc | 0 .../basic_2/{etc_new => etc}/lrsubeq_4.etc | 0 .../basic_2/{etc_new => etc}/lstas/lstas.etc | 0 .../{etc_new => etc}/lstas/lstas_aaa.etc | 0 .../{etc_new => etc}/lstas/lstas_da.etc | 0 .../{etc_new => etc}/lstas/lstas_lift.etc | 0 .../{etc_new => etc}/lstas/lstas_llpx_sn.etc | 0 .../{etc_new => etc}/lstas/lstas_lstas.etc | 0 .../lstas/statictypestar_6.etc | 0 .../{etc_new => etc}/lsubd/lrsubeqd_5.etc | 0 .../basic_2/{etc_new => etc}/lsubd/lsubd.etc | 0 .../{etc_new => etc}/lsubd/lsubd_da.etc | 0 .../{etc_new => etc}/lsubd/lsubd_lsubd.etc | 0 .../basic_2/{etc_new => etc}/lsuby/lsuby.etc | 0 .../{etc_new => etc}/lsuby/lsuby_lsuby.etc | 0 .../basic_2/{etc_new => etc}/ltls.etc | 0 .../basic_2/{etc_new => etc}/psubst_6.etc | 0 .../basic_2/{etc_new => etc}/psubststar_6.etc | 0 .../{etc_new => etc}/psubststaralt_6.etc | 0 .../{etc_new => etc}/unfold/unfold.etc | 0 .../{etc_new => etc}/unfold/unfold_4.etc | 0 .../basic_2/notation/relations/lazyeq_5.ma | 19 ++ .../relations/{lazyeq_6.ma => lazyeq_8.ma} | 4 +- .../lambdadelta/basic_2/relocation/lexs.ma | 15 +- .../lambdadelta/basic_2/static/aaa_lfdeq.ma | 45 +++ .../lambdadelta/basic_2/static/aaa_lfeq.ma | 42 --- .../basic_2/static/{ffeq.ma => ffdeq.ma} | 29 +- .../static/{ffeq_ffeq.ma => ffdeq_ffdeq.ma} | 24 +- .../lambdadelta/basic_2/static/ffdeq_fqup.ma | 23 ++ .../lambdadelta/basic_2/static/frees_lreq.ma | 40 --- .../lambdadelta/basic_2/static/lfdeq.ma | 170 +++++++++++ .../static/{lfeq_fqup.ma => lfdeq_fqup.ma} | 6 +- .../{lfeq_length.ma => lfdeq_length.ma} | 6 +- .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 54 ++++ .../lambdadelta/basic_2/static/lfeq.ma | 132 --------- .../lambdadelta/basic_2/static/lfeq_lfeq.ma | 55 ---- .../lambdadelta/basic_2/static/lfeq_lreq.ma | 36 --- .../lambdadelta/basic_2/static/lfxs.ma | 13 +- .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 12 + .../basic_2/syntax/{deq.ma => tdeq.ma} | 71 ++--- .../syntax/{deq_deq.ma => tdeq_tdeq.ma} | 12 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +- 128 files changed, 903 insertions(+), 392 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/ceq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/ceq_ceq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cir/cir.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cir/cir_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cir/prednotreducible_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cix/cix.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cix/cix_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cix/prednotreducible_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnr/cnr.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnr/cnr_cir.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnr/cnr_crr.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnr/cnr_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnr/prednormal_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnx/cnx.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnx/cnx_cix.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnx/cnx_crx.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnx/cnx_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cnx/prednormal_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpg/cpg_drops.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpg/cpg_length.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpr/cpr.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpr/cpr_cir.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpx/cpx_cix.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpx/cpx_drops.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpx/cpx_length.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpx/cpx_sta.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpy/cpy.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpy/cpy_cpy.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpy/cpy_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpy/cpy_nlift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpys/cpys.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpys/cpys_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpys/cpys_cpys.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/cpys/cpys_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crr/crr.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crr/crr_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crr/predreducible_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crx/crx.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crx/crx_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/crx/predreducible_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/da/da.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/da/da_aaa.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/da/da_da.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/da/da_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/da/degree_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/droppreds_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/drops/drops.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/drops/drops_append.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/drops/drops_drops.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/drops/drops_length.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/fqu/fqu.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/fqu/fquq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/frees/frees.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/frees/frees_append.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/frees/frees_fqus.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/frees/frees_length.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/frees/frees_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/gget/gget.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/gget/gget_gget.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/gget/rdrop_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lazyor_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lfpr_main.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lifts/lifts_neg.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_alt_rec.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_drop.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_fqus.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_llor.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lleq/lleq_lreq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_alt_rec.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_drop.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_frees.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_llor.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_lpx_sn.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_lreq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/llpx_sn/llpx_sn_tc.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lpx/lpx_fquq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lpx_sn/lpx_sn_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lpx_sn/lpx_sn_tc.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lrsubeq_4.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas_aaa.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas_da.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas_llpx_sn.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/lstas_lstas.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lstas/statictypestar_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsubd/lrsubeqd_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsubd/lsubd.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsubd/lsubd_da.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsubd/lsubd_lsubd.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsuby/lsuby.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/lsuby/lsuby_lsuby.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/ltls.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/psubst_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/psubststar_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/psubststaralt_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/unfold/unfold.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc_new => etc}/unfold/unfold_4.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeq_6.ma => lazyeq_8.ma} (87%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma rename matita/matita/contribs/lambdadelta/basic_2/static/{ffeq.ma => ffdeq.ma} (62%) rename matita/matita/contribs/lambdadelta/basic_2/static/{ffeq_ffeq.ma => ffdeq_ffdeq.ma} (57%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma rename matita/matita/contribs/lambdadelta/basic_2/static/{lfeq_fqup.ma => lfdeq_fqup.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/static/{lfeq_length.ma => lfdeq_length.ma} (85%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma rename matita/matita/contribs/lambdadelta/basic_2/syntax/{deq.ma => tdeq.ma} (50%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{deq_deq.ma => tdeq_tdeq.ma} (80%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/ceq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ceq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/ceq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/ceq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/ceq_ceq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ceq_ceq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/ceq_ceq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/ceq_ceq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cir/cir.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cir/cir.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cir/cir_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cir/cir_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/prednotreducible_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cir/prednotreducible_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/prednotreducible_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cir/prednotreducible_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cix/cix.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cix/cix.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cix/cix_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cix/cix_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/prednotreducible_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cix/prednotreducible_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/prednotreducible_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cix/prednotreducible_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_cir.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_cir.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_cir.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_cir.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_crr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_crr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_crr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_crr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/prednormal_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/prednormal_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/prednormal_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnr/prednormal_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_cix.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_cix.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_cix.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_cix.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_crx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_crx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_crx.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_crx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/prednormal_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/prednormal_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/prednormal_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnx/prednormal_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpg/cpg_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpg/cpg_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpg/cpg_drops.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpg/cpg_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpg/cpg_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpg/cpg_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpg/cpg_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpg/cpg_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr_cir.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_cir.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr_cir.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_cir.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_cix.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_cix.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_cix.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_cix.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_drops.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_sta.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_sta.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_cpy.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_cpy.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_cpy.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_nlift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_nlift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_nlift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy_nlift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crr/crr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crr/crr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crr/crr_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crr/crr_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/predreducible_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crr/predreducible_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/predreducible_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crr/predreducible_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crx/crx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crx/crx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crx/crx_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crx/crx_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/predreducible_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/crx/predreducible_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/predreducible_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/crx/predreducible_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/da/da.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/da/da.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/da/da_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/da/da_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_da.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/da/da_da.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_da.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/da/da_da.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/da/da_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/da/da_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/da/degree_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/da/degree_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/da/degree_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/da/degree_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/droppreds_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/droppreds_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_append.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_append.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_append.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fqu/fqu.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/fqu/fqu.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fquq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fqu/fquq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fquq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/fqu/fquq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_append.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_append.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_fqus.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_fqus.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_fqus.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/gget.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/gget/gget.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/gget.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/gget/gget.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/gget_gget.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/gget/gget_gget.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/gget_gget.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/gget/gget_gget.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/rdrop_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/gget/rdrop_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/gget/rdrop_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/gget/rdrop_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lazyor_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lazyor_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lazyor_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lazyor_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lfpr_main.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lfpr_main.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc new file mode 100644 index 000000000..f09a2cfc2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc @@ -0,0 +1,264 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/relocation/rtmap_id.ma". +include "basic_2/notation/relations/relationstar_4.ma". +include "basic_2/relocation/lexs.ma". +include "basic_2/static/frees.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +definition lfxs (R) (T): relation lenv ≝ + λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2. + +interpretation "generic extension on referred entries (local environment)" + 'RelationStar R T L1 L2 = (lfxs R T L1 L2). + +definition R_frees_confluent: predicate (relation3 lenv term term) ≝ + λRN. + ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 → + ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. + +definition lexs_frees_confluent: relation (relation3 lenv term term) ≝ + λRN,RP. + ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀L2. L1 ⦻*[RN, RP, f1] L2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. + +definition R_confluent2_lfxs: relation4 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RP1,RP2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. + +(* Basic properties ***********************************************************) + +lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. +/3 width=3 by lexs_atom, frees_atom, ex2_intro/ +qed. + +lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/ +qed. + +lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/ +qed. + +lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ +qed. + +lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/ +qed. + +lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. + L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 → + ∀V2. R L1 V V2 → + L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2. +#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR +/3 width=5 by lexs_pair_repl, ex2_intro/ +qed-. + +lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull → + (∀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 (H1R … Hf1 … HL12) -Hf1 +/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/ +qed-. + +lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. +#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. +#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ +qed-. + +lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. +#R #I #Y1 * /2 width=4 by lexs_inv_atom2/ +qed-. + +lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_sort … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_zero: ∀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. +#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_gref … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → + L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf +/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → + L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf +/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → + ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → + ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → + ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → + ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf +/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ +qed-. + +lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // +qed-. + +lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ +qed-. + +(* Basic_2A1: removed theorems 24: + llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref + llpx_sn_bind llpx_sn_flat + llpx_sn_inv_bind llpx_sn_inv_flat + llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length + llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx + llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc new file mode 100644 index 000000000..0a3f287bb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc @@ -0,0 +1,93 @@ +(**************************************************************************) +(* ___ *) +(* ||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/drops_ceq.ma". +include "basic_2/relocation/drops_lexs.ma". +include "basic_2/static/frees_drops.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +definition dedropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → + ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U → + ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + +definition dropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → + ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U → + ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2. + +definition dropable_dx: predicate (relation3 lenv term term) ≝ + λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 → + ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → + ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) +lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + d_liftable2 R → dedropable_sn R. +#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU +elim (frees_total L1 U) #f2 #Hf2 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf +elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 +/3 width=6 by cfull_lift, ex3_intro, ex2_intro/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) +(* Basic_2A1: was: llpx_sn_drop_conf_O *) +lemma lfxs_dropable_sn: ∀R. dropable_sn R. +#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU +elim (frees_total K1 T) #f1 #Hf1 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f +elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1 +/3 width=3 by ex2_intro/ +qed-. + +(* Basic_2A1: was: llpx_sn_drop_trans_O *) +(* Note: the proof might be simplified *) +lemma lfxs_dropable_dx: ∀R. dropable_dx R. +#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU +elim (drops_isuni_ex … H1f L1) #K1 #HLK1 +elim (frees_total K1 T) #f1 #Hf1 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f +elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 +/4 width=9 by frees_inv_lifts, ex2_intro/ +qed-. + +(* Basic_2A1: was: llpx_sn_inv_lift_O *) +lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → + ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → + ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. +#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU +elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY +lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // +qed-. + +lemma lfxs_inv_lref_sn: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. +#R #L1 #L2 #i #HL12 #I #K1 #V1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 // +#Y #HY #HLK2 elim (lfxs_inv_zero_pair_sn … HY) -HY +#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +lemma lfxs_inv_lref_dx: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. +#R #L1 #L2 #i #HL12 #I #K2 #V2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 // +#Y #HLK1 #HY elim (lfxs_inv_zero_pair_dx … HY) -HY +#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc new file mode 100644 index 000000000..62c5b0564 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Advanced properties ******************************************************) + +lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. +#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc new file mode 100644 index 000000000..01dd82cf4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Forward lemmas with length for local environments ************************) + +lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|. +#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc new file mode 100644 index 000000000..307740bea --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lexs.ma". +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/frees_frees.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Main properties **********************************************************) + +theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T. + L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 → + L1 ⦻*[R, ⓑ{p,I}V1.T] L2. +#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 +elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2)) +/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/ +qed. + +theorem lfxs_flat: ∀R,I,L1,L2,V,T. + L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 → + L1 ⦻*[R, ⓕ{I}V.T] L2. +#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) +/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ +qed. + +theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → + ∀T. Transitive … (lfxs R T). +#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 +elim (H1R … Hf1 … HL1) #f #H0 #H1 +lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2 +lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2 +lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 +@(ex2_intro … f) + +/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ +qed-. + +theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → + R_confluent2_lfxs R R R R → + ∀T. confluent … (lfxs R T). +#R #H1R #H2R #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 (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1 + elim (H1R … Hf … HL02) -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 #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02 + elim (frees_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 (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lifts/lifts_neg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lifts/lifts_neg.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lifts/lifts_neg.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lifts/lifts_neg.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt_rec.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_alt_rec.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt_rec.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_alt_rec.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_drop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_fqus.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_llor.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_llor.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_llor.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_lreq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lreq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_lreq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt_rec.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt_rec.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt_rec.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt_rec.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_frees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_frees.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_frees.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_frees.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_llor.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_llor.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_llor.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_lpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_lpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_lpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_lreq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_lreq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_lreq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_tc.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx/lpx_fquq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx/lpx_fquq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx/lpx_fquq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lrsubeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lrsubeq_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lrsubeq_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lrsubeq_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_da.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_da.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_da.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_da.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_llpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_llpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_llpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_lstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lstas.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/lstas_lstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/statictypestar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lstas/statictypestar_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/statictypestar_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lstas/statictypestar_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lrsubeqd_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lrsubeqd_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lrsubeqd_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lrsubeqd_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_da.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd_da.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_da.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd_da.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_lsubd.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd_lsubd.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_lsubd.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubd/lsubd_lsubd.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsuby/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsuby/lsuby.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lsuby/lsuby_lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lsuby/lsuby_lsuby.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/ltls.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ltls.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/ltls.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/ltls.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/psubst_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/psubst_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/psubst_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/psubst_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/psubststar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/psubststar_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/psubststar_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/psubststar_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/psubststaralt_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/psubststaralt_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/psubststaralt_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/psubststaralt_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/unfold/unfold.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/unfold/unfold.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/unfold/unfold_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/unfold/unfold_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma new file mode 100644 index 000000000..dd6a6046a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ≡ break [ term 46 h , term 46 o , term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEq $h $o $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma index eb25da48b..b4b796901 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'LazyEq $G1 $L1 $T1 $G2 $L2 $T2 }. + for @{ 'LazyEq $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index e99ea0393..4e0c82132 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -173,16 +173,23 @@ lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⦻*[RN, RP, f] #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) qed-. -(* Note: fexs_sym and fexs_trans hold, but lexs_sym and lexs_trans do not *) (* Basic_2A1: includes: lpx_sn_refl *) -lemma lexs_refl: ∀RN,RP,f. +lemma lexs_refl: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → - reflexive … (lexs RN RP f). -#RN #RP #f #HRN #HRP #L generalize in match f; -f elim L -L // + ∀f.reflexive … (lexs RN RP f). +#RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L // #L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/ qed. +lemma lexs_sym: ∀RN,RP. + (∀L1,L2,T1,T2. RN L1 T1 T2 → RN L2 T2 T1) → + (∀L1,L2,T1,T2. RP L1 T1 T2 → RP L2 T2 T1) → + ∀f. symmetric … (lexs RN RP f). +#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f +/3 width=2 by lexs_next, lexs_push/ +qed-. + lemma lexs_pair_repl: ∀RN,RP,f,I,L1,L2,V1,V2. L1.ⓑ{I}V1 ⦻*[RN, RP, f] L2.ⓑ{I}V2 → ∀W1,W2. RN L1 W1 W2 → RP L1 W1 W2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma new file mode 100644 index 000000000..cb6b1d180 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfdeq.ma". +include "basic_2/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties with degree-based equivalence on referred entries *************) + +lemma aaa_tdeq_conf_fldeq: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≡[h, o] T2 → + ∀L2. L1 ≡[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #G #L1 #s1 #X #H1 elim (tdeq_inv_sort1 … H1) -H1 // +| #I #G #L1 #V1 #B #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1 + #Y #H2 elim (lfdeq_inv_zero_pair_sn … H2) -H2 + #L2 #V2 #HL12 #HV12 #H2 destruct /3 width=1 by aaa_zero/ +| #I #G #L1 #V1 #A #i #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1 + #Y #H2 elim (lfdeq_inv_lref_pair_sn … H2) -H2 + #L2 #V2 #HL12 #H2 destruct /3 width=1 by aaa_lref/ +| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #H2 elim (lfdeq_inv_bind … H2) -H2 + /4 width=2 by aaa_abbr, lfdeq_pair_repl_dx/ +| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #H2 elim (lfdeq_inv_bind … H2) -H2 + /4 width=2 by aaa_abst, lfdeq_pair_repl_dx/ +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #H2 elim (lfdeq_inv_flat … H2) -H2 + /3 width=3 by aaa_appl/ +| #G #L1 #V1 #T1 #A #_ #_ #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #H2 elim (lfdeq_inv_flat … H2) -H2 + /3 width=1 by aaa_cast/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma deleted file mode 100644 index e5d7d0b5b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lfeq_lreq.ma". -include "basic_2/static/aaa.ma". - -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) - -(* Properties with equivalence on referred entries **************************) - -lemma lfeq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L1 ≡[T] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. -#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ -[ #I #G #L2 #V2 #A #_ #IH #L1 #H - elim (lfeq_inv_zero_pair_dx … H) -H /3 width=1 by aaa_zero/ -| #I #G #L2 #V2 #A #i #_ #IH #L1 #H - elim (lfeq_inv_lref_pair_dx … H) -H /3 width=1 by aaa_lref/ -| #p #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H - elim (lfeq_inv_bind … H) -H /3 width=2 by aaa_abbr/ -| #p #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H - elim (lfeq_inv_bind … H) -H /3 width=1 by aaa_abst/ -| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H - elim (lfeq_inv_flat … H) -H /3 width=3 by aaa_appl/ -| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H - elim (lfeq_inv_flat … H) -H /3 width=1 by aaa_cast/ -] -qed-. - -lemma aaa_lfeq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L2 ≡[T] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. -/3 width=3 by lfeq_aaa_trans, lfeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma similarity index 62% rename from matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index 48eb1ec0f..207e1e2d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -12,34 +12,31 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_6.ma". -include "basic_2/static/lfeq_lreq.ma". -include "basic_2/static/lfeq_fqup.ma". +include "basic_2/notation/relations/lazyeq_8.ma". +include "basic_2/syntax/genv.ma". +include "basic_2/static/lfdeq_fqup.ma". -(* EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *****************************) +(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) -inductive ffeq (G) (L1) (T): relation3 genv lenv term ≝ -| fleq_intro: ∀L2. L1 ≡[T] L2 → ffeq G L1 T G L2 T +inductive ffdeq (h) (o) (G) (L1) (T): relation3 genv lenv term ≝ +| ffdeq_intro: ∀L2. L1 ≡[h, o, T] L2 → ffdeq h o G L1 T G L2 T . interpretation - "equivalence on referred entries (closure)" - 'LazyEq G1 L1 T1 G2 L2 T2 = (ffeq G1 L1 T1 G2 L2 T2). + "degree-based equivalence on referred entries (closure)" + 'LazyEq h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma ffeq_refl: tri_reflexive … ffeq. -/2 width=1 by fleq_intro/ qed. - -lemma ffeq_sym: tri_symmetric … ffeq. -#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by fleq_intro, lfeq_sym/ +lemma ffdeq_sym: ∀h,o. tri_symmetric … (ffdeq h o). +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by ffdeq_intro, lfdeq_sym/ qed-. (* Basic inversion lemmas ***************************************************) -lemma ffeq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & L1 ≡[T1] L2 & T1 = T2. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ +lemma ffdeq_inv_gen: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≡[h, o, T1] L2 & T1 = T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ qed-. (* Basic_2A1: removed theorems 6: diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma similarity index 57% rename from matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma index e4a4cdd87..46400a913 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma @@ -12,22 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/static/lfeq_lfeq.ma". -include "basic_2/static/ffeq.ma". +include "basic_2/static/lfdeq_lfdeq.ma". +include "basic_2/static/ffdeq.ma". -(* EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *****************************) +(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) (* Main properties **********************************************************) -theorem ffeq_trans: tri_transitive … ffeq. -#G1 #G #L1 #L #T1 #T * -G -L -T -#L #HL1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by fleq_intro, lfeq_trans/ +theorem ffdeq_trans: ∀h,o. tri_transitive … (ffdeq h o). +#h #o #G1 #G #L1 #L #T1 #T * -G -L -T +#L #HL1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by ffdeq_intro, lfdeq_trans/ qed-. -theorem ffeq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. - ⦃G, L, T⦄ ≡ ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. -/3 width=5 by ffeq_trans, ffeq_sym/ qed-. +theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2. + ⦃G, L, T⦄ ≡[h, o] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by ffdeq_trans, ffdeq_sym/ qed-. -theorem ffeq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. - ⦃G1, L1, T1⦄ ≡ ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. -/3 width=5 by ffeq_trans, ffeq_sym/ qed-. +theorem ffdeq_canc_dx: ∀h,o,G1,G2,G,L1,L2,L,T1,T2,T. + ⦃G1, L1, T1⦄ ≡[h, o] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by ffdeq_trans, ffdeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma new file mode 100644 index 000000000..ab06d6d90 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfdeq_fqup.ma". +include "basic_2/static/ffdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) + +(* Advanced properties ******************************************************) + +lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o). +/2 width=1 by ffdeq_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma deleted file mode 100644 index 279ad0ca1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lreq.ma". -include "basic_2/static/frees.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -(* Properties with ranged equivalence for local environments ****************) - -lemma frees_lreq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. -#f #L1 #T #H elim H -f -L1 -T -[ #f #I #Hf #X #H lapply (lreq_inv_atom1 … H) -H - #H destruct /2 width=1 by frees_atom/ -| #f #I #L1 #V1 #s #_ #IH #X #H elim (lreq_inv_push1 … H) -H - /3 width=1 by frees_sort/ -| #f #I #L1 #V1 #_ #IH #X #H elim (lreq_inv_next1 … H) -H - /3 width=1 by frees_zero/ -| #f #I #L1 #V1 #i #_ #IH #X #H elim (lreq_inv_push1 … H) -H - /3 width=1 by frees_lref/ -| #f #I #L1 #V1 #l #_ #IH #X #H elim (lreq_inv_push1 … H) -H - /3 width=1 by frees_gref/ -| /6 width=5 by frees_bind, lreq_inv_tl, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/ -| /5 width=5 by frees_flat, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/ -] -qed-. - -lemma lreq_frees_trans: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L2 ≡[f] L1 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. -/3 width=3 by frees_lreq_conf, lreq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma new file mode 100644 index 000000000..e75c4e734 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -0,0 +1,170 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/lazyeq_5.ma". +include "basic_2/syntax/tdeq.ma". +include "basic_2/static/lfxs.ma". + +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) + +definition lfdeq: ∀h. sd h → relation3 term lenv lenv ≝ + λh,o. lfxs (cdeq h o). + +interpretation + "degree-based equivalence on referred entries (local environment)" + 'LazyEq h o T L1 L2 = (lfdeq h o T L1 L2). + +interpretation + "degree-based ranged equivalence (local environment)" + 'LazyEq h o f L1 L2 = (lexs (cdeq h o) cfull f L1 L2). +(* +definition lfdeq_transitive: predicate (relation3 lenv term term) ≝ + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[h, o, T1] L2 → R L1 T1 T2. +*) +(* Basic properties ***********************************************************) + +lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≡[h, o] T2 → + ∀L2. L1 ≡[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f. +#h #o #f #L1 #T1 #H elim H -f -L1 -T1 +[ #f #I1 #Hf #X #H1 elim (tdeq_fwd_atom1 … H1) -H1 + #I2 #H1 #Y #H2 lapply (lexs_inv_atom1 … H2) -H2 + #H2 destruct /2 width=1 by frees_atom/ +| #f #I #L1 #V1 #s1 #_ #IH #X #H1 elim (tdeq_inv_sort1 … H1) -H1 + #s2 #d #Hs1 #Hs2 #H1 #Y #H2 elim (lexs_inv_push1 … H2) -H2 + #L2 #V2 #HL12 #_ #H2 destruct /4 width=3 by frees_sort, tdeq_sort/ +| #f #I #L1 #V1 #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1 + #Y #H2 elim (lexs_inv_next1 … H2) -H2 + #L2 #V2 #HL12 #HV12 #H2 destruct /3 width=1 by frees_zero/ +| #f #I #L1 #V1 #i #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1 + #Y #H2 elim (lexs_inv_push1 … H2) -H2 + #L2 #V2 #HL12 #_ #H2 destruct /3 width=1 by frees_lref/ +| #f #I #L1 #V1 #l #_ #IH #X #H1 >(tdeq_inv_gref1 … H1) -H1 + #Y #H2 elim (lexs_inv_push1 … H2) -H2 + #L2 #V2 #HL12 #_ #H2 destruct /3 width=1 by frees_gref/ +| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct + /6 width=5 by frees_bind, lexs_inv_tl, sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn/ +| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1 + #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct + /5 width=5 by frees_flat, sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn/ +] +qed-. + +lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). +#h #o #T #L1 #L2 * +/4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/ +qed-. + +lemma lfdeq_atom: ∀h,o,I. ⋆ ≡[h, o, ⓪{I}] ⋆. +/2 width=1 by lfxs_atom/ qed. + +lemma lfdeq_sort: ∀h,o,I,L1,L2,V1,V2,s. + L1 ≡[h, o, ⋆s] L2 → L1.ⓑ{I}V1 ≡[h, o, ⋆s] L2.ⓑ{I}V2. +/2 width=1 by lfxs_sort/ qed. + +lemma lfdeq_zero: ∀h,o,I,L1,L2,V. + L1 ≡[h, o, V] L2 → L1.ⓑ{I}V ≡[h, o, #0] L2.ⓑ{I}V. +/2 width=1 by lfxs_zero/ qed. + +lemma lfdeq_lref: ∀h,o,I,L1,L2,V1,V2,i. + L1 ≡[h, o, #i] L2 → L1.ⓑ{I}V1 ≡[h, o, #⫯i] L2.ⓑ{I}V2. +/2 width=1 by lfxs_lref/ qed. + +lemma lfdeq_gref: ∀h,o,I,L1,L2,V1,V2,l. + L1 ≡[h, o, §l] L2 → L1.ⓑ{I}V1 ≡[h, o, §l] L2.ⓑ{I}V2. +/2 width=1 by lfxs_gref/ qed. + +lemma lfdeq_pair_repl_dx: ∀h,o,I,L1,L2.∀T:term.∀V,V1. + L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V1 → + ∀V2. V ≡[h, o] V2 → + L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V2. +/2 width=2 by lfxs_pair_repl_dx/ qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lfdeq_inv_atom_sn: ∀h,o,I,Y2. ⋆ ≡[h, o, ⓪{I}] Y2 → Y2 = ⋆. +/2 width=3 by lfxs_inv_atom_sn/ qed-. + +lemma lfdeq_inv_atom_dx: ∀h,o,I,Y1. Y1 ≡[h, o, ⓪{I}] ⋆ → Y1 = ⋆. +/2 width=3 by lfxs_inv_atom_dx/ qed-. + +lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * +/3 width=9 by ex4_5_intro, or_introl, or_intror, conj/ +qed-. + +lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +/2 width=1 by lfxs_inv_lref/ qed-. + +lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → + L1 ≡[h, o, V] L2 ∧ L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. +/2 width=2 by lfxs_inv_bind/ qed-. + +lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → + L1 ≡[h, o, V] L2 ∧ L1 ≡[h, o, T] L2. +/2 width=2 by lfxs_inv_flat/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfdeq_inv_zero_pair_sn: ∀h,o,I,Y2,L1,V1. L1.ⓑ{I}V1 ≡[h, o, #0] Y2 → + ∃∃L2,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & Y2 = L2.ⓑ{I}V2. +#h #o #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero_pair_sn … H) -H /2 width=5 by ex3_2_intro/ +qed-. + +lemma lfdeq_inv_zero_pair_dx: ∀h,o,I,Y1,L2,V2. Y1 ≡[h, o, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & Y1 = L1.ⓑ{I}V1. +#h #o #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero_pair_dx … H) -H +#L1 #V1 #HL12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +lemma lfdeq_inv_lref_pair_sn: ∀h,o,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ≡[h, o, #⫯i] Y2 → + ∃∃L2,V2. L1 ≡[h, o, #i] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_lref_pair_sn/ qed-. + +lemma lfdeq_inv_lref_pair_dx: ∀h,o,I,Y1,L2,V2,i. Y1 ≡[h, o, #⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≡[h, o, #i] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_lref_pair_dx/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfdeq_fwd_bind_sn: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1 ≡[h, o, V] L2. +/2 width=4 by lfxs_fwd_bind_sn/ qed-. + +lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T. + L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. +/2 width=2 by lfxs_fwd_bind_dx/ qed-. + +lemma lfdeq_fwd_flat_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, V] L2. +/2 width=3 by lfxs_fwd_flat_sn/ qed-. + +lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, T] L2. +/2 width=3 by lfxs_fwd_flat_dx/ qed-. + +lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. +/2 width=3 by lfxs_fwd_pair_sn/ qed-. + +(* Basic_2A1: removed theorems 30: + lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref + lleq_fwd_drop_sn lleq_fwd_drop_dx + lleq_fwd_bind_sn lleq_fwd_bind_dx lleq_fwd_flat_sn lleq_fwd_flat_dx + lleq_sort lleq_skip lleq_lref lleq_free lleq_gref lleq_bind lleq_flat + lleq_refl lleq_Y lleq_sym lleq_ge_up lleq_ge lleq_bind_O llpx_sn_lrefl + lleq_trans lleq_canc_sn lleq_canc_dx lleq_nlleq_trans nlleq_lleq_div +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma index bb513ab37..b6e2a18f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma @@ -13,11 +13,11 @@ (**************************************************************************) include "basic_2/static/lfxs_fqup.ma". -include "basic_2/static/lfeq.ma". +include "basic_2/static/lfdeq.ma". -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) (* Advanced properties ******************************************************) -lemma lfeq_refl: ∀T. reflexive … (lfeq T). +lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T). /2 width=1 by lfxs_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma similarity index 85% rename from matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index db2217702..d7c04b6ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -13,11 +13,11 @@ (**************************************************************************) include "basic_2/static/lfxs_length.ma". -include "basic_2/static/lfeq.ma". +include "basic_2/static/lfdeq.ma". -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) (* Forward lemmas with length for local environments ************************) -lemma lfeq_fwd_length: ∀L1,L2,T. L1 ≡[T] L2 → |L1| = |L2|. +lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma new file mode 100644 index 000000000..71b1c0d4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tdeq_tdeq.ma". +include "basic_2/static/lfxs_lfxs.ma". +include "basic_2/static/lfdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) + +(* Main properties **********************************************************) + +theorem lfdeq_bind: ∀h,o,p,I,L1,L2,V1,V2,T. + L1 ≡[h, o, V1] L2 → L1.ⓑ{I}V1 ≡[h, o, T] L2.ⓑ{I}V2 → + L1 ≡[h, o, ⓑ{p,I}V1.T] L2. +/2 width=2 by lfxs_bind/ qed. + +theorem lfdeq_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, V] L2 → L1 ≡[h, o, T] L2 → + L1 ≡[h, o, ⓕ{I}V.T] L2. +/2 width=1 by lfxs_flat/ qed. + +theorem lfdeq_trans: ∀h,o,T. Transitive … (lfdeq h o T). +#h #o #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 +lapply (frees_tdeq_conf_lexs … Hf1 T … HL1) // #H0 +lapply (frees_mono … Hf2 … H0) -Hf2 -H0 +/4 width=7 by lexs_trans, lexs_eq_repl_back, tdeq_trans, ex2_intro/ +qed-. + +theorem lfdeq_canc_sn: ∀h,o,T. left_cancellable … (lfdeq h o T). +/3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. + +theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T). +/3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. + +(* Advanced properies on negated lazy equivalence *****************************) + +(* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred ************) +lemma lfdeq_nlfdeq_trans: ∀h,o.∀T:term.∀L1,L. L1 ≡[h, o, T] L → + ∀L2. (L ≡[h, o, T] L2 → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). +/3 width=3 by lfdeq_canc_sn/ qed-. + +lemma nlfdeq_lfdeq_div: ∀h,o.∀T:term.∀L2,L. L2 ≡[h, o, T] L → + ∀L1. (L1 ≡[h, o, T] L → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). +/3 width=3 by lfdeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma deleted file mode 100644 index 1386a6a7d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma +++ /dev/null @@ -1,132 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/notation/relations/lazyeq_3.ma". -include "basic_2/static/lfxs.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) - -definition lfeq: relation3 term lenv lenv ≝ lfxs ceq. - -interpretation - "equivalence on referred entries (local environment)" - 'LazyEq T L1 L2 = (lfeq T L1 L2). - -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 properties ***********************************************************) - -lemma lfeq_atom: ∀I. ⋆ ≡[⓪{I}] ⋆. -/2 width=1 by lfxs_atom/ qed. - -lemma lfeq_sort: ∀I,L1,L2,V1,V2,s. - L1 ≡[⋆s] L2 → L1.ⓑ{I}V1 ≡[⋆s] L2.ⓑ{I}V2. -/2 width=1 by lfxs_sort/ qed. - -lemma lfeq_zero: ∀I,L1,L2,V. - L1 ≡[V] L2 → L1.ⓑ{I}V ≡[#0] L2.ⓑ{I}V. -/2 width=1 by lfxs_zero/ qed. - -lemma lfeq_lref: ∀I,L1,L2,V1,V2,i. - L1 ≡[#i] L2 → L1.ⓑ{I}V1 ≡[#⫯i] L2.ⓑ{I}V2. -/2 width=1 by lfxs_lref/ qed. - -lemma lfeq_gref: ∀I,L1,L2,V1,V2,l. - L1 ≡[§l] L2 → L1.ⓑ{I}V1 ≡[§l] L2.ⓑ{I}V2. -/2 width=1 by lfxs_gref/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lfeq_inv_atom_sn: ∀I,Y2. ⋆ ≡[⓪{I}] Y2 → Y2 = ⋆. -/2 width=3 by lfxs_inv_atom_sn/ qed-. - -lemma lfeq_inv_atom_dx: ∀I,Y1. Y1 ≡[⓪{I}] ⋆ → Y1 = ⋆. -/2 width=3 by lfxs_inv_atom_dx/ qed-. - -lemma lfeq_inv_zero: ∀Y1,Y2. Y1 ≡[#0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V. L1 ≡[V] L2 & - Y1 = L1.ⓑ{I}V & Y2 = L2.ⓑ{I}V. -#Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * -/3 width=7 by ex3_4_intro, or_introl, or_intror, conj/ -qed-. - -lemma lfeq_inv_lref: ∀Y1,Y2,i. Y1 ≡[#⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ≡[#i] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -/2 width=1 by lfxs_inv_lref/ qed-. - -lemma lfeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 → - L1 ≡[V] L2 ∧ L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. -/2 width=2 by lfxs_inv_bind/ qed-. - -lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → - L1 ≡[V] L2 ∧ L1 ≡[T] L2. -/2 width=2 by lfxs_inv_flat/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma lfeq_inv_zero_pair_sn: ∀I,Y2,L1,V. L1.ⓑ{I}V ≡[#0] Y2 → - ∃∃L2. L1 ≡[V] L2 & Y2 = L2.ⓑ{I}V. -#I #Y2 #L1 #V #H elim (lfxs_inv_zero_pair_sn … H) -H /2 width=3 by ex2_intro/ -qed-. - -lemma lfeq_inv_zero_pair_dx: ∀I,Y1,L2,V. Y1 ≡[#0] L2.ⓑ{I}V → - ∃∃L1. L1 ≡[V] L2 & Y1 = L1.ⓑ{I}V. -#I #Y1 #L2 #V #H elim (lfxs_inv_zero_pair_dx … H) -H -#L1 #X #HL12 #HX #H destruct /2 width=3 by ex2_intro/ -qed-. - -lemma lfeq_inv_lref_pair_sn: ∀I,Y2,L1,V1,i. L1.ⓑ{I}V1 ≡[#⫯i] Y2 → - ∃∃L2,V2. L1 ≡[#i] L2 & Y2 = L2.ⓑ{I}V2. -/2 width=2 by lfxs_inv_lref_pair_sn/ qed-. - -lemma lfeq_inv_lref_pair_dx: ∀I,Y1,L2,V2,i. Y1 ≡[#⫯i] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ≡[#i] L2 & Y1 = L1.ⓑ{I}V1. -/2 width=2 by lfxs_inv_lref_pair_dx/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lfeq_fwd_bind_sn: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 → L1 ≡[V] L2. -/2 width=4 by lfxs_fwd_bind_sn/ qed-. - -lemma lfeq_fwd_bind_dx: ∀p,I,L1,L2,V,T. - L1 ≡[ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. -/2 width=2 by lfxs_fwd_bind_dx/ qed-. - -lemma lfeq_fwd_flat_sn: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[V] L2. -/2 width=3 by lfxs_fwd_flat_sn/ qed-. - -lemma lfeq_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[T] L2. -/2 width=3 by lfxs_fwd_flat_dx/ qed-. - -lemma lfeq_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≡[②{I}V.T] L2 → L1 ≡[V] L2. -/2 width=3 by lfxs_fwd_pair_sn/ qed-. - -(* Advanceded forward lemmas with generic extension on referred entries *****) - -lemma lfex_fwd_lfxs_refl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2,T. L1 ≡[T] L2 → L1 ⦻*[R, T] L2. -/2 width=3 by lfxs_co/ qed-. - -(* Basic_2A1: removed theorems 30: - lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref - lleq_fwd_drop_sn lleq_fwd_drop_dx - lleq_fwd_bind_sn lleq_fwd_bind_dx lleq_fwd_flat_sn lleq_fwd_flat_dx - lleq_sort lleq_skip lleq_lref lleq_free lleq_gref lleq_bind lleq_flat - lleq_refl lleq_Y lleq_sym lleq_ge_up lleq_ge lleq_bind_O llpx_sn_lrefl - lleq_trans lleq_canc_sn lleq_canc_dx lleq_nlleq_trans nlleq_lleq_div -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma deleted file mode 100644 index 677f53973..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lreq_lreq.ma". -include "basic_2/static/lfxs_lfxs.ma". -include "basic_2/static/lfeq_lreq.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) - -(* Main properties **********************************************************) - -theorem lfeq_bind: ∀p,I,L1,L2,V1,V2,T. - L1 ≡[V1] L2 → L1.ⓑ{I}V1 ≡[T] L2.ⓑ{I}V2 → - L1 ≡[ⓑ{p,I}V1.T] L2. -/2 width=2 by lfxs_bind/ qed. - -theorem lfeq_flat: ∀I,L1,L2,V,T. L1 ≡[V] L2 → L1 ≡[T] L2 → - L1 ≡[ⓕ{I}V.T] L2. -/2 width=1 by lfxs_flat/ qed. - -(* Note: /2 width=3 by lfeq_lfxs_trans/ *) -theorem lfeq_trans: ∀T. Transitive … (lfeq T). -#T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 -lapply (frees_lreq_conf … Hf1 … HL1) #H0 -lapply (frees_mono … Hf2 … H0) -Hf2 -H0 -/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ -qed-. - -theorem lfeq_canc_sn: ∀T. left_cancellable … (lfeq T). -/3 width=3 by lfeq_trans, lfeq_sym/ qed-. - -theorem lfeq_canc_dx: ∀T. right_cancellable … (lfeq T). -/3 width=3 by lfeq_trans, lfeq_sym/ qed-. - -(* Advanced properies on negated lazy equivalence *****************************) - -(* Note: for use in auto, works with /4 width=8/ so lfeq_canc_sn is preferred *) -lemma lfeq_nlfeq_trans: ∀T,L1,L. L1 ≡[T] L → - ∀L2. (L ≡[T] L2 → ⊥) → (L1 ≡[T] L2 → ⊥). -/3 width=3 by lfeq_canc_sn/ qed-. - -lemma nlfeq_lfeq_div: ∀T,L2,L. L2 ≡[T] L → - ∀L1. (L1 ≡[T] L → ⊥) → (L1 ≡[T] L2 → ⊥). -/3 width=3 by lfeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma deleted file mode 100644 index fc902a4a3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma +++ /dev/null @@ -1,36 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lreq.ma". -include "basic_2/static/lfeq.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) - -(* Inversion lemmas with ranged equivalence for local environments **********) - -lemma lfeq_inv_lreq: ∀L1,L2,T. L1 ≡[T] L2 → ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ≡[f] L2. -#L1 #L2 #T * /2 width=3 by ex2_intro/ -qed-. - -(* Properties with ranged equivalence for local environments ****************) - -lemma lreq_lfeq: ∀f,L1,L2,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → L1 ≡[T] L2. -/2 width=3 by ex2_intro/ qed. - -(* Advanced properties ******************************************************) - -lemma lfeq_sym: ∀T. symmetric … (lfeq T). -#T #L1 #L2 #H elim (lfeq_inv_lreq … H) -H -/3 width=3 by lreq_lfeq, frees_lreq_conf, lreq_sym/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 92888ef46..a2f681634 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -77,6 +77,13 @@ lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. /3 width=5 by lexs_pair_repl, ex2_intro/ qed-. +lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull → + (∀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 (H1R … Hf1 … HL12) -Hf1 +/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/ +qed-. + lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ @@ -93,7 +100,7 @@ lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. qed-. lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 @@ -106,7 +113,7 @@ lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → qed-. lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * @@ -117,7 +124,7 @@ lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → qed-. lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * 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 26289760b..654ab4d0d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -35,7 +35,19 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T. #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ qed. +(* +theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → + ∀T. Transitive … (lfxs R T). +#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 +elim (H1R … Hf1 … HL1) #f #H0 #H1 +lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2 +lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2 +lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 +@(ex2_intro … f) +/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ +qed-. +*) theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → R_confluent2_lfxs R R R R → ∀T. confluent … (lfxs R T). diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/deq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma similarity index 50% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/deq.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index a14f7e3d8..b1658534c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/deq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -18,37 +18,37 @@ include "basic_2/syntax/lenv.ma". (* DEGREE-BASED EQUIVALENCE ON TERMS ****************************************) -inductive deq (h) (o): relation term ≝ -| deq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → deq h o (⋆s1) (⋆s2) -| deq_lref: ∀i. deq h o (#i) (#i) -| deq_gref: ∀l. deq h o (§l) (§l) -| deq_pair: ∀I,V1,V2,T1,T2. deq h o V1 V2 → deq h o T1 T2 → deq h o (②{I}V1.T1) (②{I}V2.T2) +inductive tdeq (h) (o): relation term ≝ +| tdeq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tdeq h o (⋆s1) (⋆s2) +| tdeq_lref: ∀i. tdeq h o (#i) (#i) +| tdeq_gref: ∀l. tdeq h o (§l) (§l) +| tdeq_pair: ∀I,V1,V2,T1,T2. tdeq h o V1 V2 → tdeq h o T1 T2 → tdeq h o (②{I}V1.T1) (②{I}V2.T2) . interpretation "degree-based equivalence (terms)" - 'LazyEq h o T1 T2 = (deq h o T1 T2). + 'LazyEq h o T1 T2 = (tdeq h o T1 T2). definition cdeq: ∀h. sd h → relation3 lenv term term ≝ - λh,o,L. deq h o. + λh,o,L. tdeq h o. (* Basic properties *********************************************************) -lemma deq_refl: ∀h,o. reflexive … (deq h o). -#h #o #T elim T -T /2 width=1 by deq_pair/ -* /2 width=1 by deq_lref, deq_gref/ -#s elim (deg_total h o s) /2 width=3 by deq_sort/ +lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o). +#h #o #T elim T -T /2 width=1 by tdeq_pair/ +* /2 width=1 by tdeq_lref, tdeq_gref/ +#s elim (deg_total h o s) /2 width=3 by tdeq_sort/ qed. -lemma deq_sym: ∀h,o. symmetric … (deq h o). +lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). #h #o #T1 #T2 #H elim H -T1 -T2 -/2 width=3 by deq_sort, deq_lref, deq_gref, deq_pair/ +/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ qed-. (* Basic inversion lemmas ***************************************************) -fact deq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → - ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. #h #o #X #Y * -X -Y [ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/ | #i #s #H destruct @@ -57,32 +57,32 @@ fact deq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → ] qed-. -lemma deq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → - ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. -/2 width=3 by deq_inv_sort1_aux/ qed-. +lemma tdeq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +/2 width=3 by tdeq_inv_sort1_aux/ qed-. -fact deq_inv_lref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀i. X = #i → Y = #i. +fact tdeq_inv_lref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀i. X = #i → Y = #i. #h #o #X #Y * -X -Y // [ #s1 #s2 #d #_ #_ #j #H destruct | #I #V1 #V2 #T1 #T2 #_ #_ #j #H destruct ] qed-. -lemma deq_inv_lref1: ∀h,o,Y,i. #i ≡[h, o] Y → Y = #i. -/2 width=5 by deq_inv_lref1_aux/ qed-. +lemma tdeq_inv_lref1: ∀h,o,Y,i. #i ≡[h, o] Y → Y = #i. +/2 width=5 by tdeq_inv_lref1_aux/ qed-. -fact deq_inv_gref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀l. X = §l → Y = §l. +fact tdeq_inv_gref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀l. X = §l → Y = §l. #h #o #X #Y * -X -Y // [ #s1 #s2 #d #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct ] qed-. -lemma deq_inv_gref1: ∀h,o,Y,l. §l ≡[h, o] Y → Y = §l. -/2 width=5 by deq_inv_gref1_aux/ qed-. +lemma tdeq_inv_gref1: ∀h,o,Y,l. §l ≡[h, o] Y → Y = §l. +/2 width=5 by tdeq_inv_gref1_aux/ qed-. -fact deq_inv_pair1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 → - ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. +fact tdeq_inv_pair1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 → + ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. #h #o #X #Y * -X -Y [ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct | #i #J #W1 #U1 #H destruct @@ -91,14 +91,21 @@ fact deq_inv_pair1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T ] qed-. -lemma deq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≡[h, o] Y → - ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. -/2 width=3 by deq_inv_pair1_aux/ qed-. +lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≡[h, o] Y → + ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. +/2 width=3 by tdeq_inv_pair1_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma deq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d → - ∃∃s2. deg h o s2 d & Y = ⋆s2. -#h #o #Y #s1 #H #d #Hs1 elim (deq_inv_sort1 … H) -H +lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d → + ∃∃s2. deg h o s2 d & Y = ⋆s2. +#h #o #Y #s1 #H #d #Hs1 elim (tdeq_inv_sort1 … H) -H #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≡[h, o] Y → ∃J. Y = ⓪{J}. +#h #o * #x #Y #H [ elim (tdeq_inv_sort1 … H) -H ] +/3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/deq_deq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma similarity index 80% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/deq_deq.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma index b69e2dc4e..39b06145c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/deq_deq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma @@ -12,19 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/syntax/deq.ma". +include "basic_2/syntax/tdeq.ma". (* DEGREE-BASED EQUIVALENCE ON TERMS ****************************************) (* Main properties **********************************************************) -theorem deq_trans: ∀h,o. Transitive … (deq h o). +theorem tdeq_trans: ∀h,o. Transitive … (tdeq h o). #h #o #T1 #T #H elim H -T1 -T [ #s1 #s #d #Hs1 #Hs #X #H - elim (deq_inv_sort1_deg … H … Hs) -s /2 width=3 by deq_sort/ -| #i1 #i #H <(deq_inv_lref1 … H) -H // -| #l1 #l #H <(deq_inv_gref1 … H) -H // + elim (tdeq_inv_sort1_deg … H … Hs) -s /2 width=3 by tdeq_sort/ +| #i1 #i #H <(tdeq_inv_lref1 … H) -H // +| #l1 #l #H <(tdeq_inv_gref1 … H) -H // | #I #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H destruct - elim (deq_inv_pair1 … H) -H /3 width=1 by deq_pair/ + elim (tdeq_inv_pair1 … H) -H /3 width=1 by tdeq_pair/ ] qed-. 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 cd88f565a..a0f7ae830 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 @@ -167,15 +167,15 @@ table { } ] [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfeq" + "aaa_aaa" * ] + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] } ] - [ { "equivalence for closures on referred entries" * } { - [ "ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "ffeq_freq" * ] + [ { "degree-based equivalence for closures on referred entries" * } { + [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] } ] - [ { "equivalence for local environments on referred entries" * } { - [ "lfeq ( ? ≡[?] ? )" "lfeq_length" + "lfeq_lreq" + "lfeq_fqup" + "lfeq_lfeq" * ] + [ { "degree-based equivalence for local environments on referred entries" * } { + [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ] } ] [ { "generic extension on referred entries" * } { @@ -187,7 +187,7 @@ table { } ] [ { "context-sensitive free variables" * } { - [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_fqup" + "frees_frees" * ] + [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ] } ] [ { "restricted ref. for local env." * } { -- 2.39.2