matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 18 Nov 2019 22:12:40 +0000 (23:12 +0100)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 18 Nov 2019 22:12:40 +0000 (23:12 +0100)
commit	adb9ba187619cea977d1d22971eba27eb437cd6a
tree	5292aae35735318dae476970fc8ea2986c8292b2	tree \| snapshot
parent	f677b4ef7fa20f1ab36c5ee59598865d5c1b719b	commit \| diff

update for the article

+ pending conjectures proved
+ some renaming
+ probe: dependences are output in order

165 files changed:

.gitignore		diff \| blob \| history
matita/components/binaries/probe/options.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/Makefile		diff \| blob \| history
matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpmre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_cpms.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_cprre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/compile_partial.sh		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/aaa_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/aaa_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/aaa_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fqup.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fqus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_req.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqup.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_rdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/static/reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_drops.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqup.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_req.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq_ext.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/teqx_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom