X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=1da837bc4bb5bd273c3af997571ea0dfc54e1e81;hb=5606bd084cbbf6c187b21ee5f523fa3b313bb9de;hp=5f68c09358f965d15084c16787fe843385c94759;hpb=b1c1894b6ee9a48c3b0bacd09be00938d8e20341;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5f68c0935..1da837bc4 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 - 143 + 229 characters - 116151 + 240969 nodes - 604153 + 1182308 propositions theorems - 45 + 61 lemmas - 428 + 805 total - 473 + 866 concepts declared - 23 + 30 defined - 33 + 66 total - 56 + 96 @@ -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,106 +371,160 @@ component plane files - +
- + + + rt-computation + uncounted context-sensitive rt-computation + csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) +
- + + + +
+ +
+ csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_cnx csx_cpxs csx_csx - rt-transition - uncounted context-sensitive rt-transition - cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) - cpx_simple cpx_drops cpx_lsubr - +
- +
+ lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) + lfpxs_length lfpxs_fqup lfpxs_cpxs - +
- counted context-sensitive rt-transition - cpg ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpg_simple cpg_drops cpg_lsubr - +
- + cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + cpxs_tdeq cpxs_tsts cpxs_tsts_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs + + + rt-transition + parallel rst-transition + fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) + fpbq_aaa + + +
+ +
+ + fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpb_lfdeq - static typing - parameters - sh - sd - +
- + t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr + + +
+ +
+ + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops - +
- restricted ref. for atomic arity assignment - lsuba ( ? ⊢ ? ⫃⁝ ? ) - lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba - +
- + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx + + +
+ uncounted context-sensitive rt-transition + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops cnx_cnx - +
- atomic arity assignment - aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_drops aaa_fqus aaa_lfeq aaa_aaa - +
- + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx + + +
+ +
+ + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs - +
- restricted ref. for local env. - lsubr ( ? ⫃ ? ) - lsubr_length lsubr_drops lsubr_lsubr - + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr + + + iterated static typing + iterated extension on referred entries + tc_lfxs ( ? ⦻**[?,?] ? ) +
- + + + static typing + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drops lsubc_lsubr lsubc_lsuba + + + +
+ +
+ gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa
- equivalence for closures on referred entries - ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - ffeq_freq - +
+ gcp
@@ -454,55 +533,77 @@
- equivalence for local environments on referred entries - lfeq ( ? ≡[?] ? ) - lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq - + atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + + +
- +
+ aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
- generic extension on referred entries - lfxs ( ? ⦻*[?,?] ? ) - lfxs_length lfxs_fqup lfxs_lfxs - + 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
context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees + + +
- +
+ frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_drops frees_fqup frees_frees + + + +
+ + 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 - -
- - -
- + fqus_weight fqus_drops fqus_fqup fqus_fqus @@ -512,25 +613,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 @@ -540,24 +629,12 @@
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - fqu_length fqu_weight - -
- - -
- + fqu_length fqu_weight relocation generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - -
- - -
- + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )
@@ -569,14 +646,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 @@ -584,13 +655,7 @@ generic relocation for terms lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lifts_vector - -
- - -
- + lifts_lifts_vector @@ -600,13 +665,7 @@
lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts - -
- - -
- + lifts_simple lifts_weight lifts_tdeq lifts_lifts @@ -614,36 +673,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 + + +
+ same top term structure + tsts ( ? ⩳[?,?] ? ) + tsts_simple tsts_tdeq tsts_tsts tsts_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 ( ♯{?,?} )
@@ -652,12 +731,18 @@
- context-sensitive equivalences for terms - ceq - ceq_ceq - + global environments + genv + +
+ + + +
+ local environments + lenv_length ( |?| )
@@ -666,12 +751,10 @@
- same top term structure - tsts ( ? ≂ ? ) - tsts_tsts tsts_vector - +
+ lenv_weight ( ♯{?} )
@@ -680,12 +763,10 @@
- closures - cl_weight ( ♯{?,?,?} ) - cl_restricted_weight ( ♯{?,?} ) - +
+ lenv
@@ -694,14 +775,20 @@
- internal syntax - genv - + terms + term_vector ( Ⓐ?.? ) + +
+ + + +
- +
+ term_simple ( 𝐒⦃?⦄ )
@@ -713,9 +800,7 @@
- lenv - lenv_weight ( ♯{?} ) - lenv_length ( |?| ) + term_weight ( ♯{?} )
@@ -728,40 +813,50 @@
term - term_weight ( ♯{?} ) - term_simple ( 𝐒⦃?⦄ ) - term_vector ( Ⓐ?.? ) + +
+
- + items + item_sd +
- item - + + +
- +
+ item_sh
- +
- external syntax - aarity - +
- + item +
+ + + +
+ + atomic arities + aarity
@@ -795,6 +890,6 @@

-
Last update: Sat, 21 May 2016 22:22:39 +0200
+
Last update: Thu, 16 Mar 2017 20:59:31 +0100