]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma
update in ground_2, static_2, basic_2, apps_2, alpha_1
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Wed, 8 Jan 2020 21:39:47 +0000 (22:39 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Wed, 8 Jan 2020 21:39:47 +0000 (22:39 +0100)
commitbd53c4e895203eb049e75434f638f26b5a161a2b
tree2602b57dddd42985e1274f6ef4647fd7282f55fc
parent3b7b8afcb429a60d716d5226a5b6ab0d003228b1
update in ground_2, static_2, basic_2, apps_2, alpha_1

+ updated notation with uniform bracket policy
+ notation update for acr
+ some renaming in alpha_1
485 files changed:
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma
matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma
matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma
matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma
matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma
matita/matita/contribs/lambdadelta/apps_2/models/li.ma
matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma
matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma
matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_5.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmre.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpmre.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpts.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_ntas.ma
matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/colon_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/colonstar_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/exclaim_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalwstar_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pty_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/ptystar_6.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_cprre.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cnr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc.ma
matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpes.ma
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpms.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_fqu.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fquq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fquq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rpx.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/notation/functions/apply_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/basic_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/cocompose_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/semicolon_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/uniform_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/uparrowstar_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/functions/upspoonstar_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/isdivergent_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/isfinite_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/isidentity_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/isredtype_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/istotal_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/istype_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcoafter_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_2.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isdiv.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_max.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_shift.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
matita/matita/contribs/lambdadelta/static_2/i_static/rexs.ma
matita/matita/contribs/lambdadelta/static_2/i_static/rexs_drops.ma
matita/matita/contribs/lambdadelta/static_2/i_static/rexs_fqup.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/dxbind1_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/dxbind2_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/dxitem_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/item0_1.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabbr_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabbrneg_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabbrpos_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabst_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabstneg_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snabstpos_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snbind1_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snbind2_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snbind2_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snbind2neg_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snbind2pos_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snflat2_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snitem2_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/snitem_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/weight_1.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/weight_2.ma
matita/matita/contribs/lambdadelta/static_2/notation/functions/weight_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/atomicarity_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/freeplus_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/ideqsn_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/ineint_5.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/notation/relations/inwbrackets_5.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/lrsubeqa_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/lrsubeqc_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/lrsubeqf_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/rdropstar_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/rdropstar_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/relation_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/rliftstar_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/simple_1.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_6.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/subseteq_4.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/supterm_6.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/supterm_7.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermopt_6.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermopt_7.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermplus_6.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermplus_7.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermstar_6.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/suptermstar_7.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/voidstareq_4.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_lex.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_seq.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
matita/matita/contribs/lambdadelta/static_2/relocation/drops_weight.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_simple.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight_bind.ma
matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
matita/matita/contribs/lambdadelta/static_2/relocation/sex_length.ma
matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_drops.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_weight.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_drops.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_fqup.ma
matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_weight.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_length.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqx.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_weight.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fquq.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_weight.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_feqx.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_fqus.ma
matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma
matita/matita/contribs/lambdadelta/static_2/static/frees.ma
matita/matita/contribs/lambdadelta/static_2/static/frees_append.ma
matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
matita/matita/contribs/lambdadelta/static_2/static/frees_frees.ma
matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
matita/matita/contribs/lambdadelta/static_2/static/fsle_length.ma
matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma
matita/matita/contribs/lambdadelta/static_2/static/lsuba_aaa.ma
matita/matita/contribs/lambdadelta/static_2/static/lsuba_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubc.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubc_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubr.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubr.ma
matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/req.ma
matita/matita/contribs/lambdadelta/static_2/static/req_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqup.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
matita/matita/contribs/lambdadelta/static_2/static/rex.ma
matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
matita/matita/contribs/lambdadelta/static_2/static/rex_fqup.ma
matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma
matita/matita/contribs/lambdadelta/static_2/static/rex_length.ma
matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
matita/matita/contribs/lambdadelta/static_2/syntax/append.ma
matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma
matita/matita/contribs/lambdadelta/static_2/syntax/bind_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma
matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.ma
matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma
matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma
matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_simple.ma
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl