X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fweb%2Fchanges.tbl;h=9ef76e8f408e1b07422d902293e6b9ee84ea6d9f;hb=3f57ed2589601e79478c85d74708d8ebdec2cf20;hp=bf985679d8c0459016396b8e3a34e02e00eaebd6;hpb=a82d87a4c2ff9f518385fba7357dafb632a22882;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/web/changes.tbl b/matita/matita/contribs/lambdadelta/web/changes.tbl
index bf985679d..9ef76e8f4 100644
--- a/matita/matita/contribs/lambdadelta/web/changes.tbl
+++ b/matita/matita/contribs/lambdadelta/web/changes.tbl
@@ -9,63 +9,143 @@ table {
   [ { "λδ-2B" + "(November 2019)" * }
     {
      [ [{ "validity" * }]
-       { "@" "" "@" }
-       { "+" "-" "*" }
-       { "type assignment (terms)"
-         "stratified higher validity (terms) removed"
+       { "" "@" "" "@" }
+       { "+" "+" "-" "*" }
+       { "iterated type assignment (terms)"
+         "type assignment (terms)"
+         "higher validity (terms) removed"
          "primitive validity (terms)"
        }
      ]
      [ [{ "equivalences" * }]
-       { "" "" "" "" }
-       { "+" "+" "+" "-" }
-       { "equivalence for full rt-reduction (terms)"
+       { "" "" "" "" "" "" "" }
+       { "+" "-" "+" "+" "+" "+" "-" }
+       { "derived rt-equivalence (terms)"
+         "primitive decomposed rt-equivalence (terms) removed"
          "equivalence for whd rt-reduction (terms)"
-         "equivalence for full rt-reduction (terms, referred lenvs, closures)"
-         "syntactic equivalence (closures) removed"
+         "equivalence for full rt-reduction (terms, items, referred lenvs, referred closures)"
+         "equivalence up to exclusion binders (selected lenvs)"
+         "syntactic equivalence (items)"
+         "syntactic equivalence (selected closures) removed"
        }
      ]
      [ [{ "partial orders" * }]
-       { "" }
-       { "+" }
-       { "switch in primitive order relations for closures to enable the exclusion binder"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with inclusion (hereditarily free variables)"
+         "inclusion (hereditarily free variables)"
+         "inclusion (applicability)"
+         "switch in primitive order relations (closures) to enable the exclusion binder"
+         "simple weight (items, genvs)"
+       }
+     ]
+     [ [{ "reducibility" * }]
+       { "" "" "" }
+       { "+" "-" "*" }
+       { "compatibility relation for strong normalization (referred lenvs)"
+         "compatibility predicate for strong normalization (referred lenvs) removed"
+         "abatract Tait's candidates with 6 postulates"
        }
      ]
      [ [{ "normal form predicates" * }]
-       { "" "" "" "" "" }
-       { "-" "-" "-" "-" "-" }
-       { "irreducible forms for full rt-reduction (terms) removed"
+       { "" "" "" "" "" "" "" "" "" "" }
+       { "+" "-" "+" "*" "+" "-" "-" "-" "-" "-" }
+       { "properties with evaluation"
+         "evaluation for full rt-reduction (terms) removed"
+         "whd evaluation for mixed rt-reduction (terms)"
+         "evaluation for mixed rt-reduction (terms)"
+         "whd normal form for mixed rt-reduction (terms)"
+         "irreducible forms for full rt-reduction (terms) removed"
          "reducible forms for full rt-reduction (terms) removed"
          "irreducible forms for reduction (terms) removed"
          "reducible forms for reduction (terms) removed"
          "abstract reducibility properties (items) removed"
        }
      ]
+     [ [{ "reduction and type synthesis" * }]
+       { "" "" "@" "" "" "@" "" "" "@" "@" }
+       { "*" "*" "-" "+" "*" "+" "*" "+" "*" "+" }
+       { "counted iterated type synthesis (terms)"
+         "full rt-computation (terms, items, lenvs)"
+         "decomposed rt-computation (terms) removed"
+         "r-computation (items)"
+         "mixerd rt-computation (terms)"
+         "counted type synthesis (terms) with δ,s,l,e"
+         "full rt-transition (terms, items, lenvs, referred lenvs)"
+         "r-transition (items)"
+         "mixed rt-transition (terms)"
+         "primitive generic rt transition (terms) with typed β, δ, (correct) ζ, θ, ε"
+       }
+     ]
      [ [{ "substitution" * }]
-       { "" }
-       { "-" }
-       { "zero or more refs (terms) removed"
+       { "" "" }
+       { "-" "-" }
+       { "(restricted) zero or more selected refs (terms) removed"
+         "zero or more refs (terms) removed"
        }
      ]
-     [ [{ "relocation" * }]
-       { "" "" "" "" }
-       { "-" "*" "-" "*" }
-       { "basic slicing (lenvs) removed"
+     [ [{ "degree" * }]
+       { "" "@" }
+       { "-" "-" }
+       { "refinement for degree (lenvs) removed"
+         "degree assignment (terms) removed"
+       }
+     ]
+     [ [{ "relocation and slicing" * }]
+       { "" "" "" "" "" "" "" }
+       { "-" "+" "-" "*" "-" "+" "*" }
+       { "look-up predicate (genvs) removed"
+         "properties with abstract relocation (terms/items)"
+         "basic slicing (lenvs) removed"
          "primitive finite slicing (lenvs)"
-         "basic relocation (lists of terms) removed"
+         "basic relocation (terms, lists of terms) removed"
+         "primitive finite relocation (items)" 
          "primitive finite relocation (terms, lists of terms)"
        }
      ]
      [ [{ "free varibles" * }]
-       { "" }
-       { "+" }
-       { "union (referred lenvs) removed"
+       { "" "" }
+       { "+" "-" }
+       { "refinement for hereditarily free variables (lenvs)"
+         "union (referred lenvs) removed"
+       }
+     ]
+     [ [{ "helpers" * }]
+       { "" "" "" "" "" }
+       { "-" "+" "+" "-" "+" }
+       { "unfold (closures) removed"
+         "append (restricted closures) wrong on excluded entries"
+         "length (genvs)"
+         "refinement (selected lenvs) removed"
+         "abstract properties with append (lenvs)"
+       }
+     ]
+     [ [{ "extension" * }]
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with iterated extension (referred lenvs)"
+         "iterated for 3-relations (referred lenvs)"
+         "abstract properties with extension (selected lenvs)"
+         "for 3-relations (selected lenvs)"
+         "for 2-relations and 3-relations (items)"
        }
      ]
      [ [{ "syntax" * }]
-       { "@" }
-       { "+" }
-       { "exclusion binder for lenvs"
+       { "@" "" }
+       { "+" "+" }
+       { "exclusion binder (lenvs)"
+         "bonding items (lenvs)"
+       }
+     ]
+     [ [{ "parameters" * }]
+       { "" "" "@" "" "" "@" }
+       { "+" "+" "+" "-" "+" "*" }
+       { "instances (applicability)"
+         "predicates (applicability)"
+         "abstract applicability condition"
+         "instances (sort hierarchy) removed"
+         "predicates (sort hierarchy) including strict monotonicity condition based on non-negative integers"
+         "abstract sort hierarchy without predicates"
        }
      ]
      [ [{ "ground" * }]
@@ -81,7 +161,7 @@ table {
   ]
 
   class "orange"
-  [ { "λδ-2A" + "(October 2014)" * }
+  [ { "λδ-2A" + "(August 2015)" * }
     {
      [ [{ "validity" * }]
        { "" "" "@" "" "" "" "@" }
@@ -96,24 +176,26 @@ table {
        }
      ]
      [ [{ "equivalences" * }]
-       { "@" "" "@" "" "" "" }
-       { "+" "+" "-" "-" "-" "+" }
+       { "@" "" "@" "" "" "" "" }
+       { "+" "+" "-" "-" "-" "+" "+" }
        { "primitive decomposed rt-equivalence (terms)"
          "single-step context-sensitive r-eqivalence (terms)"
          "primitive context-sensitive r-eqivalence (terms) removed"
          "context-free r-eqivalence (terms) removed"
          "level equivalence (binary arities) removed"
-         "syntactic equivalence (selected lenvs, referred lenvs, selected closures)"
+         "properties with syntactic equivalence (referred lenvs)"
+         "syntactic equivalence (selected lenvs, referred lenvs, referred closures)"
        }
      ]
      [ [{ "partial orders" * }]
-       { "" "" "" "" "" "" "" }
-       { "+" "*" "+" "-" "-" "-" "-" }
+       { "" "" "" "" "" "" "" "" }
+       { "+" "*" "+" "-" "-" "-" "-" "-" }
        { "big-tree order relations (closures)"
-         "primitive order relations for closures"
+         "primitive order relations (closures)"
          "simple weight (restricted closures)"
+         "order relation (lenvs) based on look-up removed"
          "order relation (lists of terms) based on lengths removed"
-         "order relations (binary arities) based on weights removed"
+         "order relations (terms, lenvs, binary arities) based on weights removed"
          "simple weights (binary arities) removed"
          "complex weight (terms) removed"
        }
@@ -132,11 +214,12 @@ table {
        }
      ]
      [ [{ "normal form predicates" * }]
-       { "" "" "" "" "" "" "" "" "" }
-       { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
+       { "" "" "" "" "" "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" "+" "-" "+" "+" "+" }
        { "evaluation for full rt-reduction (terms)"
+         "evaluation for reduction (terms)"
          "normal form for full rt-reduction (terms)"
-         "irreducible forms for fulld rt-reduction (terms)"
+         "irreducible forms for full rt-reduction (terms)"
          "reducible forms for full rt-reduction (terms)"
          "evaluation for reduction (terms)"
          "normal form for reduction (lists of terms) removed"
@@ -146,14 +229,15 @@ table {
        }
      ]
      [ [{ "reduction and type synthesis" * }]
-       { "" "" "@" "@" "" "" "" "@" "@" }
-       { "+" "+" "+" "*" "-" "+" "-" "*" "-" }
+       { "" "" "@" "@" "" "" "" "" "@" "@" }
+       { "+" "+" "+" "*" "-" "+" "+" "-" "*" "-" }
        { "stratified full rt-computation (terms, lenvs)"
          "stratified full rt-transition (terms, lenvs)"
          "decomposed rt-computation (terms)"
          "primitive counted iterated type synthesis with δ,s,l,e (terms)"
          "syntax-oriented type synthesis (terms) removed"
          "refinement for reduction (lenvs)"
+         "context-sensitive computation (lenvs)"
          "context-free computation (terms) removed"
          "primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)"
          "context-free transition (terms, lenvs) removed"
@@ -169,7 +253,7 @@ table {
        }
      ]
      [ [{ "degree" * }]
-       { "@" "" "@" "" }
+       { "" "@" "" "@" }
        { "+" "+" "+" "+" }
        { "refinement for degree (lenvs)"
          "degree assignment (terms)"
@@ -204,7 +288,7 @@ table {
          "refinement (selected lenvs)"
          "append (lenvs)"
          "left cons (lenvs) removed"
-         "flat construction clear (lenvs) removed"
+         "flat entry clear (lenvs) removed"
          "sort extraction (lenvs) removed"
          "context predicate (terms) removed"
          "neutral predicate (terms)"
@@ -232,8 +316,8 @@ table {
      ]
      [ [{ "parameters" * }]
        { "" "" }
-       { "+" "-"}
-       { "concrete sort hierarchies"
+       { "+" "-" }
+       { "instances (sort hierarchy)"
          "iterated next function (sort hierarchy) removed"
        }
      ]
@@ -249,7 +333,7 @@ table {
   ]
 
   class "red"
-  [ { "λδ-1A" + "(November 2006)" * }
+  [ { "λδ-1A" + "(May 2008)" * }
     {
      [ [{ "validity" * }]
        { "@" "" "" }
@@ -270,9 +354,10 @@ table {
        }
      ]
      [ [{ "partial orders" * }]
-       { "" "" "" "" }
-       { "+" "+" "+" "+" }
-       { "order relation (specialized lists of terms) based on lengths"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "order relation (lenvs) based on look-up"
+         "order relation (specialized lists of terms) based on lengths"
          "order relations (terms, lenvs, closures, binary arities) based on weights"
          "simple weights (terms, lenvs, closures, binary arities)"
          "complex weight (terms)"
@@ -293,7 +378,7 @@ table {
      [ [{ "normal form predicates" * }]
        { "" }
        { "+" }
-       { "normal form for context-sensitive reduction (terms, specialized lists of terms)"
+       { "normal form for reduction (terms, specialized lists of terms)"
        }
      ]
      [ [{ "reduction and type synthesis" * }]
@@ -316,10 +401,9 @@ table {
        }
      ]
      [ [{ "relocation and slicing" * }]
-       { "" "" "" "" "" "" "" "" }
-       { "+" "+" "+" "+" "+" "+" "+" "+" }
-       { "order relation (lenvs) based on look-up"
-         "look-up predicate (lenvs)"
+       { "" "" "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" "+" "+" }
+       { "look-up predicate (lenvs)"
          "finite slicing (lenvs)"
          "basic slicing (lenvs)"
          "finite relocation (terms, specialized lists of terms)"