From: Ferruccio Guidi Date: Thu, 16 Feb 2017 11:24:32 +0000 (+0000) Subject: update in basic_2 ... X-Git-Tag: make_still_working~504 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3adf21d15f533c901cb82ee8d459d93ac8cf77a5 update in basic_2 ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index edb2efd59..1e48bd7da 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:57 +0100
+
Last update: Thu, 16 Feb 2017 12:23:38 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 348d6970e..a6435234d 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:57 +0100
+
Last update: Thu, 16 Feb 2017 12:23:39 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 6bbb5a0b7..1dc6f50a0 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:56 +0100
+
Last update: Thu, 16 Feb 2017 12:23:38 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0fe96093f..f1ea20bbf 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 181 + 214 characters - 192119 + 202530 nodes - 993162 + 1010247 propositions theorems 48 lemmas - 642 + 675 total - 690 + 723 concepts declared 26 defined - 44 + 46 total - 70 + 72 @@ -362,6 +362,14 @@
+ + rt-computation + uncounted context-sensitive rt-transition + cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + +
+ + rt-transition parallel qrst-rtransition @@ -403,6 +411,16 @@
uncounted context-sensitive rt-transition + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops + + + +
+ + +
+ lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa @@ -426,7 +444,7 @@ static typing - restricted ref. for atomic arity assignment + atomic arity assignment lsuba ( ? ⊢ ? ⫃⁝ ? ) lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba @@ -434,7 +452,9 @@
- atomic arity assignment + +
+ aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) aaa_drops aaa_fqus aaa_lfdeq aaa_aaa @@ -442,7 +462,7 @@
- degree-based equivalence for closures on referred entries + degree-based equivalence on referred entries ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) ffdeq_fqup ffdeq_ffdeq @@ -450,7 +470,9 @@
- degree-based equivalence for local environments on referred entries + +
+ lfdeq ( ? ≡[?,?,?] ? ) lfdeq_length lfdeq_fqup lfdeq_lfdeq @@ -466,7 +488,7 @@
- restricted ref. for context-sensitive free variables + context-sensitive free variables lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) lsubf_frees @@ -474,7 +496,9 @@
- context-sensitive free variables + +
+ frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) frees_weight frees_drops frees_fqup frees_frees @@ -777,6 +801,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:58 +0100
+
Last update: Thu, 16 Feb 2017 12:23:40 +0100
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index ca6afb9ee..10cc0e438 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -7116,6 +7116,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:57 +0100
+
Last update: Thu, 16 Feb 2017 12:23:39 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index b691cdda6..f711e521b 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:55 +0100
+
Last update: Thu, 16 Feb 2017 12:23:36 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index e4d3d99e9..b20e79223 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:56 +0100
+
Last update: Thu, 16 Feb 2017 12:23:38 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index a2fcb0e61..d90a18687 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -136,7 +136,7 @@ characters 135595 nodes - 314125 + 314345 propositions @@ -819,6 +819,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:57 +0100
+
Last update: Thu, 16 Feb 2017 12:23:39 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index b8badf041..8312b1587 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -290,6 +290,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:54 +0100
+
Last update: Thu, 16 Feb 2017 12:23:36 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index bf0637f6a..da0010691 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:55 +0100
+
Last update: Thu, 16 Feb 2017 12:23:37 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 7b5157df9..d79757c9f 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:54 +0100
+
Last update: Thu, 16 Feb 2017 12:23:36 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 7ecb4f5fa..0406ae14e 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:55 +0100
+
Last update: Thu, 16 Feb 2017 12:23:37 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 13cbdf1cb..f0a1ea4f9 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Wed, 01 Feb 2017 20:52:56 +0100
+
Last update: Thu, 16 Feb 2017 12:23:37 +0100