]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/computation/
- main proposition on lsx finally proved!
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation /
drwxr-xr-x   ..
-rw-r--r-- 2625 acp.ma
-rw-r--r-- 5141 acp_aaa.ma
-rw-r--r-- 8824 acp_cr.ma
-rw-r--r-- 2517 cpds.ma
-rw-r--r-- 1432 cpds_aaa.ma
-rw-r--r-- 3923 cpds_cpds.ma
-rw-r--r-- 1857 cpds_lift.ma
-rw-r--r-- 1930 cpre.ma
-rw-r--r-- 1583 cpre_cpre.ma
-rw-r--r-- 6593 cprs.ma
-rw-r--r-- 8741 cprs_cprs.ma
-rw-r--r-- 2804 cprs_lift.ma
-rw-r--r-- 1938 cpxe.ma
-rw-r--r-- 8124 cpxs.ma
-rw-r--r-- 1674 cpxs_aaa.ma
-rw-r--r-- 10577 cpxs_cpxs.ma
-rw-r--r-- 1375 cpxs_cpys.ma
-rw-r--r-- 6163 cpxs_lift.ma
-rw-r--r-- 1962 cpxs_lleq.ma
-rw-r--r-- 5347 cpxs_tstc.ma
-rw-r--r-- 9026 cpxs_tstc_vector.ma
-rw-r--r-- 5926 csx.ma
-rw-r--r-- 3131 csx_aaa.ma
-rw-r--r-- 4958 csx_alt.ma
-rw-r--r-- 2037 csx_fpbs.ma
-rw-r--r-- 5432 csx_lift.ma
-rw-r--r-- 6709 csx_lpx.ma
-rw-r--r-- 5770 csx_tstc_vector.ma
-rw-r--r-- 2080 csx_vector.ma
-rw-r--r-- 1876 fpbc.ma
-rw-r--r-- 1544 fpbc_fpbs.ma
-rw-r--r-- 1988 fpbc_fpns.ma
-rw-r--r-- 3541 fpbg.ma
-rw-r--r-- 2803 fpbg_fpbg.ma
-rw-r--r-- 4115 fpbg_fpns.ma
-rw-r--r-- 1739 fpbg_lift.ma
-rw-r--r-- 6451 fpbs.ma
-rw-r--r-- 1618 fpbs_aaa.ma
-rw-r--r-- 3113 fpbs_alt.ma
-rw-r--r-- 2544 fpbs_fpbs.ma
-rw-r--r-- 1464 fpbs_fpns.ma
-rw-r--r-- 1707 fpbs_lift.ma
-rw-r--r-- 2550 fpbu.ma
-rw-r--r-- 3860 fpbu_fpns.ma
-rw-r--r-- 1872 fpbu_lift.ma
-rw-r--r-- 2051 fpns.ma
-rw-r--r-- 1483 fpns_fpns.ma
-rw-r--r-- 2283 fsb.ma
-rw-r--r-- 3886 fsb_aaa.ma
-rw-r--r-- 4010 fsb_alt.ma
-rw-r--r-- 3519 fsb_csx.ma
-rw-r--r-- 3635 lcosx.ma
-rw-r--r-- 3767 lcosx_cpxs.ma
-rw-r--r-- 3232 lprs.ma
-rw-r--r-- 2409 lprs_alt.ma
-rw-r--r-- 6845 lprs_cprs.ma
-rw-r--r-- 1569 lprs_ldrop.ma
-rw-r--r-- 1595 lprs_lprs.ma
-rw-r--r-- 3553 lpxs.ma
-rw-r--r-- 1743 lpxs_aaa.ma
-rw-r--r-- 2510 lpxs_alt.ma
-rw-r--r-- 6627 lpxs_cpxs.ma
-rw-r--r-- 1593 lpxs_ldrop.ma
-rw-r--r-- 6943 lpxs_lleq.ma
-rw-r--r-- 1279 lpxs_lpxs.ma
-rw-r--r-- 5028 lsubc.ma
-rw-r--r-- 3675 lsubc_ldrop.ma
-rw-r--r-- 1870 lsubc_ldrops.ma
-rw-r--r-- 1535 lsubc_lsuba.ma
-rw-r--r-- 4406 lsx.ma
-rw-r--r-- 3175 lsx_csx.ma
-rw-r--r-- 3980 lsx_ldrop.ma
-rw-r--r-- 6026 lsx_lpxs.ma