X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fbasic_2_src.tbl;h=12f91aff4518b7e6ca3317e25b1054b463dcf17b;hb=56bae915998d8058aaa00da663faf75499561ba4;hp=fff49d93a78b08fef841f1cd21f2b116f41faddc;hpb=243d091f23f8338e155cdde14969a6043b8c89af;p=helm.git diff --git a/helm/www/lambdadelta/web/home/basic_2_src.tbl b/helm/www/lambdadelta/web/home/basic_2_src.tbl index fff49d93a..12f91aff4 100644 --- a/helm/www/lambdadelta/web/home/basic_2_src.tbl +++ b/helm/www/lambdadelta/web/home/basic_2_src.tbl @@ -77,7 +77,12 @@ table { ] class "cyan" [ { "computation" * } { - [ { "big tree order" * } { + [ { "focalized computation" * } { + [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ] + [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] + } + ] + [ { "\"big tree\" order" * } { [ "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ] } ] @@ -94,11 +99,6 @@ table { [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ] } ] - [ { "focalized computation" * } { - [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ] - [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] - } - ] [ { "context-sensitive computation" * } { [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ] } @@ -120,10 +120,6 @@ table { ] class "water" [ { "reducibility" * } { - [ { "big tree successor" * } { - [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ] - } - ] [ { "context-sensitive focalized reduction" * } { [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ] } @@ -133,6 +129,10 @@ table { [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ] } ] + [ { "\"big tree\" successor" * } { + [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ] + } + ] [ { "context-sensitive normal forms" * } { [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] }