From: Ferruccio Guidi Date: Sun, 19 Feb 2017 15:26:15 +0000 (+0000) Subject: update in basic_2 X-Git-Tag: make_still_working~503 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5712c83e9c25c8cf44812586c31ee823771e95e0 update in basic_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 1e48bd7da..0634519d0 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:38 +0100
+
Last update: Sun, 19 Feb 2017 16:24:36 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index a6435234d..580dfeb4a 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:39 +0100
+
Last update: Sun, 19 Feb 2017 16:24:37 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 1dc6f50a0..25b338a1f 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:38 +0100
+
Last update: Sun, 19 Feb 2017 16:24:36 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index f1ea20bbf..d3cb6f28e 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 214 + 221 characters - 202530 + 212361 nodes - 1010247 + 1046022 propositions theorems - 48 + 49 lemmas - 675 + 691 total - 723 + 740 concepts declared - 26 + 29 defined - 46 + 61 total - 72 + 90 @@ -358,6 +358,9 @@ component plane files + +
+
@@ -366,14 +369,42 @@ rt-computation uncounted context-sensitive rt-transition cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + +
+
+ + +
+ + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drop lsubc_drops lsubc_lsubr lsubc_lsuba + +
+ + + + +
+ + +
+ + gcp + gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa + rt-transition parallel qrst-rtransition fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + +
+
@@ -384,7 +415,10 @@ 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 + +
+ @@ -394,7 +428,10 @@
cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) - cpr_drops + cpr_drops + +
+ @@ -404,7 +441,10 @@
cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx + +
+ @@ -412,7 +452,10 @@ uncounted context-sensitive rt-transition cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) - cnx_simple cnx_drops + cnx_simple cnx_drops + +
+ @@ -422,7 +465,10 @@
lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) - lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa + +
+ @@ -432,7 +478,10 @@
cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) - cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq + +
+ @@ -440,13 +489,19 @@ counted context-sensitive rt-transition cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) - cpg_simple cpg_drops cpg_lsubr + cpg_simple cpg_drops cpg_lsubr + +
+ static typing atomic arity assignment lsuba ( ? ⊢ ? ⫃⁝ ? ) - lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + +
+ @@ -456,7 +511,10 @@
aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_drops aaa_fqus aaa_lfdeq aaa_aaa + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa + +
+ @@ -464,7 +522,10 @@ degree-based equivalence on referred entries ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) - ffdeq_fqup ffdeq_ffdeq + ffdeq_fqup ffdeq_ffdeq + +
+ @@ -474,7 +535,10 @@
lfdeq ( ? ≡[?,?,?] ? ) - lfdeq_length lfdeq_fqup lfdeq_lfdeq + lfdeq_length lfdeq_fqup lfdeq_lfdeq + +
+ @@ -482,7 +546,10 @@ generic extension on referred entries lfxs ( ? ⦻*[?,?] ? ) - lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + +
+ @@ -490,7 +557,10 @@ context-sensitive free variables lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) - lsubf_frees + lsubf_frees + +
+ @@ -500,7 +570,10 @@
frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_drops frees_fqup frees_frees + frees_weight frees_drops frees_fqup frees_frees + +
+ @@ -508,13 +581,19 @@ 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 + +
+ @@ -524,13 +603,19 @@
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 + +
+ @@ -540,12 +625,18 @@
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - fqu_length fqu_weight + fqu_length fqu_weight + +
+ relocation generic slicing for local environments drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + +
+
@@ -558,7 +649,10 @@
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 + +
+ @@ -566,7 +660,10 @@ generic relocation for terms lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lifts_vector + lifts_lifts_vector + +
+ @@ -576,7 +673,10 @@
lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_tdeq lifts_lifts + lifts_simple lifts_weight lifts_tdeq lifts_lifts + +
+ @@ -584,7 +684,10 @@ ranged equivalence for local environments lreq ( ? ≡[?] ? ) - lreq_length lreq_lreq + lreq_length lreq_lreq + +
+ @@ -592,13 +695,19 @@ generic entrywise extension lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs + lexs_length lexs_lexs + +
+ syntax append for local environments append ( ? @@ ? ) - append_length + append_length + +
+ @@ -606,7 +715,10 @@ degree-based equivalence for terms deq ( ? ≡[?,?] ? ) - deq_deq + deq_deq + +
+ @@ -614,7 +726,10 @@ same top term structure tsts ( ? ≂ ? ) - tsts_tsts tsts_vector + tsts_tsts tsts_vector + +
+ @@ -622,6 +737,9 @@ closures cl_weight ( ♯{?,?,?} ) + +
+
@@ -634,6 +752,9 @@
cl_restricted_weight ( ♯{?,?} ) + +
+
@@ -644,6 +765,9 @@ global environments genv + +
+
@@ -654,6 +778,9 @@ local environments lenv_length ( |?| ) + +
+
@@ -666,6 +793,9 @@
lenv_weight ( ♯{?} ) + +
+
@@ -678,6 +808,9 @@
lenv + +
+
@@ -688,6 +821,9 @@ terms term_vector ( Ⓐ?.? ) + +
+
@@ -700,6 +836,9 @@
term_simple ( 𝐒⦃?⦄ ) + +
+
@@ -712,6 +851,9 @@
term_weight ( ♯{?} ) + +
+
@@ -724,6 +866,9 @@
term + +
+
@@ -734,6 +879,9 @@ items item_sd + +
+
@@ -746,6 +894,9 @@
item_sh + +
+
@@ -758,6 +909,9 @@
item + +
+
@@ -768,6 +922,9 @@ atomic arities aarity + +
+
@@ -801,6 +958,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:40 +0100
+
Last update: Sun, 19 Feb 2017 16:24:37 +0100
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index 10cc0e438..943e8f3bf 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -7116,6 +7116,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:39 +0100
+
Last update: Sun, 19 Feb 2017 16:24:37 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index f711e521b..cfa5da464 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:36 +0100
+
Last update: Sun, 19 Feb 2017 16:24:34 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index b20e79223..262fa33a4 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:38 +0100
+
Last update: Sun, 19 Feb 2017 16:24:36 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index d90a18687..fc97ab85d 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -819,6 +819,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:39 +0100
+
Last update: Sun, 19 Feb 2017 16:24:37 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index 8312b1587..bcc7d8f5a 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -290,6 +290,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:36 +0100
+
Last update: Sun, 19 Feb 2017 16:24:34 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index da0010691..20c5d424a 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:37 +0100
+
Last update: Sun, 19 Feb 2017 16:24:35 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index d79757c9f..ed7d91490 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:36 +0100
+
Last update: Sun, 19 Feb 2017 16:24:34 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 0406ae14e..19f26c850 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:37 +0100
+
Last update: Sun, 19 Feb 2017 16:24:35 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index f0a1ea4f9..50e64b634 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Thu, 16 Feb 2017 12:23:37 +0100
+
Last update: Sun, 19 Feb 2017 16:24:35 +0100