X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=b2fec951153ebe0d0e552f62b6b675da56a1264e;hb=d48d412796a295256c048256c8f7a843e3406980;hp=3a00820c886f3835965f70ae62536878404e2f04;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 3a00820c8..b2fec9511 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -58,29 +58,29 @@
@@ -246,7 +246,7 @@
examples |
terms with special features |
- ex_sta_ldec ex_cpr_omega |
+ ex_sta_ldec ex_cpr_omega ex_fpbg_refl |
|
@@ -385,7 +385,7 @@
|
- strongly normalizing "big tree" computation |
+ strongly normalizing qrst-computation |
fsb ( �,?⦠⢠⦥[?,?] ? ) |
fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
fsb_aaa fsb_csx |
@@ -455,41 +455,9 @@
|
- "big tree" parallel computation |
+ parallel qrst-computation |
fpbg ( â¦?,?,?⦠>â¡[?,?] â¦?,?,?⦠) |
- fpbg_lift fpbg_fleq fpbg_fpbg |
-
-
- |
-
-
- |
-
-
-
-
- |
-
-
- |
- fpbc ( â¦?,?,?⦠â»â¡[?,?] â¦?,?,?⦠) |
- fpbc_fleq fpbc_fpbs |
-
-
- |
-
-
- |
-
-
-
-
- |
-
-
- |
- fpbu ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpbu_lift fpbu_lleq fpbu_fleq |
+ fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg |
|
@@ -506,7 +474,7 @@
fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext |
+ fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
|
@@ -613,9 +581,23 @@
reduction |
- "big tree" parallel reduction |
- fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- fpb_lift fpb_aaa |
+ parallel qrst-reduction |
+ fpbq ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpbq_alt ( â¦?,?,?⦠â½â½[?,?] â¦?,?,?⦠) |
+ fpbq_lift fpbq_aaa |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpb_lift fpb_lleq fpb_fleq |
|
@@ -924,7 +906,7 @@
pointwise union for local environments |
- llor ( ? â©[?,?] ? â¡ ? ) |
+ llor ( ? â[?,?] ? â¡ ? ) |
llor_alt llor_drop |
@@ -994,7 +976,7 @@
|
iterated local env. slicing |
- drops ( â©*[?,?] ? â¡ ? ) |
+ drops ( â¬*[?,?] ? â¡ ? ) |
drops_drop drops_drops |
@@ -1008,7 +990,7 @@
|
generic term relocation |
- lifts_vector ( â§*[?] ? â¡ ? ) |
+ lifts_vector ( â¬*[?] ? â¡ ? ) |
lifts_lift_vector |
@@ -1024,7 +1006,7 @@
|
|
- lifts ( â§*[?] ? â¡ ? ) |
+ lifts ( â¬*[?] ? â¡ ? ) |
lifts_lift lifts_lifts |
@@ -1078,7 +1060,7 @@
|
global env. slicing |
- gget ( â©[?] ? â¡ ? ) |
+ gget ( â¬[?] ? â¡ ? ) |
gget_gget |
@@ -1134,7 +1116,7 @@
|
basic local env. slicing |
- drop ( â©[?,?,?] ? â¡ ? ) |
+ drop ( â¬[?,?,?] ? â¡ ? ) |
drop_append drop_leq drop_drop |
@@ -1148,7 +1130,7 @@
|
basic term relocation |
- lift_vector ( â§[?,?] ? â¡ ? ) |
+ lift_vector ( â¬[?,?] ? â¡ ? ) |
lift_lift_vector |
@@ -1164,7 +1146,7 @@
|
|
- lift ( â§[?,?] ? â¡ ? ) |
+ lift ( â¬[?,?] ? â¡ ? ) |
lift_neq lift_lift |
@@ -1321,6 +1303,6 @@
- Last update: Sun, 14 Sep 2014 23:26:35 +0200
+ Last update: Sat, 04 Oct 2014 22:58:58 +0200
|