X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2.ldw.xml;h=f69061eaf5c8ed934c45156cb5de2327b041ab8d;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=9f2c61a6454c250e988694f0dce4289fb367e9f2;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git
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 9f2c61a64..f69061eaf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -21,86 +21,82 @@
Summary of the Specification
Here is a numerical acount of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
Stage "B"
-
+
Context-sensitive subject equivalence
for native type assignment.
Stage "A": "Weakening the Applicability Condition"
-
+
Iterated static type assignment defined (more elegantly)
as a primitive notion.
-
+
Preservation of stratified native validity
for context-sensitive computation on terms.
-
+
Strong qrst-normalization
for simply typed terms.
-
+
Lazy equivalence on local environments
addded as q-step to rst-computation on closures
(anniversary milestone).
-
+
Parametrized slicing of local environments
comprises both versions of this operation
(one from basic_1, the other used in basic_2 till now).
-
+
Passive support for global environments.
-
+
Reaxiomatized β-reductum as in rt-reduction.
-
+
Context-sensitive strong rt-normalization
for simply typed terms.
-
+
Reaxiomatized substitution and reduction
commute with respect to subclosure
(anniversary milestone).
-
+
Mutual recursive preservation of stratified native validity
for rst-computation on closures.
-
+
Confluence for context-free parallel reduction on closures.
-
+
Term binders polarized to control ζ-reduction (not released).
-
+
Context-sensitive subject equivalence
for atomic arity assignment
(anniversary milestone).
-
+
Context-sensitive strong normalization
for simply typed terms.
-
+
Support for abstract candidates of reducibility.
-
+
Confluence for context-sensitive parallel reduction on terms.
-
+
Confluence for context-free parallel reduction on terms.
-
+
Specification starts.
@@ -113,9 +109,5 @@