X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=f99504f88b5674c5d95394983e1809a7dfc28d23;hb=ff50a881cc8adf0aa2af7cfc0649bff35efc2f69;hp=ba7649484baac736a81f363e076c315e1e8f861b;hpb=775106f04b47236bf47e4321d745ec360ab4ebb4;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index ba7649484..f99504f88 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -144,29 +144,29 @@
component |
+ section |
plane |
files |
@@ -393,13 +394,15 @@
|
rt-conversion |
- context-sensitive r-conversion |
+ context-sensitive parallel r-conversion |
+ for terms |
cpc ( â¦?,?⦠⢠? â¬[?] ? ) |
cpc_cpc |
rt-computation |
- uncounted context-sensitive rt-computation |
+ uncounted context-sensitive parallel rt-computation |
+ refinement for lenvs |
lsubsx ( ? ⢠? ââ§[?,?,?] ? ) |
lsubsx_lfsx lsubsx_lsubsx |
@@ -407,9 +410,10 @@
|
-
+ |
|
+ strongly normalizing on referred entries for lenvs |
lfsx ( ? ⢠â¬*[?,?,?] ðâ¦?⦠) |
lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx |
@@ -417,9 +421,10 @@
|
-
+ |
|
+ strongly normalizing for term vectors |
csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
csx_cnx_vector csx_csx_vector |
@@ -427,9 +432,10 @@
|
-
+ |
|
+ strongly normalizing for terms |
csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx |
@@ -437,9 +443,10 @@
|
-
+ |
|
+ on referred entries for lenvs |
lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs |
@@ -447,15 +454,17 @@
|
-
+ |
|
+ for terms |
cpxs ( â¦?,?⦠⢠? â¬*[?] ? ) |
cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lfpx cpxs_cnx cpxs_cpxs |
rt-transition |
- uncounted rst-transition |
+ uncounted parallel rst-transition |
+ for closures |
fpbq ( â¦?,?,?⦠â½[?] â¦?,?,?⦠) |
fpbq_aaa |
@@ -463,9 +472,10 @@
|
-
+ |
|
+ proper for closures |
fpb ( â¦?,?,?⦠â»[?] â¦?,?,?⦠) |
fpb_lfdeq |
@@ -473,7 +483,8 @@
|
- t-bound context-sensitive rt-transition |
+ context-sensitive parallel r-transition |
+ for lenvs on referred entries |
lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
@@ -481,9 +492,10 @@
|
-
+ |
|
+ for binders |
cpr_ext ( â¦?,?⦠⢠? â¡[?] ? ) |
@@ -493,9 +505,10 @@
|
|
-
+ |
|
+ for terms |
cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
cpr_drops |
@@ -503,9 +516,8 @@
|
-
-
- |
+ t-bound context-sensitive parallel rt-transition |
+ for terms |
cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx |
@@ -513,7 +525,8 @@
|
- uncounted context-sensitive rt-transition |
+ uncounted context-sensitive parallel rt-transition |
+ normal form for terms |
cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠) |
cnx_simple cnx_drops cnx_cnx |
@@ -521,9 +534,10 @@
|
-
+ |
|
+ for lenvs on referred entries |
lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx |
@@ -531,9 +545,10 @@
|
-
+ |
|
+ for binders |
cpx_ext ( â¦?,?⦠⢠? â¬[?] ? ) |
@@ -543,9 +558,10 @@
|
|
-
+ |
|
+ for terms |
cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs |
@@ -553,19 +569,22 @@
|
- counted context-sensitive rt-transition |
+ counted context-sensitive parallel rt-transition |
+ for terms |
cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
cpg_simple cpg_drops cpg_lsubr |
iterated static typing |
- iterated extension on referred entries |
+ iterated extension on referred entries |
+ |
tc_lfxs ( ? ⦻**[?,?] ? ) |
- tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
+ tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
static typing |
- generic reducibility |
+ generic reducibility |
+ |
lsubc ( ? ⢠? â«[?] ? ) |
lsubc_drops lsubc_lsubr lsubc_lsuba |
@@ -573,9 +592,10 @@
|
-
+ |
|
+ |
gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
gcp_aaa |
@@ -583,9 +603,10 @@
|
-
+ |
|
+ |
gcp |
@@ -595,7 +616,8 @@
|
|
- atomic arity assignment |
+ atomic arity assignment |
+ |
lsuba ( ? ⢠? â«â ? ) |
lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
@@ -603,9 +625,10 @@
|
-
+ |
|
+ |
aaa ( â¦?,?⦠⢠? â ? ) |
aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
@@ -613,7 +636,8 @@
|
- degree-based equivalence on referred entries |
+ degree-based equivalence on referred entries |
+ |
ffdeq ( â¦?,?,?⦠â[?,?] â¦?,?,?⦠) |
ffdeq_fqup ffdeq_ffdeq |
@@ -621,9 +645,10 @@
|
-
+ |
|
+ |
lfdeq ( ? â[?,?,?] ? ) |
lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
@@ -631,7 +656,17 @@
|
- generic extension on referred entries |
+ syntactic equivalence on referred entries |
+ |
+ lfeq ( ? â¡[?] ? ) |
+ lfeq_fqup lfeq_lfeq |
+
+
+
+
+ |
+ generic extension on referred entries |
+ |
lfxs ( ? ⦻*[?,?] ? ) |
lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
@@ -639,7 +674,8 @@
|
- context-sensitive free variables |
+ context-sensitive free variables |
+ |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
lsubf_lsubr lsubf_frees lsubf_lsubf |
@@ -647,9 +683,10 @@
|
-
+ |
|
+ |
frees ( ? ⢠ð
*�⦠⡠? ) |
frees_drops frees_fqup frees_frees |
@@ -657,13 +694,15 @@
|
- restricted ref. for local env. |
+ restricted ref. for local env. |
+ |
lsubr ( ? â« ? ) |
lsubr_length lsubr_drops lsubr_lsubr |
s-computation |
- iterated structural successor for closures |
+ iterated structural successor for closures |
+ |
fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) |
fqus_weight fqus_drops fqus_fqup fqus_fqus |
@@ -671,15 +710,17 @@
|
-
+ |
|
+ |
fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
fqup_weight fqup_drops fqup_fqup |
s-transition |
- structural successor for closures |
+ structural successor for closures |
+ |
fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_length fquq_weight |
@@ -687,15 +728,17 @@
|
-
+ |
|
+ |
fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
fqu_length fqu_weight |
relocation |
- generic slicing for local environments |
+ generic slicing for local environments |
+ |
drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
@@ -705,17 +748,19 @@
|
|
-
+ |
|
+ |
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops |
+ drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops |
|
- generic relocation |
+ generic relocation |
+ |
lifts_bind ( â¬*[?] ? â¡ ? ) |
lifts_weight_bind lifts_lifts_bind |
@@ -723,9 +768,10 @@
|
-
+ |
|
+ |
lifts_vector ( â¬*[?] ? â¡ ? ) |
lifts_lifts_vector |
@@ -733,9 +779,10 @@
|
-
+ |
|
+ |
lifts ( â¬*[?] ? â¡ ? ) |
lifts_simple lifts_weight lifts_tdeq lifts_lifts |
@@ -743,7 +790,8 @@
|
- ranged equivalence for local environments |
+ ranged equivalence for local environments |
+ |
lreq ( ? â¡[?] ? ) |
lreq_length lreq_lreq |
@@ -751,13 +799,28 @@
|
- generic entrywise extension |
+ generic entrywise extension |
+ |
+ lex ( ? ⦻[?] ? ) |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ |
lexs ( ? ⦻*[?,?,?] ? ) |
- lexs_length lexs_lexs |
+ lexs_tc lexs_length lexs_lexs |
syntax |
- append for local environments |
+ append for local environments |
+ |
append ( ? @@ ? ) |
append_length |
@@ -765,7 +828,8 @@
|
- head equivalence for terms |
+ head equivalence for terms |
+ |
theq ( ? ⩳[?,?] ? ) |
theq_simple theq_tdeq theq_theq theq_simple_vector |
@@ -773,7 +837,8 @@
|
- degree-based equivalence |
+ degree-based equivalence |
+ |
tdeq_ext ( ? â[?,?] ? ) ( ? ⢠? â[?,?] ? ) |
@@ -783,9 +848,10 @@
|
|
-
+ |
|
+ |
tdeq ( ? â[?,?] ? ) |
tdeq_tdeq |
@@ -793,7 +859,8 @@
|
- closures |
+ closures |
+ |
cl_weight ( â¯{?,?,?} ) |
@@ -803,9 +870,10 @@
|
|
-
+ |
|
+ |
cl_restricted_weight ( â¯{?,?} ) |
@@ -815,7 +883,8 @@
|
|
- global environments |
+ global environments |
+ |
genv |
@@ -825,8 +894,20 @@
|
|
- local environments |
- lenv_ext2 |
+ local environments |
+ |
+ ceq_ext |
+ ceq_ext_ceq_ext |
+
+
+
+
+ |
+
+
+ |
+ |
+ cext2 |
|
@@ -835,9 +916,10 @@
|
-
+ |
|
+ |
lenv_length ( |?| ) |
@@ -847,9 +929,10 @@
|
|
-
+ |
|
+ |
lenv_weight ( â¯{?} ) |
@@ -859,9 +942,10 @@
|
|
-
+ |
|
+ |
lenv |
@@ -871,17 +955,19 @@
|
|
- binders for local environments |
+ binders for local environments |
+ |
ext2 |
- ext2_ext2 |
+ ext2_tc ext2_ext2 |
|
-
+ |
|
+ |
bind |
bind_weight |
@@ -889,7 +975,8 @@
|
- terms |
+ terms |
+ |
term_vector ( �.? ) |
@@ -899,9 +986,10 @@
|
|
-
+ |
|
+ |
term_simple ( ðâ¦?⦠) |
@@ -911,9 +999,10 @@
|
|
-
+ |
|
+ |
term_weight ( â¯{?} ) |
@@ -923,9 +1012,10 @@
|
|
-
+ |
|
+ |
term |
@@ -935,7 +1025,8 @@
|
|
- items |
+ items |
+ |
item_sd |
@@ -945,9 +1036,10 @@
|
|
-
+ |
|
+ |
item_sh |
@@ -957,9 +1049,10 @@
|
|
-
+ |
|
+ |
item |
@@ -969,7 +1062,8 @@
|
|
- atomic arities |
+ atomic arities |
+ |
aarity |
@@ -1004,6 +1098,6 @@
- Last update: Tue, 14 Nov 2017 16:10:30 +0100
+ Last update: Wed, 22 Nov 2017 22:20:05 +0100
|