From: Ferruccio Guidi Date: Sun, 26 Oct 2014 19:07:45 +0000 (+0000) Subject: - some renaming according to the written version of basic_2 X-Git-Tag: make_still_working~810 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c60524dec7ace912c416a90d6b926bee8553250b - some renaming according to the written version of basic_2 - more destructing lemmas invoked in place of buggy destructs --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index f13d943f8..e4499a294 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -10,32 +10,30 @@ applications of λδ version 2. In particular it contains the components below. - - Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. - - - The validation algorithm for λδ as implemented in - Helena 0.8. - + + + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + + + + The validation algorithm for λδ as implemented in + Helena 0.8. +
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]. - + The Applications directory is started. - + The Functional component is started inside the specification of λδ version 2. - + The MLTT1 component is started. @@ -48,9 +46,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. -
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 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. -
- + Natural numbers with infinity. - + Specification starts. @@ -30,9 +30,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each plane. -