X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=1e1fa23b9d2e5910e5074d4c68a50c525032755c;hb=282936907bd9b37d9de37f14e0e497db16f5d8b0;hp=f25040c2dd7094846adb33f7c1ee286d97510aff;hpb=286f7302d857a8a6674e1cf66fa1b1a1527dd1ac;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index f25040c2d..1e1fa23b9 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 - 107 + 150 characters - 68741 + 128505 nodes - 232342 + 646562 propositions theorems - 32 + 45 lemmas - 272 + 476 total - 304 + 521 concepts declared - 19 + 23 defined - 31 + 37 total - 50 + 60 @@ -180,6 +180,14 @@
Stage "A2": "Extending the Applicability Condition"
+ -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -348,6 +356,48 @@
+ + rt-transition + uncounted context-sensitive rt-transition + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup + +
+ + +
+ + + + +
+ + +
+ + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_lsubr + +
+ + +
+ + + + +
+ + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr + +
+ + +
+ + static typing parameters @@ -360,6 +410,34 @@
+ + +
+ + restricted ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + +
+ + +
+ + + + +
+ + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfeq aaa_aaa + +
+ + +
+ +
@@ -378,9 +456,37 @@
- ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq + +
+ + +
+ + + + +
+ + equivalence for local environments on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq + +
+ + +
+ + + + +
+ + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
@@ -394,7 +500,7 @@ context-sensitive free variables frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees + frees_weight frees_lreq frees_drops frees_frees
@@ -461,7 +567,7 @@ relocation generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )
@@ -479,7 +585,7 @@
- drops ( ⬇*[?,?] ? ≡ ? ) + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
@@ -536,7 +642,7 @@
- generic entrywise extension of context-sensitive relations for terma + generic entrywise extension lexs ( ? ⦻*[?,?,?] ? ) lexs_length lexs_lexs @@ -705,6 +811,6 @@

-
Last update: Fri, 08 Apr 2016 22:51:19 +0200
+
Last update: Fri, 22 Jul 2016 19:34:08 +0200