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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 21 Feb 2014 16:36:20 +0000 (16:36 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 21 Feb 2014 16:36:20 +0000 (16:36 +0000)
commit	376fd7774ef0fa2f30a4afb25aab6158e3cd04b7
tree	ffb6f7dc45aaa7a0c23efaac5341b639ce9923dc	tree \| snapshot
parent	e4be4188d549da5fde54cdc37a6fb4eb2469c15b	commit \| diff

- main proposition on lsx finally proved!
- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat

59 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/append/cir_append.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/cix_append.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/cl_shift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/cpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/cpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/crr_append.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/crx_append.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/ldrop_append.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/lpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/coeq_4.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/lcoeq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/lcoeq_lcoeq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/ldrop_lcoeq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma		diff \| blob \| history
matita/matita/predefined_virtuals.ml		diff \| blob \| history

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

RSS Atom