advances on append allow to complete the long awaited "big tree" theorem by closing...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2.ldw.xml
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml

index cc0a402b0a2f9f084be59f80da988e4e6a1707fb..4ccbf25fca33e834eaa5f7df0f5e65fafc807209 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -5,6 +5,7 @@
        title = "\lambda\delta version 2"
        head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
  >
+<!--   
     <section>System's Syntax and Behavior</section>
     <body>This is a summary of the "block structure"
           of the System's syntactic items and reductions.
@@ -15,6 +16,7 @@
           *** In global environments only.
           **** Sort level k in terms only.
     </body>
+-->
  
     <section>Summary of the Specification</section>
     <body>Here is a numerical acount of the specification's contents
@@ -30,8 +32,17 @@
           for native type assignment.
     </news>
     <news date="In progress.">
-         Closure of context-sensitive extended computation
-         for native validity.
+         Preservation of stratified native validity
+         for "big tree" computation on closures.
+   </news>
+   <news date="2014 June 9.">
+         "Big tree" strong normalization
+         for simply typed terms.
+   </news>
+   <news date="2014 April 16.">
+         lazy equivalence on local environments
+        serves as irrelevant step in "big tree" computation on closures
+         (anniversary milestone).
     </news>
     <news date="2014 January 20.">
           Parametrized slicing for local environments
@@ -61,7 +72,7 @@
           Confluence for context-free parallel reduction on closures.
     </news>
     <news date="2012 July 26.">
-         Term binders polarized to control ζ-reduction.
+         Term binders polarized to control ζ-reduction (not released).
     </news>
     <news date="2012 April 16.">
           Context-sensitive subject equivalence