From: Ferruccio Guidi Date: Sun, 22 Jan 2017 19:48:37 +0000 (+0000) Subject: update in basic_2 ... X-Git-Tag: make_still_working~514 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bba53a83579540bc3925d47d679e2aad22e85755 update in basic_2 ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 513db1fe9..0097a0f75 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index d3b26812c..71b03235c 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 549483fbe..b2b091d03 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
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
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 33432e4a8..4f8e8d475 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 944b674c2..517377c51 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index f1b34acf3..3d6459ecc 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -819,6 +819,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index e783eabc6..df7ae7b6a 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -290,6 +290,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 648cc31cf..8b59dced6 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index f91ab0380..fe85f24b8 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 57f8a9f95..90284c4a1 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:25 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 400a44814..3a88cfc67 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+
Last update: Sun, 22 Jan 2017 20:42:51 +0100