X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e3a69b03a9227da834d3dc86be104bcb8dbdb824;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=09bf6182ce9bc449816f2fcf224db9cca87da8dc;hpb=e11ce46390f264e9010157dd36c0b9e71a58ba4b;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 09bf6182c..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 - 285 - characters - 293132 - nodes - 1383578 + characters (files) + 315581 (309) + nodes (objects) + 1458870 (1431) + intrinsic loss factor + 4.6 propositions theorems - 82 + 92 lemmas - 982 + 1085 total - 1064 + 1177 concepts declared - 33 + 34 defined - 82 + 93 total - 115 + 127 @@ -385,6 +385,7 @@ component + section plane files @@ -393,23 +394,37 @@ 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 + + + +
+ + +
+ + strongly normalizing for lenvs on referred entries lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ ) - lfsx_fqup lfsx_lfpxs lfsx_lfsx + lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx
- +
+ strongly normalizing for term vectors csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_cnx_vector csx_csx_vector @@ -417,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 @@ -427,25 +443,41 @@
- +
+ 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 ( ⦃?,?⦄ ⊢ ⬈*[?] ? ) + +
+ + + + +
+ + +
+ + 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 - uncounted rst-transition + uncounted parallel rst-transition + for closures fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) fpbq_aaa @@ -453,17 +485,19 @@
- +
- fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + proper for closures + fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ ) fpb_lfdeq
- 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 @@ -471,9 +505,10 @@
- +
+ for binders cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )
@@ -483,9 +518,10 @@
- +
+ for terms cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) cpr_drops @@ -493,9 +529,8 @@
- -
- + t-bound context-sensitive parallel rt-transition + for terms cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx @@ -503,7 +538,8 @@
- uncounted context-sensitive rt-transition + uncounted context-sensitive parallel rt-transition + normal form for terms cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) cnx_simple cnx_drops cnx_cnx @@ -511,9 +547,10 @@
- +
+ for lenvs on referred entries lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx @@ -521,9 +558,23 @@
- + +
+ + for lenvs on all entries + lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? ) +
+ + + +
+ + +
+ + for binders cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )
@@ -533,29 +584,33 @@
- +
+ 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
- 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 generic extension of a context-sensitive relation + for lenvs 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 + restricted refinement for lenvs lsubc ( ? ⊢ ? ⫃[?] ? ) lsubc_drops lsubc_lsubr lsubc_lsuba @@ -563,9 +618,10 @@
- +
+ candidates gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) gcp_aaa @@ -573,9 +629,10 @@
- +
+ computation properties gcp
@@ -585,7 +642,8 @@
- atomic arity assignment + atomic arity assignment + restricted refinement for lenvs lsuba ( ? ⊢ ? ⫃⁝ ? ) lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba @@ -593,9 +651,10 @@
- +
+ for terms aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) aaa_drops aaa_fqus aaa_lfdeq aaa_aaa @@ -603,25 +662,37 @@
- degree-based equivalence on referred entries - ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) + degree-based equivalence + for closures on referred entries + ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ ) ffdeq_fqup ffdeq_ffdeq
- +
- lfdeq ( ? ≡[?,?,?] ? ) + for lenvs on referred entries + lfdeq ( ? ≛[?,?,?] ? ) lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
- generic extension on referred entries + syntactic equivalence + for lenvs on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_fqup lfeq_lfeq + + + +
+ + generic extension of a context-sensitive relation + for lenvs on referred entries lfxs ( ? ⦻*[?,?] ? ) lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs @@ -629,7 +700,8 @@
- context-sensitive free variables + context-sensitive free variables + restricted refinement for lenvs lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) lsubf_lsubr lsubf_frees lsubf_lsubf @@ -637,9 +709,10 @@
- +
+ for terms frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) frees_drops frees_fqup frees_frees @@ -647,13 +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 @@ -661,15 +736,17 @@
- +
+ 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 @@ -677,35 +754,26 @@
- +
+ 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_ext2 drops_lexs drops_lreq drops_drops + drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector
- generic relocation + generic relocation + for binders lifts_bind ( ⬆*[?] ? ≡ ? ) lifts_weight_bind lifts_lifts_bind @@ -713,9 +781,10 @@
- +
+ for term vectors lifts_vector ( ⬆*[?] ? ≡ ? ) lifts_lifts_vector @@ -723,9 +792,10 @@
- +
+ for terms lifts ( ⬆*[?] ? ≡ ? ) lifts_simple lifts_weight lifts_tdeq lifts_lifts @@ -733,7 +803,8 @@
- ranged equivalence for local environments + syntactic equivalence + for lenvs on selected entries lreq ( ? ≡[?] ? ) lreq_length lreq_lreq @@ -741,13 +812,26 @@
- generic entrywise extension + generic entrywise extension + for lenvs of one contex-sensitive relation + lex ( ? ⦻[?] ? ) + lex_tc + + + +
+ + +
+ + for lenvs of two contex-sensitive relations lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs + lexs_tc lexs_length lexs_lexs syntax - append for local environments + append for local environments + append ( ? @@ ? ) append_length @@ -755,7 +839,8 @@
- head equivalence for terms + head equivalence for terms + theq ( ? ⩳[?,?] ? ) theq_simple theq_tdeq theq_theq theq_simple_vector @@ -763,8 +848,9 @@
- degree-based equivalence - tdeq_ext ( ? ≡[?,?] ? ) ( ? ⊢ ? ≡[?,?] ? ) + degree-based equivalence + + tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )
@@ -773,17 +859,19 @@
- +
- tdeq ( ? ≡[?,?] ? ) + + tdeq ( ? ≛[?,?] ? ) tdeq_tdeq
- closures + closures + cl_weight ( ♯{?,?,?} )
@@ -793,9 +881,10 @@
- +
+ cl_restricted_weight ( ♯{?,?} )
@@ -805,7 +894,8 @@
- global environments + global environments + genv
@@ -815,8 +905,20 @@
- local environments - lenv_ext2 + local environments + + ceq_ext + ceq_ext_ceq_ext + + + +
+ + +
+ + + cext2
@@ -825,9 +927,10 @@
- +
+ lenv_length ( |?| )
@@ -837,9 +940,10 @@
- +
+ lenv_weight ( ♯{?} )
@@ -849,9 +953,10 @@
- +
+ lenv
@@ -861,17 +966,19 @@
- binders for local environments + binders for local environments + ext2 - ext2_ext2 + ext2_tc ext2_ext2
- +
+ bind bind_weight @@ -879,7 +986,8 @@
- terms + terms + term_vector ( Ⓐ?.? )
@@ -889,9 +997,10 @@
- +
+ term_simple ( 𝐒⦃?⦄ )
@@ -901,9 +1010,10 @@
- +
+ term_weight ( ♯{?} )
@@ -913,9 +1023,10 @@
- +
+ term
@@ -925,7 +1036,8 @@
- items + items + item_sd
@@ -935,9 +1047,10 @@
- +
+ item_sh
@@ -947,9 +1060,10 @@
- +
+ item
@@ -959,7 +1073,8 @@
- atomic arities + atomic arities + aarity
@@ -994,6 +1109,6 @@

-
Last update: Fri, 03 Nov 2017 19:18:59 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100