X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=374c3a7db77cd311b68881174df388362bc7e6ad;hb=b7de6afb9d3260ffea86ddf824e497419e1b56fb;hp=765da98303a8e893763f1cf116374eb6bf280b96;hpb=e866d78af74246133f5a14cb711a62af39308dee;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 765da9830..374c3a7db 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,6 +1,108 @@ -
category | objects | |||||
sizes | files | 213 | characters | 224056 | nodes | 1100545 |
propositions | theorems | 61 | lemmas | 743 | total | 804 |
concepts | declared | 29 | defined | 66 | total | 95 |
category | +objects | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
sizes | +files | +212 | +characters | +213959 | +nodes | +1057531 | +
propositions | +theorems | +62 | +lemmas | +741 | +total | +803 | +
concepts | +declared | +31 | +defined | +78 | +total | +109 | +
component | plane | files | |
rt-computation | uncounted context-sensitive rt-transition | csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) | |
csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) | csx_cnx csx_cpxs csx_csx | ||
lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) | lfpxs_length lfpxs_fqup | ||
cpxs ( â¦?,?⦠⢠? â¬*[?] ? ) | cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs | ||
rt-transition | parallel qrst-transition | fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) | |
t-bound context-sensitive rt-transition | lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) | lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr | |
cpr ( â¦?,?⦠⢠? â¡[?] ? ) | cpr_drops | ||
cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) | cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx | ||
uncounted context-sensitive rt-transition | cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠) | cnx_simple cnx_drops | |
lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) | lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx | ||
cpx ( â¦?,?⦠⢠? â¬[?] ? ) | cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs | ||
counted context-sensitive rt-transition | cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) | cpg_simple cpg_drops cpg_lsubr | |
iterated static typing | iterated extension on referred entries | tc_lfxs ( ? ⦻**[?,?] ? ) | |
static typing | generic reducibility | lsubc ( ? ⢠? â«[?] ? ) | lsubc_drops lsubc_lsubr lsubc_lsuba |
gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) | gcp_aaa | ||
gcp | |||
atomic arity assignment | lsuba ( ? ⢠? â«â ? ) | lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba | |
aaa ( â¦?,?⦠⢠? â ? ) | aaa_drops aaa_fqus aaa_lfdeq aaa_aaa | ||
degree-based equivalence on referred entries | ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠) | ffdeq_fqup ffdeq_ffdeq | |
lfdeq ( ? â¡[?,?,?] ? ) | lfdeq_length lfdeq_fqup lfdeq_lfdeq | ||
generic extension on referred entries | lfxs ( ? ⦻*[?,?] ? ) | lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs | |
context-sensitive free variables | lsubf ( â¦?,?⦠â«ð * â¦?,?⦠) | lsubf_frees | |
frees ( ? ⢠ð *â¦?⦠⡠? ) | frees_drops frees_fqup frees_frees | ||
restricted ref. for local env. | lsubr ( ? â« ? ) | lsubr_length lsubr_drops lsubr_lsubr | |
s-computation | iterated structural successor for closures | fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) | fqus_weight fqus_drops fqus_fqup fqus_fqus |
fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) | fqup_weight fqup_drops fqup_fqup | ||
s-transition | structural successor for closures | fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) | fquq_length fquq_weight |
fqu ( â¦?,?,?⦠â â¦?,?,?⦠) | fqu_length fqu_weight | ||
relocation | generic slicing for local environments | drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) | |
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) | drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops | ||
generic relocation for terms | lifts_vector ( â¬*[?] ? â¡ ? ) | lifts_lifts_vector | |
lifts ( â¬*[?] ? â¡ ? ) | lifts_simple lifts_weight lifts_tdeq lifts_lifts | ||
ranged equivalence for local environments | lreq ( ? â¡[?] ? ) | lreq_length lreq_lreq | |
generic entrywise extension | lexs ( ? ⦻*[?,?,?] ? ) | lexs_length lexs_lexs | |
syntax | append for local environments | append ( ? @@ ? ) | append_length |
degree-based equivalence for terms | deq ( ? â¡[?,?] ? ) | deq_deq | |
same top term structure | tsts ( ? â ? ) | tsts_tsts tsts_vector | |
closures | cl_weight ( â¯{?,?,?} ) | ||
cl_restricted_weight ( â¯{?,?} ) | |||
global environments | genv | ||
local environments | lenv_length ( |?| ) | ||
lenv_weight ( â¯{?} ) | |||
lenv | |||
terms | term_vector ( �.? ) | ||
term_simple ( ðâ¦?⦠) | |||
term_weight ( â¯{?} ) | |||
term | |||
items | item_sd | ||
item_sh | |||
item | |||
atomic arities | aarity |
component | +plane | +files | +
+ + |
+
rt-transition | +counted context-sensitive rt-transition | +cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) | +cpg_simple cpg_drops cpg_lsubr | +
iterated static typing | +iterated extension on referred entries | +tc_lfxs ( ? ⦻**[?,?] ? ) | +tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs | +
static typing | +generic reducibility | +lsubc ( ? ⢠? â«[?] ? ) | +lsubc_drops lsubc_lsubr lsubc_lsuba | +
+ + |
+
+ + |
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) | +gcp_aaa | +
+ + |
+
+ + |
+ gcp | +
+ + |
+
+ + |
+ atomic arity assignment | +lsuba ( ? ⢠? â«â ? ) | +lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba | +
+ + |
+
+ + |
+ aaa ( â¦?,?⦠⢠? â ? ) | +aaa_drops aaa_fqus aaa_lfdeq aaa_aaa | +
+ + |
+ degree-based equivalence on referred entries | +ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠) | +ffdeq_fqup ffdeq_ffdeq | +
+ + |
+
+ + |
+ lfdeq ( ? â¡[?,?,?] ? ) | +lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq | +
+ + |
+ generic extension on referred entries | +lfxs ( ? ⦻*[?,?] ? ) | +lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs | +
+ + |
+ context-sensitive free variables | +lsubf ( â¦?,?⦠â«ð * â¦?,?⦠) | +lsubf_lsubr lsubf_frees lsubf_lsubf | +
+ + |
+
+ + |
+ frees ( ? ⢠ð *â¦?⦠⡠? ) | +frees_drops frees_fqup frees_frees | +
+ + |
+ restricted ref. for local env. | +lsubr ( ? â« ? ) | +lsubr_length lsubr_drops lsubr_lsubr | +
s-computation | +iterated structural successor for closures | +fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) | +fqus_weight fqus_drops fqus_fqup fqus_fqus | +
+ + |
+
+ + |
+ fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) | +fqup_weight fqup_drops fqup_fqup | +
s-transition | +structural successor for closures | +fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) | +fquq_length fquq_weight | +
+ + |
+
+ + |
+ fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) | +fqu_length fqu_weight | +
relocation | +generic slicing for local environments | +drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) | +
+ + |
+
+ + |
+
+ + |
+ drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) | +drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops | +
+ + |
+ generic relocation | +lifts_bind ( â¬*[?] ? â¡ ? ) | +lifts_weight_bind lifts_lifts_bind | +
+ + |
+
+ + |
+ lifts_vector ( â¬*[?] ? â¡ ? ) | +lifts_lifts_vector | +
+ + |
+
+ + |
+ lifts ( â¬*[?] ? â¡ ? ) | +lifts_simple lifts_weight lifts_tdeq lifts_lifts | +
+ + |
+ ranged equivalence for local environments | +lreq ( ? â¡[?] ? ) | +lreq_length lreq_lreq | +
+ + |
+ generic entrywise extension | +lexs ( ? ⦻*[?,?,?] ? ) | +lexs_length lexs_lexs | +
syntax | +append for local environments | +append ( ? @@ ? ) | +append_length | +
+ + |
+ head equivalence for terms | +theq ( ? ⩳[?,?] ? ) | +theq_simple theq_tdeq theq_theq theq_simple_vector | +
+ + |
+ degree-based equivalence | +tdeq_ext ( ? â¡[?,?] ? ) | +
+ + |
+
+ + |
+
+ + |
+ tdeq ( ? â¡[?,?] ? ) | +tdeq_tdeq | +
+ + |
+ closures | +cl_weight ( â¯{?,?,?} ) | +
+ + |
+
+ + |
+
+ + |
+ cl_restricted_weight ( â¯{?,?} ) | +
+ + |
+
+ + |
+ global environments | +genv | +
+ + |
+
+ + |
+ local environments | +lenv_ext2 | +
+ + |
+
+ + |
+
+ + |
+ lenv_length ( |?| ) | +
+ + |
+
+ + |
+
+ + |
+ lenv_weight ( â¯{?} ) | +
+ + |
+
+ + |
+
+ + |
+ lenv | +
+ + |
+
+ + |
+ binders for local environments | +ext2 | +ext2_ext2 | +
+ + |
+
+ + |
+ bind | +bind_weight | +
+ + |
+ terms | +term_vector ( �.? ) | +
+ + |
+
+ + |
+
+ + |
+ term_simple ( ðâ¦?⦠) | +
+ + |
+
+ + |
+
+ + |
+ term_weight ( â¯{?} ) | +
+ + |
+
+ + |
+
+ + |
+ term | +
+ + |
+
+ + |
+ items | +item_sd | +
+ + |
+
+ + |
+
+ + |
+ item_sh | +
+ + |
+
+ + |
+
+ + |
+ item | +
+ + |
+
+ + |
+ atomic arities | +aarity | +
+ + |
+