X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=b2954f5e726dbcffa8762384a8698bb753092c48;hb=bba53a83579540bc3925d47d679e2aad22e85755;hp=a281ef3ab90034290ee427fe076111d3e4972711;hpb=1e89c373698e2b5e55661291f25dc5238e9f13fd;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index a281ef3ab..b2954f5e7 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -144,29 +144,29 @@
sizes |
files |
- 177 |
+ 178 |
characters |
- 181483 |
+ 183178 |
nodes |
- 952913 |
+ 957953 |
propositions |
theorems |
- 49 |
+ 48 |
lemmas |
- 633 |
+ 630 |
total |
- 682 |
+ 678 |
concepts |
declared |
- 24 |
+ 25 |
defined |
- 42 |
+ 43 |
total |
- 66 |
+ 68 |
@@ -358,12 +358,6 @@
component |
plane |
files |
-
-
- |
-
-
- |
|
@@ -372,13 +366,7 @@
rt-transition |
t-bound context-sensitive rt-transition |
lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
-
-
- |
-
-
- |
+ lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
@@ -388,13 +376,7 @@
|
cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
- cpr_drops |
-
-
- |
-
-
- |
+ cpr_drops |
@@ -404,13 +386,7 @@
|
cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpm_simple cpm_drops cpm_lsubr cpm_cpx |
-
-
- |
-
-
- |
+ cpm_simple cpm_drops cpm_lsubr cpm_cpx |
@@ -418,13 +394,7 @@
|
uncounted context-sensitive rt-transition |
lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa |
-
-
- |
-
-
- |
+ lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa |
@@ -434,13 +404,7 @@
|
cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_lsubr |
-
-
- |
-
-
- |
+ cpx_simple cpx_drops cpx_lsubr |
@@ -448,39 +412,13 @@
|
counted context-sensitive rt-transition |
cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
- cpg_simple cpg_drops cpg_lsubr |
-
-
- |
-
-
- |
+ cpg_simple cpg_drops cpg_lsubr |
static typing |
- parameters |
- sh |
- sd |
-
-
- |
-
-
- |
-
-
-
-
- |
restricted ref. for atomic arity assignment |
lsuba ( ? ⢠? â«â ? ) |
- lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
-
-
- |
-
-
- |
+ lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
@@ -488,13 +426,7 @@
|
atomic arity assignment |
aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_drops aaa_fqus aaa_lfeq aaa_aaa |
-
-
- |
-
-
- |
+ aaa_drops aaa_fqus aaa_lfeq aaa_aaa |
@@ -502,13 +434,7 @@
|
equivalence for closures on referred entries |
ffeq ( �,?,?⦠⡠�,?,?⦠) |
- ffeq_freq |
-
-
- |
-
-
- |
+ ffeq_freq |
@@ -516,13 +442,7 @@
|
equivalence for local environments on referred entries |
lfeq ( ? â¡[?] ? ) |
- lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq |
-
-
- |
-
-
- |
+ lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq |
@@ -530,13 +450,7 @@
|
generic extension on referred entries |
lfxs ( ? ⦻*[?,?] ? ) |
- lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
-
-
- |
-
-
- |
+ lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
@@ -544,13 +458,7 @@
|
restricted ref. for context-sensitive free variables |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
- lsubf_frees |
-
-
- |
-
-
- |
+ lsubf_frees |
@@ -558,13 +466,7 @@
|
context-sensitive free variables |
frees ( ? ⢠ð
*�⦠⡠? ) |
- frees_weight frees_lreq frees_drops frees_fqup frees_frees |
-
-
- |
-
-
- |
+ frees_weight frees_lreq frees_drops frees_fqup frees_frees |
@@ -572,25 +474,13 @@
|
restricted ref. for local env. |
lsubr ( ? â« ? ) |
- lsubr_length lsubr_drops lsubr_lsubr |
-
-
- |
-
-
- |
+ lsubr_length lsubr_drops lsubr_lsubr |
s-computation |
iterated structural successor for closures |
fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_weight fqus_drops fqus_fqup fqus_fqus |
-
-
- |
-
-
- |
+ fqus_weight fqus_drops fqus_fqup fqus_fqus |
@@ -600,25 +490,13 @@
|
fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fqup_weight fqup_drops fqup_fqup |
-
-
- |
-
-
- |
+ fqup_weight fqup_drops fqup_fqup |
s-transition |
structural successor for closures |
fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fquq_length fquq_weight |
-
-
- |
-
-
- |
+ fquq_length fquq_weight |
@@ -628,24 +506,12 @@
|
fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fqu_length fqu_weight |
-
-
- |
-
-
- |
+ fqu_length fqu_weight |
relocation |
generic slicing for local environments |
drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
-
-
- |
-
-
- |
|
@@ -658,13 +524,7 @@
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
-
-
- |
-
-
- |
+ drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
@@ -672,13 +532,7 @@
|
generic relocation for terms |
lifts_vector ( â¬*[?] ? â¡ ? ) |
- lifts_lifts_vector |
-
-
- |
-
-
- |
+ lifts_lifts_vector |
@@ -688,13 +542,7 @@
|
lifts ( â¬*[?] ? â¡ ? ) |
- lifts_simple lifts_weight lifts_lifts |
-
-
- |
-
-
- |
+ lifts_simple lifts_weight lifts_lifts |
@@ -702,36 +550,56 @@
|
ranged equivalence for local environments |
lreq ( ? â¡[?] ? ) |
- lreq_length lreq_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 |
-
+ |
|
- generic entrywise extension |
- lexs ( ? ⦻*[?,?,?] ? ) |
- lexs_length lexs_lexs |
-
+ | same top term structure |
+ tsts ( ? â ? ) |
+ tsts_tsts tsts_vector |
+
+
+
|
-
+ | closures |
+ cl_weight ( â¯{?,?,?} ) |
+
|
- grammar |
- append for local environments |
- append ( ? @@ ? ) |
- append_length |
-
+ |
+
+ |
+
|
+ cl_restricted_weight ( â¯{?,?} ) |
|
@@ -740,12 +608,18 @@
|
- context-sensitive equivalences for terms |
- ceq |
- ceq_ceq |
-
+ | global environments |
+ genv |
+
+
+ |
+
+
+
|
+ local environments |
+ lenv_length ( |?| ) |
|
@@ -754,12 +628,10 @@
|
- same top term structure |
- tsts ( ? â ? ) |
- tsts_tsts tsts_vector |
-
+ |
|
+ lenv_weight ( â¯{?} ) |
|
@@ -768,12 +640,10 @@
|
- closures |
- cl_weight ( â¯{?,?,?} ) |
- cl_restricted_weight ( â¯{?,?} ) |
-
+ |
|
+ lenv |
|
@@ -782,14 +652,20 @@
|
- internal syntax |
- genv |
-
+ | terms |
+ term_vector ( �.? ) |
+
|
-
+ |
+
+
|
+
+
+ |
+ term_simple ( ðâ¦?⦠) |
|
@@ -801,9 +677,7 @@
|
- lenv |
- lenv_weight ( â¯{?} ) |
- lenv_length ( |?| ) |
+ term_weight ( â¯{?} ) |
|
@@ -816,40 +690,50 @@
term |
- term_weight ( â¯{?} ) |
- term_simple ( ðâ¦?⦠) |
- term_vector ( �.? ) |
+
+
+ |
|
-
+ | items |
+ item_sd |
+
|
- item |
-
+ |
+
+
|
-
+ |
|
+ item_sh |
|
-
+ |
|
- external syntax |
- aarity |
-
+ |
|
-
+ | item |
+
|
+
+
+
+
+ |
+ atomic arities |
+ aarity |
|
@@ -883,6 +767,6 @@
- Last update: Sat, 21 Jan 2017 15:35:26 +0100
+ Last update: Sun, 22 Jan 2017 20:42:51 +0100