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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 5 Apr 2014 13:57:19 +0000 (13:57 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 5 Apr 2014 13:57:19 +0000 (13:57 +0000)
commit	78b27990925c54b2a34cff609fc9bcfbeb6b48f3
tree	622b9abf329f0d1ed446e322e8c09040762e3f3e	tree \| snapshot
parent	f21cc1fc7f776761926a7f017fda55735d63442e	commit \| diff

commit completed:
- pointwise ordinary reduction:
  we park the "lazy" version and we restore the "full" version
  annotating the source with our understandings
- pointwise extended reduction:
  we use the "lazy" version for now
  a better understanding of the relationship between the "full" version
  and the "lazy" version (lpx_sn_llpx_sn) allows to link the two

80 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.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_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cpcs_cpcs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_cprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsn_5.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsnstar_5.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_llpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_cprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_llprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpx_sn_llpx_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_ldrop.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma	[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/lazypredsn_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.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