X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2a5efeb991560de98c15d90ecdf0981b6b168aa0;hb=ab0d181f9a89f461a9c280f42a949a2dc2abe44c;hp=6a7c568b1a67d5159a097a7174bf07fc6d1e82e5;hpb=816f8da9c917e86d4de69fe5ae9853ec427f2b57;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 6a7c568b1..2a5efeb99 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 |
|
@@ -855,8 +897,8 @@
iterated structural successor for closures |
- fsups ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fsups_fsups |
+ fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_alt fqus_fqus |
|
@@ -871,8 +913,8 @@
|
- fsupp ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fsupp_fsupp |
+ fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_fqup |
|
@@ -937,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 |
+
+
+ |
|
@@ -1150,6 +1222,6 @@
- Last update: Sun, 06 Oct 2013 17:06:48 +0200
+ Last update: Mon, 25 Nov 2013 15:44:49 +0100