X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2944f7afec83185cc41f0d2a4a5ef7392ff5d4b4;hb=5e5f9111df82a2f84f2b560ab59392cf0e0906c0;hp=c0b48965fffb3bf3f2275c74f0cd6cd83e5d1726;hpb=a145b5df4a86b3d5f8516a9c1cb76a62f6327151;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c0b48965f..2944f7afe 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -114,7 +114,7 @@ **** Sort level k in terms only. --> -
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -144,29 +144,29 @@ sizes files - 138 + 238 characters - 109280 + 249398 nodes - 546141 + 1213337 propositions theorems - 45 + 63 lemmas - 395 + 838 total - 440 + 901 concepts declared - 23 + 30 defined - 32 + 70 total - 55 + 100 @@ -180,11 +180,36 @@
Stage "A2": "Extending the Applicability Condition"
+ + + + @@ -314,7 +339,7 @@ -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -346,120 +371,158 @@ component plane files - +
- + + + rt-computation + uncounted context-sensitive rt-computation + csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_cnx_vector csx_csx_vector + + +
- +
+ csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_simple csx_simple_theq csx_drops csx_lsubr csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_csx - rt-transition - counted context-sensitive rt-transition - cpg ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpg_simple cpg_drops cpg_lsubr - +
- +
+ lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) + lfpxs_length lfpxs_fqup lfpxs_cpxs - static typing - parameters - sh - sd - +
- +
+ cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs - + rt-transition + parallel rst-transition + fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) + fpbq_aaa + + +
- restricted ref. for atomic arity assignment - lsuba ( ? ⊢ ? ⫃⁝ ? ) - lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba - +
- + fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpb_lfdeq + + +
+ t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr - +
- atomic arity assignment - aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_drops aaa_fqus aaa_lfeq aaa_aaa - +
- + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops + + + +
+ +
+ cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx - +
- restricted ref. for local env. - lsubr ( ? ⫃ ? ) - lsubr_length lsubr_drops lsubr_lsubr - + uncounted context-sensitive rt-transition + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops cnx_cnx + + +
- +
+ lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx - +
- equivalence for closures on referred entries - ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - ffeq_freq - +
- + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs + + +
+ counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr - + iterated static typing + iterated extension on referred entries + tc_lfxs ( ? ⦻**[?,?] ? ) +
- equivalence for local environments on referred entries - lfeq ( ? ≡[?] ? ) - lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq - + + + static typing + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drops lsubc_lsubr lsubc_lsuba + + +
- +
+ gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa
- generic extension on referred entries - lfxs ( ? ⦻*[?,?] ? ) - lfxs_length lfxs_fqup lfxs_lfxs - +
+ gcp
@@ -468,55 +531,93 @@
- context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - + atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + + +
- +
+ aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa - s-computation - iterated structural successor for closures - fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) - fqus_weight fqus_drops fqus_fqup fqus_fqus - +
- + degree-based equivalence on referred entries + ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) + ffdeq_fqup ffdeq_ffdeq + + +
+ +
+ + lfdeq ( ? ≡[?,?,?] ? ) + lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq - +
- + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + + +
- fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) - fqup_weight fqup_drops fqup_fqup - + context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees + + +
- +
+ frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_drops frees_fqup frees_frees - s-transition - structural successor for closures - fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) - fquq_length fquq_weight - +
- + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + + + s-computation + iterated structural successor for closures + fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) + fqus_weight fqus_drops fqus_fqup fqus_fqus + + + +
+ +
+ fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) + fqup_weight fqup_drops fqup_fqup + + + s-transition + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight @@ -526,24 +627,12 @@
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - fqu_length fqu_weight - -
- - -
- + fqu_length fqu_weight relocation generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - -
- - -
- + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )
@@ -555,14 +644,8 @@
- drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops - -
- - -
- + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops @@ -570,13 +653,7 @@ generic relocation for terms lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lifts_vector - -
- - -
- + lifts_lifts_vector @@ -586,13 +663,7 @@
lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts - -
- - -
- + lifts_simple lifts_weight lifts_tdeq lifts_lifts @@ -600,36 +671,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 + + +
+ head equivalence for terms + theq ( ? ⩳[?,?] ? ) + theq_simple theq_tdeq theq_theq theq_simple_vector - +
- generic entrywise extension - lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs - + degree-based equivalence for terms + deq ( ? ≡[?,?] ? ) + deq_deq + + +
- + closures + cl_weight ( ♯{?,?,?} ) +
- grammar - append for local environments - append ( ? @@ ? ) - append_length - +
+ +
+ + cl_restricted_weight ( ♯{?,?} )
@@ -638,12 +729,18 @@
- context-sensitive equivalences for terms - ceq - ceq_ceq - + global environments + genv +
+ + + +
+ + local environments + lenv_length ( |?| )
@@ -652,12 +749,10 @@
- same top term structure - tsts ( ? ≂ ? ) - tsts_tsts tsts_vector - +
+ lenv_weight ( ♯{?} )
@@ -666,12 +761,10 @@
- closures - cl_weight ( ♯{?,?,?} ) - cl_restricted_weight ( ♯{?,?} ) - +
+ lenv
@@ -680,14 +773,20 @@
- internal syntax - genv - + terms + term_vector ( Ⓐ?.? ) +
- + + +
+ +
+ + term_simple ( 𝐒⦃?⦄ )
@@ -699,9 +798,7 @@
- lenv - lenv_weight ( ♯{?} ) - lenv_length ( |?| ) + term_weight ( ♯{?} )
@@ -714,40 +811,50 @@
term - term_weight ( ♯{?} ) - term_simple ( 𝐒⦃?⦄ ) - term_vector ( Ⓐ?.? ) + +
+
- + items + item_sd +
- item - + + +
- +
+ item_sh
- +
- external syntax - aarity - +
- + item +
+ + + +
+ + atomic arities + aarity
@@ -781,6 +888,6 @@

-
Last update: Thu, 19 May 2016 12:17:40 +0200
+
Last update: Sat, 01 Apr 2017 16:50:39 +0200