X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=1d89601876e0a0265bd633aa204801c0feeb1b17;hb=b3a5ce99c235f834df054a3f76379bcc40a0c370;hp=c41d2132cbc9064cadfbf8b26ae5f79d841f0fcc;hpb=9ffbf46176fb5f81768255992e46e69689663d69;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index c41d2132c..1d8960187 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -163,29 +163,29 @@
@@ -293,7 +293,7 @@
Logical Structure of the Specification
The source files are grouped in planes and components
according to the following table.
- A notation file covering the whole specification is provided.
+ Notation files covering the whole specification are provided.
The notation for the relations or functions introduced in each file
is shown in parentheses (? are placeholders).
@@ -413,7 +413,7 @@
strongly normalizing "big tree" computation |
fsb ( �,?⦠⢠⦥[?,?] ? ) |
fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
- fsb_csx |
+ fsb_aaa fsb_csx |
|
@@ -423,6 +423,22 @@
strongly normalizing extended computation |
+ lsx ( ? ⢠â¬*[?,?,?] ? ) |
+ lsx_cpxs lsx_csx |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
csx_tstc_vector csx_aaa |
@@ -441,7 +457,7 @@
|
csx ( â¦?,?⦠⢠â¬*[?,?] ? ) |
csx_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
- csx_lift csx_lpx |
+ csx_lift csx_lpx csx_fpbs |
|
@@ -451,8 +467,8 @@
"big tree" parallel computation |
- fpbr ( â¦?,?,?⦠ââ¥[?,?] â¦?,?,?⦠) |
- fpbr_fpbr |
+ fpbg ( â¦?,?,?⦠>â[?,?] â¦?,?,?⦠) |
+ fpbg_lift fpbg_fpns fpbg_fpbg |
|
@@ -467,8 +483,24 @@
|
- fpbg ( �,?,?⦠>[?,?] �,?,?⦠) |
- fpbg_lift fpbg_fpbg |
+ fpbc ( â¦?,?,?⦠â»â[?,?] â¦?,?,?⦠) |
+ fpbc_fpns fpbc_fpbs |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fpbu ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpbu_lift fpbu_fpns |
|
@@ -485,7 +517,21 @@
fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fpbs |
+ fpbs_lift fpbs_fpns fpbs_fpbs |
+
+
+ |
+
+
+
+
+ |
+ parallel computation for "big tree" normal forms |
+ fpns ( â¦?,?,?⦠⢠ââ¡*[?,?] â¦?,?,?⦠) |
+ fpns_fpns |
+
+
+ |
|
@@ -511,7 +557,7 @@
context-sensitive extended computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
lpxs_alt ( â¦?,?⦠⢠â¡â¡*[?,?] ? ) |
- lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs |
+ lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
@@ -524,7 +570,7 @@
cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? ) |
- cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs |
+ cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
|
@@ -589,22 +635,6 @@
reduction |
"big tree" parallel reduction |
- fpbc ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpbc_lift |
-
-
- |
-
-
- |
-
-
-
-
- |
-
-
- |
fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
fpb_lift |
@@ -634,7 +664,7 @@
|
context-sensitive extended reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_ldrop lpx_aaa |
+ lpx_leq lpx_ldrop lpx_lleq lpx_aaa |
|
@@ -650,7 +680,7 @@
cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpx_lift cpx_cix |
+ cpx_leq cpx_lift cpx_cix |
|
@@ -884,7 +914,7 @@
iterated structural successor for closures |
fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_alt fqus_fqus |
+ fqus_alt fqus_lleq fqus_fqus |
|
@@ -900,7 +930,7 @@
fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fqup_fqup |
+ fqup_lleq fqup_fqup |
|
@@ -965,9 +995,39 @@
relocation |
structural successor for closures |
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+ fquq_lleq |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_lleq |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ lazy equivalence for local environments |
+ lleq ( ? â[?,?] ? ) |
+ lleq_lleq |
+
+
+ |
|
@@ -992,7 +1052,7 @@
basic local env. slicing |
ldrop ( â©[?,?] ? â¡ ? ) |
- ldrop_append ldrop_lpx_sn ldrop_ldrop |
+ ldrop_append ldrop_lpx_sn ldrop_leq ldrop_ldrop |
|
@@ -1032,6 +1092,22 @@
grammar |
+ equivalence for local environments |
+ leq ( ? â[?,?] ? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
pointwise extension of a relation |
lpx_sn |
lpx_sn_tc lpx_sn_lpx_sn |
@@ -1178,6 +1254,6 @@
- Last update: Sat, 26 Oct 2013 19:48:51 +0200
+ Last update: Sat, 14 Dec 2013 23:22:14 +0100