X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=a9ccf66828dee50b5de59acf2f6ca459ed7773d2;hb=d4a90dfb8d8a56012928a600ea2f6bd4758b51f6;hp=a2d50413076ab37f793bb1c1be49886e64466907;hpb=0679e5d5a305a43a8b4b01a5ac4c7caffacc73b9;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index a2d504130..a9ccf6682 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -101,7 +101,7 @@ table { ] [ { "context-sensitive computation" * } { [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ] - [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ] + [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } { @@ -121,7 +121,7 @@ table { } ] [ { "context-sensitive reduction" * } { - [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_cpss" + "lpr_lpss" + "lpr_aaa" + "lpr_cpr" + "lpr_lpr" * ] + [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_aaa" + "lpr_lpr" * ] [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ] } ]