From: Ferruccio Guidi Date: Mon, 16 Jan 2017 11:26:06 +0000 (+0000) Subject: update in ground_2 and basic_2 ... X-Git-Tag: make_still_working~525 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=614542345e3e9c88722fdbc32c24a14b9a6c71d1 update in ground_2 and basic_2 ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 5df60f343..866682828 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:25 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 51e7ef4e5..d0cde1b49 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 044fcb0fe..ec98af6cb 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d19002196..235681848 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 167 + 157 characters - 167321 + 138411 nodes - 875248 + 711276 propositions theorems - 47 + 45 lemmas - 590 + 506 total - 637 + 551 concepts declared 23 defined - 40 + 38 total - 63 + 61 @@ -494,9 +494,9 @@
- restricted ref. for local env. - lsubr ( ? ⫃ ? ) - lsubr_length lsubr_drops lsubr_lsubr + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq
@@ -508,9 +508,9 @@
- equivalence for closures on referred entries - ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - ffeq_freq + equivalence for local environments on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq
@@ -522,9 +522,9 @@
- equivalence for local environments on referred entries - lfeq ( ? ≡[?] ? ) - lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
@@ -536,9 +536,9 @@
- generic extension on referred entries - lfxs ( ? ⦻*[?,?] ? ) - lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + restricted ref. for context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees
@@ -560,6 +560,20 @@
+ + +
+ + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + +
+ + +
+ + s-computation iterated structural successor for closures @@ -863,6 +877,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 1e24eb618..529fcb5c9 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 22c53e201..ed0eded6d 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 9083df133..8e32d0ff6 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -134,18 +134,18 @@ files 95 characters - 132639 + 131558 nodes - 308557 + 304213 propositions theorems - 38 + 37 lemmas - 635 + 626 total - 673 + 663 concepts @@ -819,6 +819,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index 2fdf11e9f..97eba933c 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -290,6 +290,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 812a44e5a..67ca18053 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index be546afcf..d8c3abe04 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index bb360ef6a..4159ea96b 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 169743bb6..8a5b43f75 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:42 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100