From 598a5c56535a8339f6533227ab580aff64e2d41c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 1 Jun 2014 21:49:56 +0000 Subject: [PATCH] - some refactoring and minor additions --- .../lambdadelta/apps_2/functional/lift.ma | 2 +- .../lambdadelta/basic_2/computation/acp.ma | 2 +- .../basic_2/computation/acp_aaa.ma | 4 +- .../lambdadelta/basic_2/computation/acp_cr.ma | 6 +- .../basic_2/computation/cpxs_lift.ma | 2 +- .../basic_2/computation/cpxs_tstc_vector.ma | 2 +- .../lambdadelta/basic_2/computation/fpbc.ma | 2 +- .../basic_2/computation/fpbc_fleq.ma | 2 +- .../lambdadelta/basic_2/computation/fpbs.ma | 2 +- .../basic_2/computation/fpbs_alt.ma | 4 +- .../basic_2/computation/fpbs_fleq.ma | 2 +- .../basic_2/computation/fpbu_fleq.ma | 2 +- .../basic_2/computation/fpbu_lleq.ma | 4 +- .../lambdadelta/basic_2/computation/lprs.ma | 2 +- .../lambdadelta/basic_2/computation/lsx.ma | 2 +- .../basic_2/computation/lsx_alt.ma | 2 +- .../basic_2/computation/lsx_ldrop.ma | 2 +- .../basic_2/computation/lsx_lpx.ma | 2 +- .../etc/{cofrees1 => cofrees}/cofrees.etc | 0 .../etc/{cofrees1 => cofrees}/cofrees_alt.etc | 0 .../{cofrees1 => cofrees}/cofrees_lift.etc | 0 .../{cofrees1 => cofrees}/cofreestar_4.etc | 0 .../basic_2/etc/cofrees0/cofrees.etc | 116 -------------- .../basic_2/etc/cofrees0/cofrees_alt.etc | 104 ------------ .../basic_2/etc/cofrees0/cofrees_lift.etc | 148 ------------------ .../basic_2/etc/cofrees0/cofreestar_3.etc | 19 --- .../{substitution => multiple}/cpys.ma | 2 +- .../{substitution => multiple}/cpys_alt.ma | 2 +- .../{substitution => multiple}/cpys_cpys.ma | 4 +- .../{substitution => multiple}/cpys_lift.ma | 4 +- .../{substitution => multiple}/fleq.ma | 2 +- .../{substitution => multiple}/fleq_fleq.ma | 4 +- .../{substitution => multiple}/fqup.ma | 2 +- .../{substitution => multiple}/fqup_fqup.ma | 2 +- .../{substitution => multiple}/fqus.ma | 4 +- .../{substitution => multiple}/fqus_alt.ma | 4 +- .../{substitution => multiple}/fqus_fqus.ma | 2 +- .../{substitution => multiple}/frees.ma | 4 +- .../{substitution => multiple}/frees_lift.ma | 4 +- .../basic_2/{substitution => multiple}/gr2.ma | 0 .../{substitution => multiple}/gr2_gr2.ma | 2 +- .../{substitution => multiple}/gr2_minus.ma | 2 +- .../{substitution => multiple}/gr2_plus.ma | 2 +- .../{substitution => multiple}/ldrops.ma | 6 +- .../ldrops_ldrop.ma | 4 +- .../ldrops_ldrops.ma | 2 +- .../{substitution => multiple}/lifts.ma | 4 +- .../{substitution => multiple}/lifts_lift.ma | 6 +- .../lifts_lift_vector.ma | 6 +- .../{substitution => multiple}/lifts_lifts.ma | 2 +- .../lifts_vector.ma | 4 +- .../{substitution => multiple}/lleq.ma | 2 +- .../{substitution => multiple}/lleq_alt.ma | 4 +- .../lleq_alt_rec.ma | 4 +- .../{substitution => multiple}/lleq_fqus.ma | 4 +- .../{substitution => multiple}/lleq_ldrop.ma | 4 +- .../{substitution => multiple}/lleq_leq.ma | 4 +- .../{substitution => multiple}/lleq_lleq.ma | 2 +- .../{substitution => multiple}/lleq_llor.ma | 4 +- .../{substitution => multiple}/llor.ma | 2 +- .../{substitution => multiple}/llor_ldrop.ma | 4 +- .../{substitution => multiple}/llpx_sn.ma | 2 +- .../{substitution => multiple}/llpx_sn_alt.ma | 4 +- .../llpx_sn_alt_rec.ma | 6 +- .../llpx_sn_ldrop.ma | 6 +- .../{substitution => multiple}/llpx_sn_leq.ma | 4 +- .../llpx_sn_llor.ma | 6 +- .../llpx_sn_lpx_sn.ma | 4 +- .../{substitution => multiple}/llpx_sn_tc.ma | 2 +- .../lambdadelta/basic_2/reduction/cpr_lift.ma | 2 +- .../basic_2/reduction/cpr_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_leq.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 4 +- .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 2 +- .../basic_2/reduction/cpx_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/crr.ma | 2 +- .../lambdadelta/basic_2/reduction/crr_lift.ma | 2 +- .../lambdadelta/basic_2/reduction/crx_lift.ma | 2 +- .../lambdadelta/basic_2/reduction/fpb.ma | 4 +- .../lambdadelta/basic_2/reduction/lpr.ma | 2 +- .../basic_2/reduction/lpr_ldrop.ma | 4 +- .../lambdadelta/basic_2/reduction/lpr_lpr.ma | 4 +- .../basic_2/reduction/lpx_frees.ma | 10 +- .../basic_2/reduction/lpx_ldrop.ma | 2 +- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 4 +- .../lambdadelta/basic_2/static/aaa.ma | 2 +- .../lambdadelta/basic_2/static/aaa_aaa.ma | 2 +- .../lambdadelta/basic_2/static/aaa_fqus.ma | 2 +- .../lambdadelta/basic_2/static/aaa_lift.ma | 2 +- .../lambdadelta/basic_2/static/aaa_lifts.ma | 2 +- .../lambdadelta/basic_2/static/aaa_lleq.ma | 2 +- .../contribs/lambdadelta/basic_2/static/da.ma | 2 +- .../lambdadelta/basic_2/static/da_lift.ma | 2 +- .../lambdadelta/basic_2/static/lsubr.ma | 2 +- .../basic_2/static/ssta_llpx_sn.ma | 2 +- .../{relocation => substitution}/cpy.ma | 2 +- .../{relocation => substitution}/cpy_cpy.ma | 2 +- .../{relocation => substitution}/cpy_lift.ma | 6 +- .../{relocation => substitution}/cpy_nlift.ma | 6 +- .../{relocation => substitution}/fqu.ma | 2 +- .../{relocation => substitution}/fquq.ma | 2 +- .../{relocation => substitution}/fquq_alt.ma | 2 +- .../{relocation => substitution}/gget.ma | 0 .../{relocation => substitution}/gget_gget.ma | 2 +- .../{relocation => substitution}/ldrop.ma | 2 +- .../ldrop_ldrop.ma | 4 +- .../{relocation => substitution}/ldrop_leq.ma | 2 +- .../{relocation => substitution}/lift.ma | 0 .../{relocation => substitution}/lift_lift.ma | 86 +++++----- .../lift_lift_vector.ma | 4 +- .../{relocation => substitution}/lift_neg.ma | 2 +- .../lift_vector.ma | 2 +- .../{relocation => substitution}/lpx_sn.ma | 0 .../lpx_sn_alt.ma | 4 +- .../lpx_sn_ldrop.ma | 4 +- .../lpx_sn_lpx_sn.ma | 2 +- .../{relocation => substitution}/lpx_sn_tc.ma | 2 +- .../{relocation => substitution}/lsuby.ma | 2 +- .../lsuby_lsuby.ma | 2 +- .../lambdadelta/basic_2/unfold/unfold.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../lambdadelta/ground_2/ynat/ynat_plus.ma | 14 +- 122 files changed, 213 insertions(+), 600 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/etc/{cofrees1 => cofrees}/cofrees.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{cofrees1 => cofrees}/cofrees_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{cofrees1 => cofrees}/cofrees_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{cofrees1 => cofrees}/cofreestar_4.etc (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofreestar_3.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/cpys.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/cpys_alt.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/cpys_cpys.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/cpys_lift.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fleq.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fleq_fleq.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fqup.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fqup_fqup.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fqus.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fqus_alt.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/fqus_fqus.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/frees.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/frees_lift.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/gr2.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/gr2_gr2.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/gr2_minus.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/gr2_plus.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/ldrops.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/ldrops_ldrop.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/ldrops_ldrops.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lifts.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lifts_lift.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lifts_lift_vector.ma (92%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lifts_lifts.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lifts_vector.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_alt.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_alt_rec.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_fqus.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_ldrop.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_leq.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_lleq.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/lleq_llor.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llor.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llor_ldrop.ma (93%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_alt.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_alt_rec.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_ldrop.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_leq.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_llor.ma (93%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_lpx_sn.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => multiple}/llpx_sn_tc.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/cpy.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/cpy_cpy.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/cpy_lift.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/cpy_nlift.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/fqu.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/fquq.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/fquq_alt.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/gget.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/gget_gget.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/ldrop.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/ldrop_ldrop.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/ldrop_leq.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lift_lift.ma (75%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lift_lift_vector.ma (94%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lift_neg.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lift_vector.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lpx_sn.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lpx_sn_alt.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lpx_sn_ldrop.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lpx_sn_lpx_sn.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lpx_sn_tc.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lsuby.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lsuby_lsuby.ma (97%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma index 634a7eb4a..4792a7ea5 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lift.ma". +include "basic_2/substitution/lift.ma". include "apps_2/functional/notation.ma". (* FUNCTIONAL RELOCATION ****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index 7830fa7c0..22efc2d11 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/genv.ma". -include "basic_2/substitution/ldrops.ma". +include "basic_2/multiple/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 13fbb93fe..7a232f0fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lifts_lifts.ma". -include "basic_2/substitution/ldrops_ldrops.ma". +include "basic_2/multiple/lifts_lifts.ma". +include "basic_2/multiple/ldrops_ldrops.ma". include "basic_2/static/aaa_lifts.ma". include "basic_2/static/aaa_aaa.ma". include "basic_2/computation/lsubc_ldrops.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index 7c6464f21..8bf08dc6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -14,9 +14,9 @@ include "basic_2/notation/relations/ineint_5.ma". include "basic_2/grammar/aarity.ma". -include "basic_2/substitution/gr2_gr2.ma". -include "basic_2/substitution/lifts_lift_vector.ma". -include "basic_2/substitution/ldrops_ldrop.ma". +include "basic_2/multiple/gr2_gr2.ma". +include "basic_2/multiple/lifts_lift_vector.ma". +include "basic_2/multiple/ldrops_ldrop.ma". include "basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 501bf323e..4a78a1b9b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fqus_fqus.ma". +include "basic_2/multiple/fqus_fqus.ma". include "basic_2/unfold/lsstas_lift.ma". include "basic_2/reduction/cpx_lift.ma". include "basic_2/computation/cpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index 41bd98df3..55ea0dff9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/tstc_vector.ma". -include "basic_2/relocation/lift_vector.ma". +include "basic_2/substitution/lift_vector.ma". include "basic_2/computation/cpxs_tstc.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma index 82ea6ec0f..f8797e72d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazybtpredproper_8.ma". -include "basic_2/substitution/fleq.ma". +include "basic_2/multiple/fleq.ma". include "basic_2/computation/fpbu.ma". (* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma index cf2ee2ffc..af496b60f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fleq_fleq.ma". +include "basic_2/multiple/fleq_fleq.ma". include "basic_2/computation/fpbu_fleq.ma". include "basic_2/computation/fpbc.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index c9f0875e4..2daaa8145 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstar_8.ma". -include "basic_2/substitution/fqus.ma". +include "basic_2/multiple/fqus.ma". include "basic_2/reduction/fpb.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/lpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index 047fd164a..254708616 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstaralt_8.ma". -include "basic_2/substitution/lleq_fqus.ma". -include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/multiple/lleq_fqus.ma". +include "basic_2/multiple/lleq_lleq.ma". include "basic_2/computation/cpxs_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/fpbs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma index 9f0c8d415..8987fcb57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fleq.ma". +include "basic_2/multiple/fleq.ma". include "basic_2/computation/fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma index c4e1813a9..8cf744d4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fleq.ma". +include "basic_2/multiple/fleq.ma". include "basic_2/computation/fpbs_alt.ma". include "basic_2/computation/fpbu_lleq.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma index e39e9d79e..6a9cf9d45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_fqus.ma". -include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/multiple/lleq_fqus.ma". +include "basic_2/multiple/lleq_lleq.ma". include "basic_2/computation/cpxs_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/fpbu.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma index c3d7203df..ddf4e24ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/predsnstar_3.ma". -include "basic_2/relocation/lpx_sn_tc.ma". +include "basic_2/substitution/lpx_sn_tc.ma". include "basic_2/reduction/lpr.ma". (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 0f47fe056..1abf9c523 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/sn_6.ma". -include "basic_2/substitution/lleq.ma". +include "basic_2/multiple/lleq.ma". include "basic_2/reduction/lpx.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma index 50b41adb2..a68fed0c2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/snalt_6.ma". -include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/multiple/lleq_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/lsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma index a520ba376..476680a16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/multiple/lleq_ldrop.ma". include "basic_2/reduction/lpx_ldrop.ma". include "basic_2/computation/lsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma index d191024b9..c4b2e04d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/multiple/lleq_lleq.ma". include "basic_2/reduction/lpx_lleq.ma". include "basic_2/computation/lsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_lift.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofrees_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofreestar_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofreestar_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofreestar_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cofrees/cofreestar_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees.etc deleted file mode 100644 index aa0ab9ec0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees.etc +++ /dev/null @@ -1,116 +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/cofreestar_3.ma". -include "basic_2/relocation/lift_neg.ma". -include "basic_2/substitution/cpys.ma". - -(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) - -definition cofrees: relation3 lenv nat term ≝ - λL,i,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶* U2 → ∃T2. ⇧[i, 1] T2 ≡ U2. - -interpretation - "context-sensitive exclusion from free variables (term)" - 'CoFreeStar L i U = (cofrees L i U). - -(* Basic forward lemmas *****************************************************) - -lemma cofrees_fwd_lift: ∀L,U,i. L ⊢ i ~ϵ 𝐅*⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U. -/2 width=1 by/ qed-. - -lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ~ϵ 𝐅*⦃W⦄. -#a #I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1 -#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/ -qed-. - -lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ → - L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄. -#a #I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1 -#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/ -qed-. - -lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ → - L ⊢ i ~ϵ 𝐅*⦃W⦄. -#I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1 -#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/ -qed-. - -lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ → - L ⊢ i ~ϵ 𝐅*⦃U⦄. -#I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1 -#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma cofrees_inv_gen: ∀L,U,U0,i. ⦃⋆, L⦄ ⊢ U ▶* U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) → - L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥. -#L #U #U0 #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U /2 width=2 by/ -qed-. - -lemma cofrees_inv_lref_eq: ∀L,i. L ⊢ i ~ϵ 𝐅*⦃#i⦄ → ⊥. -#L #i #H elim (H (#i)) -H // -#X #H elim (lift_inv_lref2_be … H) -H // -qed-. - -lemma cofrees_inv_bind: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄. -/3 width=7 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-. - -lemma cofrees_inv_flat: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ → - L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*⦃U⦄. -/3 width=6 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-. - -(* Basic Properties *********************************************************) - -lemma cofrees_sort: ∀L,i,k. L ⊢ i ~ϵ 𝐅*⦃⋆k⦄. -#L #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/ -qed. - -lemma cofrees_gref: ∀L,i,p. L ⊢ i ~ϵ 𝐅*⦃§p⦄. -#L #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/ -qed. - -lemma cofrees_bind: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → - ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → - ∀a. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄. -#L #W1 #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H -#W2 #U2 #HW12 #HU12 #H destruct -elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/ -qed. - -lemma cofrees_flat: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*⦃T⦄ → - ∀I. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄. -#L #W1 #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H -#W2 #U2 #HW12 #HU12 #H destruct -elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/ -qed. - -axiom cofrees_dec: ∀L,T,i. Decidable (L ⊢ i ~ϵ 𝐅*⦃T⦄). - -(* Basic negated inversion lemmas *******************************************) - -lemma frees_inv_bind: ∀a,I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄ → ⊥) → - (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → ⊥). -#a #I #L #W #U #i #H elim (cofrees_dec L W i) -/4 width=8 by cofrees_bind, or_intror, or_introl/ -qed-. - -lemma frees_inv_flat: ∀I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄ → ⊥) → - (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*⦃T⦄ → ⊥). -#I #L #W #U #i #H elim (cofrees_dec L W i) -/4 width=7 by cofrees_flat, or_intror, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc deleted file mode 100644 index 8443f38e3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc +++ /dev/null @@ -1,104 +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/lift_neg.ma". -include "basic_2/relocation/lift_lift.ma". -include "basic_2/substitution/cpys.ma". -include "basic_2/substitution/cofrees_lift.ma". - -(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) - -(* Alternative definition of frees_ge ***************************************) - -(* -lemma cpys_fwd_nlift2: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶* U2 → - ∀i. (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → - (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨ - ∃∃I,K,W,j. j < i & ⇩[j]L ≡ K.ⓑ{I}W & - (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥). -#G #L #U1 #U2 #H elim H -G -L -U1 -U2 -[ /3 width=2 by or_introl/ -| #I #G #L #K #V1 #V2 #W2 #j #HLK #_ #HVW2 #IHV12 #i #HnW2 - elim (lt_or_ge j i) #Hij - [ @or_intror (**) @(ex4_4_intro … HLK) // - [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // - #Y #HXY >minus_plus minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/ -] -qed-. - -lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term. - (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) → - (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) → - ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U. -#R #IH1 #IH2 #d #i #L #U -generalize in match d; -d generalize in match i; -i -@(f2_ind … rfw … L U) -L -U -#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/ --IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/ -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc deleted file mode 100644 index 02f227a7a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc +++ /dev/null @@ -1,148 +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/substitution/cpys_lift.ma". -include "basic_2/substitution/cofrees.ma". - -(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) - -(* Advanced inversion lemmas ************************************************) - -lemma cofrees_inv_lref_lt: ∀L,i,j. L ⊢ i ~ϵ 𝐅*⦃#j⦄ → j < i → - ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄. -#L #i #j #Hj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1)) -#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_delta/ -I -L -K -W1 -#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/ ->minus_plus minus_plus_plus_l // -| #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct - elim (cofrees_inv_flat … H1) -H1 #HW #HU - elim (nlift_inv_flat … H2) -H2 [ /3 width=7 by/ ] - #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *) -] -qed-. - -(* Advanced properties ******************************************************) - -lemma cofrees_lref_gt: ∀L,i,j. i < j → L ⊢ i ~ϵ 𝐅*⦃#j⦄. -#L #i #j #Hij #X #H elim (cpys_inv_lref1 … H) -H -[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/ -| * #I #K #V1 #V2 #_ #_ #H -I -L -K -V1 - elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/ -] -qed. - -lemma cofrees_lref_lt: ∀I,L,K,W,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W → - K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → L ⊢ i ~ϵ 𝐅*⦃#j⦄. -#I #L #K #W1 #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1 … H) -H -[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ -| * #I0 #K0 #W0 #W2 #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L - #H destruct elim (HW1 … HW12) -I -K -W1 - #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 // - >minus_plus minus_plus yplus_minus_assoc_inj /2 width=1 by yle_plus_to_minus_inj2/ ] -Hdedet #Hidete + [ >yplus_minus_assoc_inj /2 width=1 by yle_plus1_to_minus_inj2/ ] -Hdedet #Hidete elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV elim (lift_trans_le … HUV … HVW) -V // >minus_plus plus_plus_comm_23 in Hid2; #H lapply (le_plus_to_le_r … H) -H #H elim (le_inv_plus_l … H) -H #Hide2 #He2i lapply (transitive_le … Hd12 Hide2) -Hd12 #Hd12 - >le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); // -He2i - /4 width=3/ + >le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); + /4 width=3 by lift_lref_ge, ex2_intro/ ] | #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 - lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/ + lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3 by lift_gref, ex2_intro/ | #a #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct elim (IHW … HW2) // -IHW -HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2) /2 width=1/ /3 width=5/ + >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2) /3 width=5 by lift_bind, le_S_S, ex2_intro/ | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct elim (IHW … HW2) // -IHW -HW2 #W0 #HW2 #HW1 - elim (IHU … HU2) // /3 width=5/ + elim (IHU … HU2) /3 width=5 by lift_flat, ex2_intro/ ] qed. @@ -75,27 +75,27 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → e ≤ e1 → e1 ≤ e + e2 → ∃∃T0. ⇧[d1, e] T0 ≡ T2 & ⇧[d1, e + e2 - e1] T0 ≡ T1. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T -[ #k #d1 #e1 #e #e2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3/ +[ #k #d1 #e1 #e #e2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3 by lift_sort, ex2_intro/ | #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2 - >(lift_inv_lref2_lt … H) -H [ /3 width=3/ | /2 width=3/ ] + >(lift_inv_lref2_lt … H) -H /3 width=3 by lift_lref_lt, lt_plus_to_minus_r, lt_to_le_to_lt, ex2_intro/ | #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2 elim (lt_or_ge (i+e1) (d1+e+e2)) #Hie1d1e2 - [ elim (lift_inv_lref2_be … H) -H // /2 width=1/ + [ elim (lift_inv_lref2_be … H) -H /2 width=1 by le_plus/ | >(lift_inv_lref2_ge … H ?) -H // lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1 @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12 - @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1/ ] + @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1 by minus_le_minus_minus_comm/ ] ] -| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/ +| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct elim (IHV1 … HV2) -V // >plus_plus_comm_23 in HT2; #HT2 - elim (IHT1 … HT2) -T // -He1 -He1e2 /3 width=5/ + elim (IHT1 … HT2) -T /3 width=5 by lift_bind, ex2_intro/ | #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2 elim (lift_inv_flat2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct elim (IHV1 … HV2) -V // - elim (IHT1 … HT2) -T // -He1 -He1e2 /3 width=5/ + elim (IHT1 … HT2) -T /3 width=5 by lift_flat, ex2_intro/ ] qed. @@ -110,9 +110,9 @@ theorem lift_mono: ∀d,e,T,U1. ⇧[d,e] T ≡ U1 → ∀U2. ⇧[d,e] T ≡ U2 | #p #d #e #X #HX lapply (lift_inv_gref1 … HX) -HX // | #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ + elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX - elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1/ + elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ ] qed-. @@ -125,22 +125,22 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → >(lift_inv_sort1 … HT2) -HT2 // | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 - lapply (lift_inv_lref1_lt … HT2 Hid2) /2 width=1/ + lapply (lift_inv_lref1_lt … HT2 Hid2) /2 width=1 by lift_lref_lt/ | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21 lapply (lift_inv_lref1_ge … HT2 ?) -HT2 - [ @(transitive_le … Hd21 ?) -Hd21 /2 width=1/ - | -Hd21 /2 width=1/ + [ @(transitive_le … Hd21 ?) -Hd21 /2 width=1 by monotonic_le_plus_l/ + | -Hd21 /2 width=1 by lift_lref_ge/ ] | #p #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ >(lift_inv_gref1 … HT2) -HT2 // | #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 - elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2 width=1/ + lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, le_S_S/ (**) (* full auto a bit slow *) | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 - lapply (IHT12 … HT20 ? ?) // /2 width=1/ + lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_flat/ (**) (* full auto a bit slow *) ] qed. @@ -150,24 +150,24 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ∃∃T0. ⇧[d2, e2] T1 ≡ T0 & ⇧[d1 + e2, e1] T0 ≡ T2. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_sort1 … HX) -HX /2 width=3/ + >(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ lapply (lt_to_le_to_lt … (d1+e2) Hid1 ?) // #Hie2 - elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/ + elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /4 width=3 by lift_lref_ge_minus, lift_lref_lt, lt_minus_to_plus, monotonic_le_plus_l, ex2_intro/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21 lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2 - lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3/ #HX destruct - >plus_plus_comm_23 /4 width=3/ + lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3 by transitive_le/ #HX destruct + >plus_plus_comm_23 /4 width=3 by lift_lref_ge_minus, lift_lref_ge, monotonic_le_plus_l, ex2_intro/ | #p #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_gref1 … HX) -HX /2 width=3/ + >(lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // - elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1/ /3 width=5/ + elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_bind, le_S_S, ex2_intro/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // - elim (IHT12 … HT20) -IHT12 -HT20 // /3 width=5/ + elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_flat, ex2_intro/ ] qed. @@ -177,25 +177,25 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ∃∃T0. ⇧[d2 - e1, e2] T1 ≡ T0 & ⇧[d1, e1] T0 ≡ T2. #d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T [ #k #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_sort1 … HX) -HX /2 width=3/ + >(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hded lapply (lt_to_le_to_lt … (d1+e1) Hid1 ?) // #Hid1e - lapply (lt_to_le_to_lt … (d2-e1) Hid1 ?) /2 width=1/ #Hid2e + lapply (lt_to_le_to_lt … (d2-e1) Hid1 ?) /2 width=1 by le_plus_to_minus_r/ #Hid2e lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e -Hded #Hid2 - lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3/ + lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3 by lift_lref_lt, ex2_intro/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ - elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3/ + elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3 by lift_lref_lt, lift_lref_ge, monotonic_le_minus_l, lt_plus_to_minus_r, transitive_le, ex2_intro/ | #p #d1 #e1 #d2 #e2 #X #HX #_ - >(lift_inv_gref1 … HX) -HX /2 width=3/ + >(lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // - elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1/ #T -