X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=3bd4980e4199db1d1811d3164c9c85305dc9668c;hb=645b62762e9c86e343d4741541a2ddccfed8ebc7;hp=736d0367cffaeac33a3ea6aab53f02fcb5bf6d94;hpb=b9d48c1a4433b3a2b17483bc207b2092f7ac4fd2;p=helm.git
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 736d0367c..3bd4980e4 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -6,8 +6,8 @@
-
-
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].
@@ -72,29 +76,29 @@
sizes |
files |
- 5 |
+ 4 |
characters |
- 5790 |
+ 3927 |
nodes |
- 9846 |
+ 3637 |
propositions |
theorems |
- 4 |
+ 2 |
lemmas |
1 |
total |
- 5 |
+ 3 |
concepts |
declared |
3 |
defined |
- 10 |
+ 9 |
total |
- 13 |
+ 12 |
@@ -138,29 +142,17 @@
- MLTT1 |
- |
- genv_primitive |
- judgement |
+ functional |
+ reduction and type machine |
+ rtm |
+ rtm_step ( ? ⨠? ) |
- functional |
- reduction and type machine |
- rtm |
- rtm_step ( ? ⨠? ) |
-
-
-
+ |
|
- unfold |
- lift ( â[?,?] ? ) |
- subst ( [?â?] ? ) |
-
-
- examples |
- |
- |
+ relocation |
+ lift ( â[?,?] ? ) |
|
@@ -199,6 +191,6 @@
- Last update: Sun, 05 May 2013 20:24:24 +0200
+ Last update: Sat, 28 Jun 2014 20:29:31 +0200