From: Ferruccio Guidi Date: Wed, 22 Nov 2017 21:21:13 +0000 (+0000) Subject: update in basic_2 and in the corresponding web page X-Git-Tag: make_still_working~400 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ff50a881cc8adf0aa2af7cfc0649bff35efc2f69 update in basic_2 and in the corresponding web page --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 154c5439e..9879ce6fd 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:28 +0100
+
Last update: Wed, 22 Nov 2017 22:20:04 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index c8f02f775..d9fe079cf 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -256,6 +256,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:29 +0100
+
Last update: Wed, 22 Nov 2017 22:20:05 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index a1c6dd6eb..55bf49ffb 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:28 +0100
+
Last update: Wed, 22 Nov 2017 22:20:04 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index ba7649484..f99504f88 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 291 + 301 characters - 304017 + 311322 nodes - 1426457 + 1450558 propositions theorems - 86 + 93 lemmas - 1024 + 1054 total - 1110 + 1147 concepts declared 34 defined - 84 + 91 total - 118 + 125 @@ -385,6 +385,7 @@ component + section plane files @@ -393,13 +394,15 @@ rt-conversion - context-sensitive r-conversion + context-sensitive parallel r-conversion + for terms cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? ) cpc_cpc rt-computation - uncounted context-sensitive rt-computation + uncounted context-sensitive parallel rt-computation + refinement for lenvs lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? ) lsubsx_lfsx lsubsx_lsubsx @@ -407,9 +410,10 @@
- +
+ strongly normalizing on referred entries for lenvs lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ ) lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx @@ -417,9 +421,10 @@
- +
+ strongly normalizing for term vectors csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_cnx_vector csx_csx_vector @@ -427,9 +432,10 @@
- +
+ strongly normalizing for terms csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx @@ -437,9 +443,10 @@
- +
+ on referred entries for lenvs lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs @@ -447,15 +454,17 @@
- +
+ 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 rt-transition - uncounted rst-transition + uncounted parallel rst-transition + for closures fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) fpbq_aaa @@ -463,9 +472,10 @@
- +
+ proper for closures fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ ) fpb_lfdeq @@ -473,7 +483,8 @@
- t-bound context-sensitive rt-transition + context-sensitive parallel r-transition + for lenvs on referred entries lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr @@ -481,9 +492,10 @@
- +
+ for binders cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )
@@ -493,9 +505,10 @@
- +
+ for terms cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) cpr_drops @@ -503,9 +516,8 @@
- -
- + t-bound context-sensitive parallel rt-transition + for terms cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx @@ -513,7 +525,8 @@
- uncounted context-sensitive rt-transition + uncounted context-sensitive parallel rt-transition + normal form for terms cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) cnx_simple cnx_drops cnx_cnx @@ -521,9 +534,10 @@
- +
+ for lenvs on referred entries lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx @@ -531,9 +545,10 @@
- +
+ for binders cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )
@@ -543,9 +558,10 @@
- +
+ for terms cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs @@ -553,19 +569,22 @@
- counted context-sensitive rt-transition + counted context-sensitive parallel rt-transition + for terms cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) cpg_simple cpg_drops cpg_lsubr iterated static typing - iterated extension on referred entries + iterated extension on referred entries + tc_lfxs ( ? ⦻**[?,?] ? ) - tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs + tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs static typing - generic reducibility + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) lsubc_drops lsubc_lsubr lsubc_lsuba @@ -573,9 +592,10 @@
- +
+ gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) gcp_aaa @@ -583,9 +603,10 @@
- +
+ gcp
@@ -595,7 +616,8 @@
- atomic arity assignment + atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba @@ -603,9 +625,10 @@
- +
+ aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) aaa_drops aaa_fqus aaa_lfdeq aaa_aaa @@ -613,7 +636,8 @@
- degree-based equivalence on referred entries + degree-based equivalence on referred entries + ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ ) ffdeq_fqup ffdeq_ffdeq @@ -621,9 +645,10 @@
- +
+ lfdeq ( ? ≛[?,?,?] ? ) lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq @@ -631,7 +656,17 @@
- generic extension on referred entries + syntactic equivalence on referred entries + + lfeq ( ? ≡[?] ? ) + lfeq_fqup lfeq_lfeq + + + +
+ + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs @@ -639,7 +674,8 @@
- context-sensitive free variables + context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) lsubf_lsubr lsubf_frees lsubf_lsubf @@ -647,9 +683,10 @@
- +
+ frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) frees_drops frees_fqup frees_frees @@ -657,13 +694,15 @@
- restricted ref. for local env. + restricted ref. for local env. + 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 @@ -671,15 +710,17 @@
- +
+ fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) fqup_weight fqup_drops fqup_fqup s-transition - structural successor for closures + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) fquq_length fquq_weight @@ -687,15 +728,17 @@
- +
+ fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) fqu_length fqu_weight relocation - generic slicing for local environments + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )
@@ -705,17 +748,19 @@
- +
+ drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops + drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops
- generic relocation + generic relocation + lifts_bind ( ⬆*[?] ? ≡ ? ) lifts_weight_bind lifts_lifts_bind @@ -723,9 +768,10 @@
- +
+ lifts_vector ( ⬆*[?] ? ≡ ? ) lifts_lifts_vector @@ -733,9 +779,10 @@
- +
+ lifts ( ⬆*[?] ? ≡ ? ) lifts_simple lifts_weight lifts_tdeq lifts_lifts @@ -743,7 +790,8 @@
- ranged equivalence for local environments + ranged equivalence for local environments + lreq ( ? ≡[?] ? ) lreq_length lreq_lreq @@ -751,13 +799,28 @@
- generic entrywise extension + generic entrywise extension + + lex ( ? ⦻[?] ? ) + +
+ + + + +
+ + +
+ + lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs + lexs_tc lexs_length lexs_lexs syntax - append for local environments + append for local environments + append ( ? @@ ? ) append_length @@ -765,7 +828,8 @@
- head equivalence for terms + head equivalence for terms + theq ( ? ⩳[?,?] ? ) theq_simple theq_tdeq theq_theq theq_simple_vector @@ -773,7 +837,8 @@
- degree-based equivalence + degree-based equivalence + tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )
@@ -783,9 +848,10 @@
- +
+ tdeq ( ? ≛[?,?] ? ) tdeq_tdeq @@ -793,7 +859,8 @@
- closures + closures + cl_weight ( ♯{?,?,?} )
@@ -803,9 +870,10 @@
- +
+ cl_restricted_weight ( ♯{?,?} )
@@ -815,7 +883,8 @@
- global environments + global environments + genv
@@ -825,8 +894,20 @@
- local environments - lenv_ext2 + local environments + + ceq_ext + ceq_ext_ceq_ext + + + +
+ + +
+ + + cext2
@@ -835,9 +916,10 @@
- +
+ lenv_length ( |?| )
@@ -847,9 +929,10 @@
- +
+ lenv_weight ( ♯{?} )
@@ -859,9 +942,10 @@
- +
+ lenv
@@ -871,17 +955,19 @@
- binders for local environments + binders for local environments + ext2 - ext2_ext2 + ext2_tc ext2_ext2
- +
+ bind bind_weight @@ -889,7 +975,8 @@
- terms + terms + term_vector ( Ⓐ?.? )
@@ -899,9 +986,10 @@
- +
+ term_simple ( 𝐒⦃?⦄ )
@@ -911,9 +999,10 @@
- +
+ term_weight ( ♯{?} )
@@ -923,9 +1012,10 @@
- +
+ term
@@ -935,7 +1025,8 @@
- items + items + item_sd
@@ -945,9 +1036,10 @@
- +
+ item_sh
@@ -957,9 +1049,10 @@
- +
+ item
@@ -969,7 +1062,8 @@
- atomic arities + atomic arities + aarity
@@ -1004,6 +1098,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:30 +0100
+
Last update: Wed, 22 Nov 2017 22:20:05 +0100
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index bbb53240e..c8153ffba 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -7116,6 +7116,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:29 +0100
+
Last update: Wed, 22 Nov 2017 22:20:05 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index c2836a039..a65e208d7 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:27 +0100
+
Last update: Wed, 22 Nov 2017 22:20:02 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index a60a94bf4..782704e32 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:28 +0100
+
Last update: Wed, 22 Nov 2017 22:20:04 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 60cd43288..2b612538e 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -132,29 +132,29 @@ sizes files - 102 + 104 characters - 143239 + 145725 nodes - 332314 + 337704 propositions theorems 42 lemmas - 679 + 693 total - 721 + 735 concepts declared - 65 + 66 defined - 70 + 73 total - 135 + 139 @@ -260,6 +260,9 @@
+ +
+
@@ -314,6 +317,9 @@
+ +
+
@@ -335,6 +341,7 @@ rtmap_isuni ( 𝐔⦃?⦄ ) rtmap_uni ( 𝐔❴?❵ ) rtmap_sle ( ? ⊆ ? ) + rtmap_sdj ( ? ∥ ? ) rtmap_sand ( ? ⋒ ? ≡ ? ) rtmap_sor ( ? ⋓ ? ≡ ? ) rtmap_at ( @⦃?,?⦄ ≡ ? ) @@ -364,6 +371,7 @@ + nstream_sor nstream_istot ( ?@❴?❵ ) @@ -426,6 +434,9 @@
+ +
+
@@ -478,6 +489,9 @@
+ +
+
@@ -534,6 +548,9 @@
+ +
+
@@ -598,6 +615,9 @@
+ +
+
@@ -662,6 +682,9 @@
+ +
+
@@ -673,7 +696,7 @@
- relations + relations ( ? ⊆ ? ) star lstar @@ -724,6 +747,9 @@
+ +
+
@@ -784,6 +810,9 @@
+ +
+
@@ -848,6 +877,9 @@
+ +
+
@@ -881,6 +913,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:29 +0100
+
Last update: Wed, 22 Nov 2017 22:20:04 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index dacccaa55..4c3b99b8f 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -297,6 +297,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:27 +0100
+
Last update: Wed, 22 Nov 2017 22:20:02 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 0044990cd..90ffe5b81 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:27 +0100
+
Last update: Wed, 22 Nov 2017 22:20:03 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index bdb4df1b6..a994c1acc 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:26 +0100
+
Last update: Wed, 22 Nov 2017 22:20:02 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 96735b310..12e353526 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:28 +0100
+
Last update: Wed, 22 Nov 2017 22:20:03 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index be057fc75..5bf4c3c29 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Tue, 14 Nov 2017 16:10:28 +0100
+
Last update: Wed, 22 Nov 2017 22:20:03 +0100