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=af73af5fc26343c50eebd3dfc4b6f0380b75fb64;hb=f95f6cb21b86f3dad114b21f687aa5df36088064;hp=b2cadf0d28d42d383f7858061959bb851f030c97;hpb=8fa70fc9a05fa9e9d37ff0c33b532908174d1c22;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 b2cadf0d2..af73af5fc 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 @@ -19,6 +19,10 @@

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]. @@ -30,6 +34,9 @@ for native validity. + Passive support for global environments. + + Reaxiomatized Î²-reductum as in extended Î²-reduction