]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
- lambda_delta: programmed renaming to lambdadelta
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 25 Dec 2012 21:48:14 +0000 (21:48 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 25 Dec 2012 21:48:14 +0000 (21:48 +0000)
commite8998d29ab83e7b6aa495a079193705b2f6743d3
tree4d3e66f630a9e668c4f4a1a53ad8e2028f3ea7bf
parentbde429ac54e48de74b3d8b1df72dfcb86aa9bae5
- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta
605 files changed:
matita/matita/contribs/lambda_delta/Makefile [deleted file]
matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma [deleted file]
matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma [deleted file]
matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma [deleted file]
matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma [deleted file]
matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/basic_1.orig [deleted file]
matita/matita/contribs/lambda_delta/basic_2/basic_1.txt [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas_lift.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_cpcs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_ldrop.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_nta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_aaa.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_alt.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_lift.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpr.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_lift.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_ltpss.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sstas/sstas_sstas.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_lift.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_ltpss.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_sta.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.etc [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/names.txt [deleted file]
matita/matita/contribs/lambda_delta/basic_2/notation.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_dx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss_sn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/sd.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/sh.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta_aaa.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/arith.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/list.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/notation.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/star.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml [deleted file]
matita/matita/contribs/lambda_delta/ground_2/xoa.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma [deleted file]
matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma [deleted file]
matita/matita/contribs/lambda_delta/ma2etc.sh [deleted file]
matita/matita/contribs/lambda_delta/orig.sh [deleted file]
matita/matita/contribs/lambda_delta/replace.sh [deleted file]
matita/matita/contribs/lambda_delta/root [deleted file]
matita/matita/contribs/lambdadelta/Makefile [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/basic_1.orig [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/basic_1.txt [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_cpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/ypr.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_csups.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_xprs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/yprs_yprs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/csup/ysteps_csups.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/hod/ntas_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs_ltpr.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lenv_px_sn.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubn/lsubn_lsubn.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ssta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_cpcs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_ldrop.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/lsubn_nta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_aaa.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_alt.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpr.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_ltpss.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_nta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_thin.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_cpcs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_ldrop.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/lsubsn_snta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpr.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpss.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_snta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_thin.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_ltpss.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_sstas.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_ltpss.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/names.txt [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cif_append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/crf.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/crf_append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_fpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_lfpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/thnf.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/sd.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/sh.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp_frsupp.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/gr2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/arith.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/list.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/notation.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/star.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/xoa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ma2etc.sh [new file with mode: 0644]
matita/matita/contribs/lambdadelta/orig.sh [new file with mode: 0644]
matita/matita/contribs/lambdadelta/replace.sh [new file with mode: 0644]
matita/matita/contribs/lambdadelta/root [new file with mode: 0644]
matita/matita/lib/arithmetics/nat.ma