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=d8206ed982e239c5ef674bd7fefaaba3f5ed4e2d;hpb=8ff4315142253a1a0478b67c07dddf70c36f50cd;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 d8206ed98..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 @@ -33,6 +33,11 @@ Extended context-sensitive strong normalization 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.