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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 14 Dec 2013 22:18:47 +0000 (22:18 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 14 Dec 2013 22:18:47 +0000 (22:18 +0000)
commit	f6a6221dcb90a12b04378ca2de86192e0e39f9ab
tree	160599516c7f805322c74d23715b353efffd6269	tree \| snapshot
parent	d1b944b638846d98dfeb21fa6757e89c609be82a	commit \| diff

- "big tree" theorem is now proved up to some conjectures involving
just computation
- redefined "big tree" proper computation now replaces its restricted
form and is transitive
- improved definition of "big tree" proper reduction involves lazy
extended computation for local enviroments

40 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/btpredstarproper_8.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/names.txt		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history

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

RSS Atom