From 060864edadf332c07663e85bdc2299ee64e191ee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 2 Oct 2014 20:33:41 +0000 Subject: [PATCH] update in basic_2 ... --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 94 ++++++++++++------------ helm/www/lambdadelta/documentation.html | 2 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/implementation.html | 2 +- helm/www/lambdadelta/index.html | 2 +- helm/www/lambdadelta/news.html | 2 +- helm/www/lambdadelta/version_1.html | 2 +- helm/www/lambdadelta/version_2.html | 2 +- 10 files changed, 56 insertions(+), 56 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index bfbad5204..80d8b11b1 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:45 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index c5afbc884..b71a8c609 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:45 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index abeab7da6..2661fa63c 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -58,29 +58,29 @@ sizes files - 359 + 361 characters - 429628 + 431938 nodes - 1855731 + 1861135 propositions theorems - 127 + 128 lemmas - 1276 + 1289 total - 1403 + 1417 concepts declared 54 defined - 85 + 89 total - 139 + 143 @@ -246,7 +246,7 @@ examples terms with special features - ex_sta_ldec ex_cpr_omega + ex_sta_ldec ex_cpr_omega ex_fpbg_refl
@@ -385,7 +385,7 @@
- strongly normalizing "big tree" computation + strongly normalizing qrst-computation fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? ) fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? ) fsb_aaa fsb_csx @@ -455,41 +455,9 @@
- "big tree" parallel computation + parallel qrst-computation fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) - fpbg_lift fpbg_fleq fpbg_fpbg - -
- - -
- - - - -
- - -
- - fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ ) - fpbc_fleq fpbc_fpbs - -
- - -
- - - - -
- - -
- - fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) - fpbu_lift fpbu_lleq fpbu_fleq + fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg
@@ -506,7 +474,7 @@ fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) - fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext + fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbu fpbs_fpbc fpbs_fpbs
@@ -613,7 +581,39 @@ reduction - "big tree" parallel reduction + parallel qrst-reduction + fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ ) + fpbc_fleq + +
+ + +
+ + + + +
+ + +
+ + fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpbu_lift fpbu_lleq fpbu_fleq + +
+ + +
+ + + + +
+ + +
+ fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) fpb_lift fpb_aaa @@ -1321,6 +1321,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:45 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 3aa8581dc..07f373247 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -333,6 +333,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 12045bc1a..3edd96498 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:45 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 41e4e25d5..f426864c2 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -266,6 +266,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index ed71515eb..02398eb22 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -135,6 +135,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 5c33295ad..6db48ca8b 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -303,6 +303,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:51 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index 3e9c72737..1927e339b 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -167,6 +167,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index a1544fcb4..4335535ed 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -131,6 +131,6 @@

-
Last update: Tue, 30 Sep 2014 16:37:52 +0200
+
Last update: Thu, 02 Oct 2014 22:32:44 +0200
-- 2.39.2