From: Ferruccio Guidi Date: Fri, 24 Nov 2017 20:00:25 +0000 (+0000) Subject: update in basic_2 X-Git-Tag: make_still_working~397 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f6fd7c37170e17fa29ee835cdff3922ac11be398 update in basic_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 9879ce6fd..d19919f15 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:04 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index d9fe079cf..eb3ac6cda 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -138,7 +138,7 @@ category - objects + units
@@ -157,12 +157,12 @@ sizes - files - 2 - characters - 594 - nodes - 779 + characters (files) + 377 (1) + nodes (objects) + 779 (6) + intrinsic loss factor + 2.1 propositions @@ -256,6 +256,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:05 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 55bf49ffb..b6f6ce3b2 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:04 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
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
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index c8153ffba..f0ff46f51 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -7116,6 +7116,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:05 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index a65e208d7..f77e224f3 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:02 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 782704e32..ccc5ff801 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:04 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 2b612538e..4fb7ca304 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -112,7 +112,7 @@ category - objects + units
@@ -131,12 +131,12 @@ sizes - files - 104 - characters - 145725 - nodes - 337704 + characters (files) + 145725 (104) + nodes (objects) + 337452 (911) + intrinsic loss factor + 2.3 propositions @@ -913,6 +913,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:04 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index 4c3b99b8f..59aae3134 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -297,6 +297,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:02 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 90ffe5b81..02abad18e 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:03 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index a994c1acc..31665034e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:02 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 12e353526..8348a7506 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:03 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 5bf4c3c29..b86e965c0 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Wed, 22 Nov 2017 22:20:03 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100