From 79340579023e8e6ee8338da90e2aa9eb3d1fc633 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 6 Oct 2013 11:51:04 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 4 +-- helm/www/lambdadelta/basic_2.html | 50 ++++++++++++++++++++----------- 3 files changed, 36 insertions(+), 20 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 833669fb2..cd3a2346a 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Fri, 04 Oct 2013 17:03:31 +0200
+
Last update: Sun, 06 Oct 2013 13:50:12 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index f6b48a053..828f7fba0 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -80,7 +80,7 @@ characters 3922 nodes - 3637 + 3861 propositions @@ -191,6 +191,6 @@

-
Last update: Fri, 04 Oct 2013 17:03:32 +0200
+
Last update: Sun, 06 Oct 2013 13:50:12 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 16bb892ad..dbef0bf0e 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,20 +163,20 @@ sizes files - 265 + 266 characters - 399415 + 400863 nodes - 1201927 + 1203013 propositions theorems 81 lemmas - 806 + 814 total - 887 + 895 concepts @@ -411,8 +411,8 @@
strongly normalizing computation - csn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csn_tstc_vector csn_aaa + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) + csx_tstc_vector csx_aaa
@@ -427,9 +427,9 @@
- csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) - csn_lift csn_lpx + csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) + csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) + csx_lift csx_lpx
@@ -439,8 +439,8 @@
"big tree" parallel computation - ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) - ygt_lift ygt_ygt + fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) + fpbg_lift fpbg_fpbg
@@ -455,8 +455,8 @@
- yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) - yprs_lift yprs_yprs + fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) + fpbs_lift fpbs_fpbs
@@ -563,8 +563,24 @@ reduction "big tree" parallel reduction - ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) - ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpbc_lift + +
+ + +
+ + + + +
+ + +
+ + fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) + fpb_lift
@@ -1136,6 +1152,6 @@

-
Last update: Fri, 04 Oct 2013 17:03:32 +0200
+
Last update: Sun, 06 Oct 2013 13:50:12 +0200
-- 2.39.2