X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=33356dfc5392d10d2d3514b02f196f717f3f4c94;hb=296f79ae045db68312a245e4111afb554561de42;hp=3779a6c0ff682942794c0fabbdbbcf1925b54137;hpb=7adeb2882d9841c0ab5b357f1652bd42800e77fc;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 3779a6c0f..33356dfc5 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 |
|
@@ -317,7 +317,7 @@
equivalence |
- decomposed extended equivalence |
+ decomposed rt-equivalence |
scpes ( â¦?,?⦠⢠? â¢*â¬*[?,?,?,?] ? ) |
scpes_aaa scpes_cpcs scpes_scpes |
@@ -355,7 +355,7 @@
|
computation |
- evaluation for context-sensitive extended reduction |
+ evaluation for context-sensitive rt-reduction |
cpxe ( â¦?,?⦠⢠â¡*[?,?] ðâ¦?⦠) |
@@ -385,9 +385,9 @@
|
|
- strongly normalizing "big tree" computation |
- fsb ( �,?⦠⢠⦥[?,?] ? ) |
- fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ strongly normalizing qrst-computation |
+ fsb ( ⦥[?,?] �,?,?⦠) |
+ fsb_alt ( ⦥⦥[?,?] �,?,?⦠) |
fsb_aaa fsb_csx |
@@ -397,7 +397,7 @@
|
|
- strongly normalizing extended computation |
+ strongly normalizing rt-computation |
lcosx ( ? ⢠~â¬*[?,?,?] ? ) |
lcosx_cpx |
@@ -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 |
|
@@ -515,7 +483,7 @@
|
- decomposed extended computation |
+ decomposed rt-computation |
scpds ( â¦?,?⦠⢠? â¢*â¡*[?,?,?] ? ) |
scpds_lift scpds_aaa scpds_scpds |
@@ -529,7 +497,7 @@
|
|
- context-sensitive extended computation |
+ context-sensitive rt-computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
@@ -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 |
|
@@ -627,7 +609,7 @@
|
- normal forms for context-sensitive extended reduction |
+ normal forms for context-sensitive rt-reduction |
cnx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
cnx_lift cnx_crx cnx_cix |
@@ -641,7 +623,7 @@
|
|
- context-sensitive extended reduction |
+ context-sensitive rt-reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
lpx_drop lpx_frees lpx_lleq lpx_aaa |
@@ -671,7 +653,7 @@
|
|
- irreducible forms for context-sensitive extended reduction |
+ irreducible forms for context-sensitive rt-reduction |
cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
cix_lift |
@@ -685,7 +667,7 @@
|
|
- reducible forms for context-sensitive extended reduction |
+ reducible forms for context-sensitive rt-reduction |
crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
crx_lift |
@@ -924,7 +906,7 @@
|
pointwise union for local environments |
- llor ( ? â©[?,?] ? â¡ ? ) |
+ llor ( ? â[?,?] ? â¡ ? ) |
llor_alt llor_drop |
@@ -951,7 +933,7 @@
|
|
- contxt-sensitive extended multiple substitution |
+ contxt-sensitive multiple rt-substitution |
cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
cpys_lift cpys_cpys |
@@ -1091,7 +1073,7 @@
|
- contxt-sensitive extended ordinary substitution |
+ contxt-sensitive ordinary rt-substitution |
cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
cpy_lift cpy_nlift cpy_cpy |
@@ -1105,7 +1087,7 @@
|
|
- local env. ref. for extended substitution |
+ local env. ref. for rt-substitution |
lsuby ( ? â[?,?] ? ) |
lsuby_lsuby |
@@ -1321,6 +1303,6 @@
- Last update: Mon, 15 Sep 2014 16:17:55 +0200
+ Last update: Thu, 09 Oct 2014 20:11:24 +0200
|