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=1c4a0bef5072bbecc79b820015ae008ec76cf0d7;hb=90ee1e85245752414b93826aabe388409571187a;hp=c20aa4b1057f4af6976966fa0f0f3e931c1a0f65;hpb=037b48dbbc0b4373ad1e43d837ac9158787486ef;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 c20aa4b10..1c4a0bef5 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
@@ -11,11 +11,11 @@
* In terms only.
- ** In terms and local environments only.
+ ** In terms and local environments only.
*** In global environments only.
- **** Sort level k in terms only.
+ **** Sort level k in terms only.
Here is a numerical acount of the specification's contents
and its timeline.
@@ -23,30 +23,39 @@
Context-sensitive subject equivalence
- for native type assignment.
+ for native type assignment.
Closure of extended context-sensitive computation
- for native validity.
+ for native validity.
Extended context-sensitive strong normalization
- for simply typed terms.
+ for simply typed terms.
+
+
+ Reaxiomatized substitution and reduction
+ commute with respect to subclosure
+ (anniversary milestone).
+
+
+ Mutual recursive preservation of stratified native validity
+ for hyper computation on closures.
Confluence for context-free parallel reduction on closures.
Term binders polarized to control ζ reduction.
-
+
Context-sensitive subject equivalence
- for atomic arity assignment
- (anniversary milestone).
+ for atomic arity assignment
+ (anniversary milestone).
Context-sensitive strong normalization
- for simply typed terms.
+ for simply typed terms.
Support for abstract candidates of reducibility.
@@ -65,8 +74,8 @@
The source files are grouped in planes and components
according to the following table.
A notation file covering the whole specification is provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses (? are placeholders).