X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2a5efeb991560de98c15d90ecdf0981b6b168aa0;hb=ab0d181f9a89f461a9c280f42a949a2dc2abe44c;hp=16bb892ad42f9c5997426a51a76f306821d03259;hpb=f5c6d4c41cbbdabdf998be0c4a8242849a790f1b;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 16bb892ad..2a5efeb99 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -163,29 +163,29 @@
@@ -410,9 +410,21 @@
|
- strongly normalizing computation |
- csn_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csn_tstc_vector csn_aaa |
+ strongly normalizing "big tree" computation |
+ fsb ( �,?⦠⢠⦥[?,?] ? ) |
+ fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ fsb_fleq fsb_csx |
+
+
+ |
+
+
+
+
+ |
+ strongly normalizing extended computation |
+ csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_tstc_vector csx_aaa |
|
@@ -427,9 +439,23 @@
|
- csn ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csn_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
- csn_lift csn_lpx |
+ csx ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
+ csx_lift csx_lpx |
+
+
+ |
+
+
+
+
+ |
+ parallel computation for "big tree" normal forms |
+ fpns ( â¦?,?,?⦠⢠ââ¡*[?,?] â¦?,?,?⦠) |
+ fpns_fpns |
+
+
+ |
|
@@ -439,8 +465,8 @@
"big tree" parallel computation |
- ygt ( �,?,?⦠>[?,?] �,?,?⦠) |
- ygt_lift ygt_ygt |
+ fpbr ( â¦?,?,?⦠ââ¥[?,?] â¦?,?,?⦠) |
+ fpbr_fpbr |
|
@@ -455,8 +481,8 @@
|
- yprs ( ? ⢠â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
- yprs_lift yprs_yprs |
+ fpbg ( �,?,?⦠>[?,?] �,?,?⦠) |
+ fpbg_lift fpbg_fpbg |
|
@@ -464,6 +490,20 @@
+
+
+
+ |
+
+
+ |
+ fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
+ fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
+ fpbs_lift fpbs_fleq fpbs_fpbs |
+
+
+ |
+
@@ -563,8 +603,24 @@
|
reduction |
"big tree" parallel reduction |
- ypr ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- ysc ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpbc ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpbc_lift |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpb_lift |
|
@@ -592,7 +648,7 @@
context-sensitive extended reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_ldrop lpx_aaa |
+ lpx_ldrop lpx_aaa lpx_lpx |
|
@@ -608,7 +664,7 @@
cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpx_lift cpx_cix |
+ cpx_lift cpx_cix cpx_cpx |
|
@@ -841,8 +897,8 @@
iterated structural successor for closures |
- fsups ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fsups_fsups |
+ fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_alt fqus_fqus |
|
@@ -857,8 +913,8 @@
|
- fsupp ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fsupp_fsupp |
+ fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_fqup |
|
@@ -923,9 +979,39 @@
relocation |
structural successor for closures |
- fsup ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fsupq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fsupq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+ fquq_fquq |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_fqu |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ lazy equivalence for local environments |
+ lleq ( ? â[?] ? ) |
+ lleq_fleq |
+
+
+ |
|
@@ -1136,6 +1222,6 @@
- Last update: Fri, 04 Oct 2013 17:03:32 +0200
+ Last update: Mon, 25 Nov 2013 15:44:49 +0100