X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2.ldw.xml;h=07c82f98af320945c0fcdfdda7f74aab54133623;hb=fca909e9e53de73771e1b47e94434ae8f747d7fb;hp=0908b1e0a017d4454141a7d79712ed6017732a67;hpb=3cb5a8e407f0a783c27a4165187578aae980bc39;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 0908b1e0a..07c82f98a 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 @@ -27,17 +27,25 @@ pp. 53-78]. + + Stage "B" Context-sensitive subject equivalence for native type assignment. - - Closure of native validity - for context-sensitive extended computation. + + Stage "A": "Weakening the Applicability Condition" + + Preservation of stratified native validity + for context-sensitive computation on terms. + + + "Big tree" strong normalization + for simply typed terms. - lazy equivalence for local environments - serves as irrelevant step in "big tree" computation + lazy equivalence on local environments + serves as irrelevant step in "big tree" computation on closures (anniversary milestone).