X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=b6ba4f2bef310ac3c810e447efcbb2350b58d18b;hb=c713c14cb3c69b1e9a4c693aed382eedc04512c1;hp=cf44a00e41927a36ade7768d1e4557bcbe1535bb;hpb=93c509f03ffa0d622fa76e39addf32966a173147;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index cf44a00e4..b6ba4f2be 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -163,29 +163,29 @@
sizes |
files |
- 337 |
+ 327 |
characters |
- 575141 |
+ 564871 |
nodes |
- 1625856 |
+ 1606196 |
propositions |
theorems |
105 |
lemmas |
- 1144 |
+ 1107 |
total |
- 1249 |
+ 1212 |
concepts |
declared |
- 51 |
+ 52 |
defined |
- 79 |
+ 76 |
total |
- 130 |
+ 128 |
@@ -431,8 +431,24 @@
strongly normalizing extended computation |
- lsx ( ? ⢠â¬*[?,?,?] ? ) |
- lsx_cpxs lsx_csx |
+ lcosx ( ? ⢠⧤â¬*[?,?,?] ? ) |
+ lcosx_cpxs |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ lsx ( ? ⢠ââ¬*[?,?,?,?] ? ) |
+ lsx_ldrop lsx_cpxs lsx_csx |
|
@@ -565,7 +581,7 @@
context-sensitive extended computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
lpxs_alt ( â¦?,?⦠⢠â¡â¡*[?,?] ? ) |
- lpxs_ldrop lpxs_cpye lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
+ lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
@@ -578,7 +594,7 @@
cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? ) |
- cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
+ cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs |
|
@@ -672,7 +688,7 @@
context-sensitive extended reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_ldrop lpx_cpys lpx_cpye lpx_lleq lpx_aaa |
+ lpx_ldrop lpx_cpys lpx_lleq lpx_aaa |
|
@@ -702,7 +718,7 @@
irreducible forms for context-sensitive extended reduction |
cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
- cix_append cix_lift |
+ cix_lift |
|
@@ -716,7 +732,7 @@
reducible forms for context-sensitive extended reduction |
crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
- crx_append crx_lift |
+ crx_lift |
|
@@ -774,7 +790,7 @@
irreducible forms for context-sensitive reduction |
cir ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
- cir_append cir_lift |
+ cir_lift |
|
@@ -788,7 +804,7 @@
reducible forms for context-sensitive reduction |
crr ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
- crr_append crr_lift |
+ crr_lift |
|
@@ -909,19 +925,7 @@
lazy equivalence for local environments |
lleq ( ? â[?,?] ? ) |
lleq_alt ( ? ââ[?,?] ? ) |
- lleq_ldrop lleq_fqus lleq_cpye lleq_lleq lleq_ext |
-
-
- |
-
-
-
-
- |
- evaluation for contxt-sensitive extended substitution |
- cpye ( â¦?,?⦠⢠? â¶*[?,?] ðâ¦?⦠) |
- cpye_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ðâ¦?⦠) |
- cpye_lift cpye_cpye |
+ lleq_ldrop lleq_fqus lleq_lleq lleq_ext |
|
@@ -933,7 +937,7 @@
contxt-sensitive extended multiple substitution |
cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
- cpys_lift cpys_cny cpys_cpys |
+ cpys_lift cpys_cpys |
|
@@ -1024,20 +1028,6 @@
relocation |
- normal forms for context-sensitive extended substitution |
- cny ( â¦?,?⦠⢠â¶[?,?] ðâ¦?⦠) |
- cny_lift |
-
-
- |
-
-
- |
-
-
-
-
- |
contxt-sensitive extended ordinary substitution |
cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
cpy_lift cpy_cpy |
@@ -1052,9 +1042,9 @@
|
- local env. ref. for extended substitution |
- lsuby ( ? âÃ[?,?] ? ) |
- lsuby_lsuby |
+ restricted local env. ref. |
+ lsubr ( ? â ? ) |
+ lsubr_lsubr |
|
@@ -1066,9 +1056,9 @@
|
- restricted local env. ref. |
- lsubr ( ? â ? ) |
- lsubr_lsubr |
+ local env. ref. for extended substitution |
+ lsuby ( ? âÃ[?,?] ? ) |
+ lsuby_lsuby |
|
@@ -1128,7 +1118,7 @@
basic local env. slicing |
ldrop ( â©[?,?,?] ? â¡ ? ) |
- ldrop_append ldrop_lpx_sn ldrop_ldrop |
+ ldrop_lpx_sn ldrop_leq ldrop_ldrop |
|
@@ -1168,6 +1158,20 @@
grammar |
+ equivalence for local environments |
+ leq ( ? â[?,?] ? ) |
+ leq_leq |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
pointwise extension of a relation |
lpx_sn |
lpx_sn_tc lpx_sn_lpx_sn |
@@ -1197,8 +1201,8 @@
closures |
- cl_shift ( ? @@ ? ) |
- cl_weight ( â¯{?,?,?} ) |
+ cl_weight ( â¯{?,?,?} ) |
+ cl_restricted_weight ( â¯{?,?} ) |
|
@@ -1314,6 +1318,6 @@
- Last update: Tue, 11 Feb 2014 22:11:38 +0100
+ Last update: Fri, 21 Feb 2014 17:37:37 +0100