X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=007aded03ab5ea453de4ad46f28b87679602e84c;hb=3a47f3e553f17690908dfcacfdfa58c0da378a9b;hp=2fd65b8cd1e980dca197760d1c519ce671381393;hpb=8913001064f595c21ed4234884e7c370be2afb52;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 2fd65b8cd..007aded03 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -163,29 +163,29 @@
@@ -410,7 +410,19 @@
|
- strongly normalizing computation |
+ strongly normalizing "big tree" computation |
+ fsb ( �,?⦠⢠⦥[?,?] ? ) |
+ fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ fsb_fleq fsb_csx |
+
+
+ |
+
+
+
+
+ |
+ strongly normalizing extended computation |
csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
csx_tstc_vector csx_aaa |
@@ -434,11 +446,41 @@
|
+
+
+
+ |
+ parallel computation for "big tree" normal forms |
+ fpns ( â¦?,?,?⦠⢠ââ¡*[?,?] â¦?,?,?⦠) |
+ fpns_fpns |
+
+
+ |
+
+
+ |
+
|
"big tree" parallel computation |
+ fpbr ( â¦?,?,?⦠ââ¥[?,?] â¦?,?,?⦠) |
+ fpbr_fpbr |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
fpbg ( �,?,?⦠>[?,?] �,?,?⦠) |
fpbg_lift fpbg_fpbg |
@@ -457,7 +499,7 @@
|
fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fpbs |
+ fpbs_lift fpbs_fleq fpbs_fpbs |
|
@@ -606,7 +648,7 @@
context-sensitive extended reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_ldrop lpx_aaa |
+ lpx_ldrop lpx_aaa lpx_lpx |
|
@@ -622,7 +664,7 @@
cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpx_lift cpx_cix |
+ cpx_lift cpx_cix cpx_cpx |
|
@@ -856,7 +898,7 @@
iterated structural successor for closures |
fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_fqus |
+ fqus_alt fqus_fqus |
|
@@ -937,9 +979,39 @@
relocation |
structural successor for closures |
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+ fquq_fquq |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_fqu |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ lazy equivalence for local environments |
+ lleq ( ? â[?] ? ) |
+ lleq_fleq |
+
+
+ |
|
@@ -1150,6 +1222,6 @@
- Last update: Sat, 12 Oct 2013 19:38:34 +0200
+ Last update: Sun, 03 Nov 2013 13:06:26 +0100