X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e3a69b03a9227da834d3dc86be104bcb8dbdb824;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=f99504f88b5674c5d95394983e1809a7dfc28d23;hpb=ff50a881cc8adf0aa2af7cfc0649bff35efc2f69;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index f99504f88..e3a69b03a 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -124,7 +124,7 @@
| category |
- objects |
+ units |
|
@@ -143,30 +143,30 @@
| sizes |
- files |
- 301 |
- characters |
- 311322 |
- nodes |
- 1450558 |
+ characters (files) |
+ 315581 (309) |
+ nodes (objects) |
+ 1458870 (1431) |
+ intrinsic loss factor |
+ 4.6 |
| propositions |
theorems |
- 93 |
+ 92 |
lemmas |
- 1054 |
+ 1085 |
total |
- 1147 |
+ 1177 |
| concepts |
declared |
34 |
defined |
- 91 |
+ 93 |
total |
- 125 |
+ 127 |
@@ -413,7 +413,7 @@
|
- strongly normalizing on referred entries for lenvs |
+ strongly normalizing for lenvs on referred entries |
lfsx ( ? ⢠â¬*[?,?,?] ðâ¦?⦠) |
lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx |
@@ -446,9 +446,22 @@
|
- on referred entries for lenvs |
+ for lenvs on referred entries |
lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs |
+ lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs |
+
+
+
+
+ |
+
+
+ |
+ for lenvs on all entries |
+ lpxs ( â¦?,?⦠⢠â¬*[?] ? ) |
+
+
+ |
|
@@ -459,7 +472,7 @@
|
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 |
+ cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs |
| rt-transition |
@@ -541,6 +554,19 @@
lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx |
+
+
+
+ |
+
+
+ |
+ for lenvs on all entries |
+ lpx ( â¦?,?⦠⢠â¬[?] ? ) |
+
+
+ |
+
@@ -563,7 +589,7 @@
|
for terms |
cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs |
+ cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq |
|
@@ -576,15 +602,15 @@
|
| iterated static typing |
- iterated extension on referred entries |
- |
+ iterated generic extension of a context-sensitive relation |
+ for lenvs on referred entries |
tc_lfxs ( ? ⦻**[?,?] ? ) |
tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
| static typing |
generic reducibility |
- |
+ restricted refinement for lenvs |
lsubc ( ? ⢠? â«[?] ? ) |
lsubc_drops lsubc_lsubr lsubc_lsuba |
@@ -595,7 +621,7 @@
|
- |
+ candidates |
gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
gcp_aaa |
@@ -606,7 +632,7 @@
|
- |
+ computation properties |
gcp |
@@ -617,7 +643,7 @@
|
atomic arity assignment |
- |
+ restricted refinement for lenvs |
lsuba ( ? ⢠? â«â ? ) |
lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
@@ -628,7 +654,7 @@
|
- |
+ for terms |
aaa ( â¦?,?⦠⢠? â ? ) |
aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
@@ -636,8 +662,8 @@
|
- degree-based equivalence on referred entries |
- |
+ degree-based equivalence |
+ for closures on referred entries |
ffdeq ( â¦?,?,?⦠â[?,?] â¦?,?,?⦠) |
ffdeq_fqup ffdeq_ffdeq |
@@ -648,7 +674,7 @@
|
- |
+ for lenvs on referred entries |
lfdeq ( ? â[?,?,?] ? ) |
lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
@@ -656,8 +682,8 @@
|
- syntactic equivalence on referred entries |
- |
+ syntactic equivalence |
+ for lenvs on referred entries |
lfeq ( ? â¡[?] ? ) |
lfeq_fqup lfeq_lfeq |
@@ -665,8 +691,8 @@
|
- generic extension on referred entries |
- |
+ generic extension of a context-sensitive relation |
+ for lenvs on referred entries |
lfxs ( ? ⦻*[?,?] ? ) |
lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
@@ -675,7 +701,7 @@
context-sensitive free variables |
- |
+ restricted refinement for lenvs |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
lsubf_lsubr lsubf_frees lsubf_lsubf |
@@ -686,7 +712,7 @@
|
- |
+ for terms |
frees ( ? ⢠ð
*�⦠⡠? ) |
frees_drops frees_fqup frees_frees |
@@ -694,15 +720,15 @@
|
- restricted ref. for local env. |
- |
+ local environments |
+ restricted refinement |
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 |
@@ -713,14 +739,14 @@
|
- |
+ proper for closures |
fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
fqup_weight fqup_drops fqup_fqup |
| s-transition |
- structural successor for closures |
- |
+ structural successor |
+ for closures |
fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_length fquq_weight |
@@ -731,36 +757,23 @@
|
- |
+ proper for closures |
fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
fqu_length fqu_weight |
| relocation |
- generic slicing for local environments |
- |
- drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
-
-
- |
-
-
-
-
- |
-
-
- |
- |
+ generic slicing |
+ for lenvs |
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops |
+ drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector |
|
generic relocation |
- |
+ for binders |
lifts_bind ( â¬*[?] ? â¡ ? ) |
lifts_weight_bind lifts_lifts_bind |
@@ -771,7 +784,7 @@
|
- |
+ for term vectors |
lifts_vector ( â¬*[?] ? â¡ ? ) |
lifts_lifts_vector |
@@ -782,7 +795,7 @@
|
- |
+ for terms |
lifts ( â¬*[?] ? â¡ ? ) |
lifts_simple lifts_weight lifts_tdeq lifts_lifts |
@@ -790,8 +803,8 @@
|
- ranged equivalence for local environments |
- |
+ syntactic equivalence |
+ for lenvs on selected entries |
lreq ( ? â¡[?] ? ) |
lreq_length lreq_lreq |
@@ -800,11 +813,9 @@
generic entrywise extension |
- |
+ for lenvs of one contex-sensitive relation |
lex ( ? ⦻[?] ? ) |
-
-
- |
+ lex_tc |
|
@@ -813,7 +824,7 @@
|
|
- |
+ for lenvs of two contex-sensitive relations |
lexs ( ? ⦻*[?,?,?] ? ) |
lexs_tc lexs_length lexs_lexs |
@@ -1098,6 +1109,6 @@
- Last update: Wed, 22 Nov 2017 22:20:05 +0100
+ Last update: Fri, 24 Nov 2017 21:00:01 +0100