X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fld_basic_2.tbl;h=503c11d45c1ba4f9ed7329668b1471c6f88f7786;hb=aedbc9769bb8e65b2a99ef86c44b446b0f9a2dc7;hp=8480c70de4796ca4afb625f29958e3992d72f888;hpb=1e6ccf5e87e8c52cc8b360350fe91f2557d9311d;p=helm.git

diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.tbl b/helm/www/lambda_delta/web/home/ld_basic_2.tbl
index 8480c70de..503c11d45 100644
--- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl
+++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl
@@ -9,64 +9,94 @@ table {
         ]
      }
    ]
+   class "blue"
+   [ { "examples" * } {
+        [ { "" * } {
+	     [ "" * ]
+	  }
+        ]
+     }
+   ]
    class "sky"
    [ { "native typing" * } {
-         [ { "" * } {
-	      [ "nty" * ]
-	   }
-         ]
-      }
+        [ { "" * } {
+	     [ "nty" * ]
+	  }
+        ]
+     }
    ]
    class "cyan"
    [ { "conversion" * } {
-         [ { "context-sensitive" * } {
-	      [ "cpcs" * ]
-	   }
-         ]
-      }
+        [ { "context-sensitive conversion" * } {
+	     [ "cpcs" * ]
+	  }
+        ]
+     }
    ]
    class "water"
    [ { "computation" * } {
-         [ { "strongly normalizing" * } {
-	      [ "csn" * ]
-	   }
-         ]
-         [ { "context-sensitive" * } {
-	      [ "cprs" * ]
-	   }
-         ]
-      }
+        [ { "strongly normalizing computation" * } {
+	     [ "lsubcs" * ]
+	     [ "csn" "csn_cr" "csn_aarity" * ]
+	  }
+        ]
+        [ { "context-sensitive computation" * } {
+	     [ "cprs" * ]
+	  }
+        ]
+        [ { "support for abstract comptation properties" * } {
+	     [ "lsubc" * ]
+	     [ "acp" "acp_cr" * ]
+          }
+	]
+     }
    ]
    class "green"
-   [ { "reduction" * } {
-         [ { "context-sensitive" * } {
-	      [ "lcpr" * ]
-	      [ "cpr" "cpr_lift" "cpr_tpss" "cpr_cpr" * ]
-	   }
-         ]
-         [ { "context-free" * } {
-	      [ "ltpr" "ltpr_drop" * ]
-	      [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
-           }
-	 ]
-      }
+   [ { "reducibility" * } {
+        [ { "context-sensitive reduction" * } {
+	     [ "lcpr" * ]
+	     [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
+	  }
+        ]
+        [ { "context-free normal forms" * } {
+	     [ "twhnf" "tnf" * ]
+          }
+	]
+        [ { "context-free reduction" * } {
+	     [ "ltpr" "ltpr_ldrop" * ]
+	     [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
+          }
+	]
+        [ { "context-free reducible forms" * } {
+	     [ "trf" * ]
+          }
+	]
+     }
    ]
    class "grass"
    [ { "static typing" * } {
-         [ { "atomic arity ass." * } {
-	      [ "aaa" "aaa_lift" "aaa_aaa" * ]
-	   }
-         ]
-         [ { "static type ass." * } {
-	      [ "sty" "sty_lift" "sty_sty" * ]
-           }
-	 ]
-      }
-   ]   
+        [ { "static type ass." * } {
+	     [ "sty" "sty_lift" "sty_sty" * ]
+          }
+	]
+        [ { "atomic arity ass." * } {
+	     [ "aaa" "aaa_lift" "aaa_aaa" * ]
+	  }
+        ]
+        [ { "parameters" * } {
+             [ "sh" * ]
+          }
+        ]
+     }
+   ]
    class "yellow"
    [ { "unfold" * } {
-        [ { "partial" * } {
-             [ "ltpss" "ltpss_drop" "ltpss_tps" "ltpss_ltpss" * ] 
+        [ { "term inverse relocation" * } {
+	     [ "delift" * ]
+          }
+	]
+	[ { "partial unfold" * } {
+             [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
 	     [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
           }
 	]
@@ -74,13 +104,13 @@ table {
    ]
    class "orange"   
    [ { "substitution" * } { 
-        [ { "parallel" * } {
-             [ "ltps" "ltps_drop" "ltps_tps" "ltps_ltps" * ]
+        [ { "parallel substitution" * } {
+             [ "ltps" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
 	     [ "tps" "tps_lift" "tps_tps" * ]
           }
 	]
 	[ { "local env. dropping" * } {
-             [ "drop" "drop_drop" * ]
+             [ "ldrop" "ldrop_ldrop" * ]
           }
 	]
         [ { "term relocation" * } {
@@ -113,10 +143,6 @@ table {
              [ "aarity" * ]
 	  }
 	] 
-        [ { "parameters" * } {
-             [ "sh" * ]
-          }
-        ]
      }
    ]
 }