From e9f96fa56226dfd74de214c89d827de0c5018ac7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 16 Apr 2016 22:01:54 +0000 Subject: [PATCH] refactoring to park the notions: lstas, unfold, crr, cir, cnr, crx, cix, cnx --- .../lambdadelta/basic_2/{reduction/cir.ma => etc_new/cir/cir.etc} | 0 .../basic_2/{reduction/cir_lift.ma => etc_new/cir/cir_lift.etc} | 0 .../prednotreducible_3.ma => etc_new/cir/prednotreducible_3.etc} | 0 .../lambdadelta/basic_2/{reduction/cix.ma => etc_new/cix/cix.etc} | 0 .../basic_2/{reduction/cix_lift.ma => etc_new/cix/cix_lift.etc} | 0 .../prednotreducible_5.ma => etc_new/cix/prednotreducible_5.etc} | 0 .../lambdadelta/basic_2/{reduction/cnr.ma => etc_new/cnr/cnr.etc} | 0 .../basic_2/{reduction/cnr_cir.ma => etc_new/cnr/cnr_cir.etc} | 0 .../basic_2/{reduction/cnr_crr.ma => etc_new/cnr/cnr_crr.etc} | 0 .../basic_2/{reduction/cnr_lift.ma => etc_new/cnr/cnr_lift.etc} | 0 .../relations/prednormal_3.ma => etc_new/cnr/prednormal_3.etc} | 0 .../lambdadelta/basic_2/{reduction/cnx.ma => etc_new/cnx/cnx.etc} | 0 .../basic_2/{reduction/cnx_cix.ma => etc_new/cnx/cnx_cix.etc} | 0 .../basic_2/{reduction/cnx_crx.ma => etc_new/cnx/cnx_crx.etc} | 0 .../basic_2/{reduction/cnx_lift.ma => etc_new/cnx/cnx_lift.etc} | 0 .../relations/prednormal_5.ma => etc_new/cnx/prednormal_5.etc} | 0 .../lambdadelta/basic_2/{reduction/crr.ma => etc_new/crr/crr.etc} | 0 .../basic_2/{reduction/crr_lift.ma => etc_new/crr/crr_lift.etc} | 0 .../predreducible_3.ma => etc_new/crr/predreducible_3.etc} | 0 .../lambdadelta/basic_2/{reduction/crx.ma => etc_new/crx/crx.etc} | 0 .../basic_2/{reduction/crx_lift.ma => etc_new/crx/crx_lift.etc} | 0 .../predreducible_5.ma => etc_new/crx/predreducible_5.etc} | 0 .../basic_2/{unfold/lstas.ma => etc_new/lstas/lstas.etc} | 0 .../basic_2/{unfold/lstas_aaa.ma => etc_new/lstas/lstas_aaa.etc} | 0 .../basic_2/{unfold/lstas_da.ma => etc_new/lstas/lstas_da.etc} | 0 .../{unfold/lstas_lift.ma => etc_new/lstas/lstas_lift.etc} | 0 .../{unfold/lstas_llpx_sn.ma => etc_new/lstas/lstas_llpx_sn.etc} | 0 .../{unfold/lstas_lstas.ma => etc_new/lstas/lstas_lstas.etc} | 0 .../statictypestar_6.ma => etc_new/lstas/statictypestar_6.etc} | 0 .../basic_2/{unfold/unfold.ma => etc_new/unfold/unfold.etc} | 0 .../relations/unfold_4.ma => etc_new/unfold/unfold_4.etc} | 0 .../lambdadelta/basic_2/{computation => rt_computation}/cpre.ma | 0 .../basic_2/{computation => rt_computation}/cpre_cpre.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/cprs.ma | 0 .../basic_2/{computation => rt_computation}/cprs_cprs.ma | 0 .../basic_2/{computation => rt_computation}/cprs_lift.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/cpxe.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/cpxs.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_aaa.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_cpxs.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_lift.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_lleq.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_lreq.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_tsts.ma | 0 .../basic_2/{computation => rt_computation}/cpxs_tsts_vector.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/csx.ma | 0 .../basic_2/{computation => rt_computation}/csx_aaa.ma | 0 .../basic_2/{computation => rt_computation}/csx_alt.ma | 0 .../basic_2/{computation => rt_computation}/csx_fpbs.ma | 0 .../basic_2/{computation => rt_computation}/csx_lift.ma | 0 .../basic_2/{computation => rt_computation}/csx_lleq.ma | 0 .../basic_2/{computation => rt_computation}/csx_lpx.ma | 0 .../basic_2/{computation => rt_computation}/csx_lpxs.ma | 0 .../basic_2/{computation => rt_computation}/csx_tsts_vector.ma | 0 .../basic_2/{computation => rt_computation}/csx_vector.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/fpbg.ma | 0 .../basic_2/{computation => rt_computation}/fpbg_fleq.ma | 0 .../basic_2/{computation => rt_computation}/fpbg_fpbg.ma | 0 .../basic_2/{computation => rt_computation}/fpbg_fpbs.ma | 0 .../basic_2/{computation => rt_computation}/fpbg_lift.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/fpbs.ma | 0 .../basic_2/{computation => rt_computation}/fpbs_aaa.ma | 0 .../basic_2/{computation => rt_computation}/fpbs_alt.ma | 0 .../basic_2/{computation => rt_computation}/fpbs_fpb.ma | 0 .../basic_2/{computation => rt_computation}/fpbs_fpbs.ma | 0 .../basic_2/{computation => rt_computation}/fpbs_lift.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/fsb.ma | 0 .../basic_2/{computation => rt_computation}/fsb_aaa.ma | 0 .../basic_2/{computation => rt_computation}/fsb_alt.ma | 0 .../basic_2/{computation => rt_computation}/fsb_csx.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/gcp.ma | 0 .../basic_2/{computation => rt_computation}/gcp_aaa.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/gcp_cr.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/lcosx.ma | 0 .../basic_2/{computation => rt_computation}/lcosx_cpx.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/lprs.ma | 0 .../basic_2/{computation => rt_computation}/lprs_cprs.ma | 0 .../basic_2/{computation => rt_computation}/lprs_drop.ma | 0 .../basic_2/{computation => rt_computation}/lprs_lprs.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/lpxs.ma | 0 .../basic_2/{computation => rt_computation}/lpxs_aaa.ma | 0 .../basic_2/{computation => rt_computation}/lpxs_cpxs.ma | 0 .../basic_2/{computation => rt_computation}/lpxs_drop.ma | 0 .../basic_2/{computation => rt_computation}/lpxs_lleq.ma | 0 .../basic_2/{computation => rt_computation}/lpxs_lpxs.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/lsubc.ma | 0 .../basic_2/{computation => rt_computation}/lsubc_drop.ma | 0 .../basic_2/{computation => rt_computation}/lsubc_drops.ma | 0 .../basic_2/{computation => rt_computation}/lsubc_lsuba.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/lsx.ma | 0 .../basic_2/{computation => rt_computation}/lsx_alt.ma | 0 .../basic_2/{computation => rt_computation}/lsx_csx.ma | 0 .../basic_2/{computation => rt_computation}/lsx_drop.ma | 0 .../basic_2/{computation => rt_computation}/lsx_lpx.ma | 0 .../basic_2/{computation => rt_computation}/lsx_lpxs.ma | 0 .../lambdadelta/basic_2/{computation => rt_computation}/scpds.ma | 0 .../basic_2/{computation => rt_computation}/scpds_aaa.ma | 0 .../basic_2/{computation => rt_computation}/scpds_lift.ma | 0 .../basic_2/{computation => rt_computation}/scpds_scpds.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpr.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpr_cir.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpr_lift.ma | 0 .../basic_2/{reduction => rt_transition}/cpr_llpx_sn.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpx.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpx_cix.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpx_lift.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpx_lleq.ma | 0 .../basic_2/{reduction => rt_transition}/cpx_llpx_sn.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/cpx_lreq.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpb.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpb_fleq.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpb_lift.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpb_lleq.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpbq.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpbq_aaa.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpbq_alt.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/fpbq_lift.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpr.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpr_drop.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpr_lpr.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpx.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpx_aaa.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpx_drop.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpx_frees.ma | 0 .../lambdadelta/basic_2/{reduction => rt_transition}/lpx_lleq.ma | 0 125 files changed, 0 insertions(+), 0 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cir.ma => etc_new/cir/cir.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cir_lift.ma => etc_new/cir/cir_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/prednotreducible_3.ma => etc_new/cir/prednotreducible_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cix.ma => etc_new/cix/cix.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cix_lift.ma => etc_new/cix/cix_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/prednotreducible_5.ma => etc_new/cix/prednotreducible_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnr.ma => etc_new/cnr/cnr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnr_cir.ma => etc_new/cnr/cnr_cir.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnr_crr.ma => etc_new/cnr/cnr_crr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnr_lift.ma => etc_new/cnr/cnr_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/prednormal_3.ma => etc_new/cnr/prednormal_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnx.ma => etc_new/cnx/cnx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnx_cix.ma => etc_new/cnx/cnx_cix.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnx_crx.ma => etc_new/cnx/cnx_crx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cnx_lift.ma => etc_new/cnx/cnx_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/prednormal_5.ma => etc_new/cnx/prednormal_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/crr.ma => etc_new/crr/crr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/crr_lift.ma => etc_new/crr/crr_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predreducible_3.ma => etc_new/crr/predreducible_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/crx.ma => etc_new/crx/crx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/crx_lift.ma => etc_new/crx/crx_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predreducible_5.ma => etc_new/crx/predreducible_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas.ma => etc_new/lstas/lstas.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas_aaa.ma => etc_new/lstas/lstas_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas_da.ma => etc_new/lstas/lstas_da.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas_lift.ma => etc_new/lstas/lstas_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas_llpx_sn.ma => etc_new/lstas/lstas_llpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lstas_lstas.ma => etc_new/lstas/lstas_lstas.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/statictypestar_6.ma => etc_new/lstas/statictypestar_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/unfold.ma => etc_new/unfold/unfold.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/unfold_4.ma => etc_new/unfold/unfold_4.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpre.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpre_cpre.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cprs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cprs_cprs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cprs_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxe.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_cpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_lleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_lreq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_tsts.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/cpxs_tsts_vector.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_fpbs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_lleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_lpx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_lpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_tsts_vector.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/csx_vector.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbg.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbg_fleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbg_fpbg.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbg_fpbs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbg_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs_fpb.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs_fpbs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fpbs_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fsb.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fsb_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fsb_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/fsb_csx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/gcp.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/gcp_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/gcp_cr.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lcosx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lcosx_cpx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lprs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lprs_cprs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lprs_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lprs_lprs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs_cpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs_lleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lpxs_lpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsubc.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsubc_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsubc_drops.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsubc_lsuba.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx_csx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx_lpx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/lsx_lpxs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/scpds.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/scpds_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/scpds_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation => rt_computation}/scpds_scpds.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpr.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpr_cir.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpr_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpr_llpx_sn.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx_cix.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx_lleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx_llpx_sn.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/cpx_lreq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpb.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpb_fleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpb_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpb_lleq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpbq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpbq_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpbq_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/fpbq_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpr.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpr_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpr_lpr.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpx.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpx_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpx_drop.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpx_frees.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction => rt_transition}/lpx_lleq.ma (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/cir_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/prednotreducible_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cir/prednotreducible_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/cix_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/prednotreducible_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cix/prednotreducible_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_cir.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_cir.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_crr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_crr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/cnr_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/prednormal_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnr/prednormal_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_cix.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_cix.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_crx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_crx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/prednormal_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/prednormal_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/crr_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/predreducible_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crr/predreducible_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/crx_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/predreducible_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/crx/predreducible_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_da.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_da.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_llpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_llpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas_lstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/statictypestar_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/statictypestar_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_4.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxe.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxe.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lreq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lreq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpb.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_csx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_csx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_cir.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_cir.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_cix.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_cix.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lreq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lreq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_frees.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_frees.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_lleq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_lleq.ma -- 2.39.2