]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambda_delta/Basic_2/reducibility/
- we proved that context-free reduction admits no one-step loops
[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility /
drwxr-xr-x   ..
-rw-r--r-- 3616 cpr.ma
-rw-r--r-- 2823 cpr_cpr.ma
-rw-r--r-- 3656 cpr_lift.ma
-rw-r--r-- 2499 cpr_ltpr.ma
-rw-r--r-- 1699 lcpr.ma
-rw-r--r-- 3253 ltpr.ma
-rw-r--r-- 2618 ltpr_ldrop.ma
-rw-r--r-- 4367 tnf.ma
-rw-r--r-- 9630 tpr.ma
-rw-r--r-- 6441 tpr_lift.ma
-rw-r--r-- 11712 tpr_tpr.ma
-rw-r--r-- 5383 tpr_tpss.ma
-rw-r--r-- 3902 trf.ma