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=fcabdb760ea8eef4719ebd1de1d2a0ee152c0d9c;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hp=ffb7cbb90d332fc4cbc01daee40aca9ffcae9c0f;hpb=e9b09b14538f770b9e65083c24e3e9cf487df648;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 ffb7cbb90..fcabdb760 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
@@ -7,7 +7,7 @@
head = "cic:/matita/lambdadelta/basic_2/ (core λδ version 2)"
>
-
-
+
+ λδ-2B is repackaged without λδ-ground_2.
+
+
+ λδ-2B is released.
+
+
+ Applicability condition is now parametrized
+ with a generic subset of numbers.
+
+
+ Applicability condition parametrized
+ with an initial interval of numbers
+ allows λδ-2B to generalize both λδ-2A and λδ-1B.
+
+
+ Extended (λδ-2A) and restricted (λδ-1B) validity is decidable
+ (anniversary milestone).
+
+
+ Preservation of validity for rt-computation
+ does not need the sort degree parameter
+ (i.e. no induction on the degree).
+
+
+ Extended (λδ-2A) and restricted (λδ-1B) validity rules justified.
+
+
λδ-2A completed with
confluence of rt-computation and
preservation of validity for rt-computation.
-
+
Behavioral component rt_computation completed.
-
+
"Big tree" theorem
(anniversary milestone).
-
+
Support for rt-computation completed.
-
+
Exclusion binder in local environments.
Syntactic component updated:
syntax, relocation, s_transition, s_computation, static, i_static.
-
+
Strong rt-normalization
for simply typed terms
(anniversary milestone).
-
+
Behavioral component rt_transition completed.
-
+
Generic candidates of reducibility.
-
+
Confluence for parallel r-transition on referred entries of local environments.
-
+
Confluence for context-sensitive parallel r-transition on terms.
-
+
Syntactic component completed:
syntax, relocation, s_transition, s_computation, static
(anniversary milestone).
-
+
Relocation with reference transforming maps (rtmap).
-
+
λδ-2B is started.
- Stage "A"
-
- λδ-2A appears too complex and is dismissed.
-
-
- λδ version 2A is released.
-
-
- 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
- added as q-step to rst-computation on closures
- (anniversary milestone).
-
-
- Parametrized slicing on 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.
-
-
- Generic candidates of reducibility.
-
-
- Confluence for context-sensitive parallel reduction on terms.
-
-
- Confluence for context-free parallel reduction on terms.
-
-
- λδ-2A is started.
-
-
Logical Structure of the Specification
This table reports the specification's components and their planes.