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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 15 Feb 2013 14:17:58 +0000 (14:17 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 15 Feb 2013 14:17:58 +0000 (14:17 +0000)
commit	18bc3082b332504f60345245e716b62ae628e3a7
tree	8f09908a911dd189b3f9936cbeee33131a745707	tree \| snapshot
parent	1ea0f459b4435459442c8afb113bae815e38986e	commit \| diff

we reformulate the extended computation to simplify the proof of its
normalization property

42 files changed:

matita/matita/contribs/lambdadelta/Makefile		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.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_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma	[new file with mode: 0644]	blob

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

RSS Atom