X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=b0891996f5b4d39903a43e15d6654452a0ad9efc;hb=9b75ad80a3ee31314c02f113b255ad533a87d3d2;hp=d48c03de785f09136188205e128fd41bbb29e62f;hpb=6f1f9e20aa2775d41bba64289fc903e6612baaf3;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index d48c03de7..b0891996f 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -58,20 +58,20 @@
computation |
- evaluation for context-sensitive extended reduction |
+ evaluation for context-sensitive rt-reduction |
cpxe ( â¦?,?⦠⢠â¡*[?,?] ðâ¦?⦠) |
@@ -397,7 +397,7 @@
|
|
- strongly normalizing extended computation |
+ strongly normalizing rt-computation |
lcosx ( ? ⢠~â¬*[?,?,?] ? ) |
lcosx_cpx |
@@ -474,7 +474,7 @@
|
fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbu fpbs_fpbc fpbs_fpbs |
+ fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
|
@@ -483,7 +483,7 @@
|
- decomposed extended computation |
+ decomposed rt-computation |
scpds ( â¦?,?⦠⢠? â¢*â¡*[?,?,?] ? ) |
scpds_lift scpds_aaa scpds_scpds |
@@ -497,7 +497,7 @@
|
|
- context-sensitive extended computation |
+ context-sensitive rt-computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
@@ -582,27 +582,9 @@
|
-
-
- |
-
-
- |
- fpbu ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpbu_lift fpbu_lleq fpbu_fleq |
-
-
- |
+ fpbq ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpbq_alt ( â¦?,?,?⦠â½â½[?,?] â¦?,?,?⦠) |
+ fpbq_lift fpbq_aaa |
|
@@ -614,8 +596,8 @@
|
- fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- fpb_lift fpb_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 |
@@ -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: Thu, 02 Oct 2014 23:21:16 +0200
+ Last update: Sun, 05 Oct 2014 16:38:32 +0200
|