]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/reducibility/
- lambdadelta: third recursive part of preservation finally proved!
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility /
drwxr-xr-x   ..
-rw-r--r-- 2623 cfpr.ma
-rw-r--r-- 1505 cfpr_aaa.ma
-rw-r--r-- 1480 cfpr_cfpr.ma
-rw-r--r-- 3205 cfpr_cpr.ma
-rw-r--r-- 2101 cfpr_ltpss.ma
-rw-r--r-- 3093 cif.ma
-rw-r--r-- 1765 cif_append.ma
-rw-r--r-- 2892 cnf.ma
-rw-r--r-- 4199 cnf_cif.ma
-rw-r--r-- 3720 cnf_lift.ma
-rw-r--r-- 4436 cpr.ma
-rw-r--r-- 1419 cpr_aaa.ma
-rw-r--r-- 3059 cpr_cpr.ma
-rw-r--r-- 2027 cpr_delift.ma
-rw-r--r-- 8592 cpr_lift.ma
-rw-r--r-- 2514 cpr_ltpr.ma
-rw-r--r-- 1610 cpr_ltpss_dx.ma
-rw-r--r-- 1879 cpr_ltpss_sn.ma
-rw-r--r-- 2008 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-- 5940 fpr_cpr.ma
-rw-r--r-- 1461 fpr_fpr.ma
-rw-r--r-- 1941 lfpr.ma
-rw-r--r-- 1426 lfpr_aaa.ma
-rw-r--r-- 3367 lfpr_alt.ma
-rw-r--r-- 1664 lfpr_cpr.ma
-rw-r--r-- 1600 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-- 1693 ltpr_ltpss_sn.ma
-rw-r--r-- 2834 ltpr_tps.ma
-rw-r--r-- 2453 thnf.ma
-rw-r--r-- 10524 tpr.ma
-rw-r--r-- 1571 tpr_delift.ma
-rw-r--r-- 6103 tpr_lift.ma
-rw-r--r-- 10973 tpr_tpr.ma
-rw-r--r-- 2873 tpr_tps.ma
-rw-r--r-- 5109 tpr_tpss.ma