X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=235681848e1017ce2553cd0f71bbae0cb7285fdc;hb=614542345e3e9c88722fdbc32c24a14b9a6c71d1;hp=d1900219605788c8fa756c027926ef9c4c29b654;hpb=f82a900182012664dd58eb1d8ab012c2a6f541ab;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d19002196..235681848 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 167 + 157 characters - 167321 + 138411 nodes - 875248 + 711276 propositions theorems - 47 + 45 lemmas - 590 + 506 total - 637 + 551 concepts declared 23 defined - 40 + 38 total - 63 + 61 @@ -494,9 +494,9 @@
- restricted ref. for local env. - lsubr ( ? ⫃ ? ) - lsubr_length lsubr_drops lsubr_lsubr + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq
@@ -508,9 +508,9 @@
- 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
@@ -522,9 +522,9 @@
- 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
@@ -536,9 +536,9 @@
- generic extension on referred entries - lfxs ( ? ⦻*[?,?] ? ) - lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + restricted ref. for context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees
@@ -560,6 +560,20 @@
+ + +
+ + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + +
+ + +
+ + s-computation iterated structural successor for closures @@ -863,6 +877,6 @@

-
Last update: Thu, 22 Sep 2016 15:52:43 +0200
+
Last update: Mon, 16 Jan 2017 12:25:24 +0100