]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/reducibility/
- notation change for weight functions (following lambda)
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility /
drwxr-xr-x   ..
-rw-r--r-- 2625 cfpr.ma
-rw-r--r-- 1506 cfpr_aaa.ma
-rw-r--r-- 1480 cfpr_cfpr.ma
-rw-r--r-- 3239 cfpr_cpr.ma
-rw-r--r-- 2099 cfpr_ltpss.ma
-rw-r--r-- 3095 cif.ma
-rw-r--r-- 1765 cif_append.ma
-rw-r--r-- 2892 cnf.ma
-rw-r--r-- 4200 cnf_cif.ma
-rw-r--r-- 3720 cnf_lift.ma
-rw-r--r-- 4044 cpr.ma
-rw-r--r-- 1419 cpr_aaa.ma
-rw-r--r-- 3061 cpr_cpr.ma
-rw-r--r-- 2027 cpr_delift.ma
-rw-r--r-- 8062 cpr_lift.ma
-rw-r--r-- 2514 cpr_ltpr.ma
-rw-r--r-- 1511 cpr_ltpss.ma
-rw-r--r-- 1601 cpr_tpss.ma
-rw-r--r-- 4545 crf.ma
-rw-r--r-- 2698 crf_append.ma
-rw-r--r-- 2976 fpr.ma
-rw-r--r-- 3192 fpr_cpr.ma
-rw-r--r-- 1461 fpr_fpr.ma
-rw-r--r-- 1859 lfpr.ma
-rw-r--r-- 1426 lfpr_aaa.ma
-rw-r--r-- 3367 lfpr_alt.ma
-rw-r--r-- 1662 lfpr_cpr.ma
-rw-r--r-- 1601 lfpr_fpr.ma
-rw-r--r-- 2033 lfpr_lfpr.ma
-rw-r--r-- 2906 ltpr.ma
-rw-r--r-- 4461 ltpr_aaa.ma
-rw-r--r-- 1504 ltpr_ldrop.ma
-rw-r--r-- 1601 ltpr_ltpr.ma
-rw-r--r-- 1957 ltpr_ltpss_dx.ma
-rw-r--r-- 1694 ltpr_ltpss_sn.ma
-rw-r--r-- 2834 ltpr_tps.ma
-rw-r--r-- 2453 thnf.ma
-rw-r--r-- 10182 tpr.ma
-rw-r--r-- 1572 tpr_delift.ma
-rw-r--r-- 6082 tpr_lift.ma
-rw-r--r-- 10981 tpr_tpr.ma
-rw-r--r-- 2873 tpr_tps.ma
-rw-r--r-- 5110 tpr_tpss.ma
-rw-r--r-- 1575 xpr.ma
-rw-r--r-- 1437 xpr_aaa.ma
-rw-r--r-- 2486 xpr_lift.ma
-rw-r--r-- 1533 xpr_lsubss.ma