From ebc95c29889f75f43a2ccc4dc2d1ca4e58c18629 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 14 Mar 2013 23:07:40 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 99 +++++++++++++------------------ 2 files changed, 42 insertions(+), 59 deletions(-) diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 0796ff3ad..bf977f717 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Mon, 11 Mar 2013 20:22:08 +0100
+
Last update: Fri, 15 Mar 2013 00:07:00 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 38fbd5bfd..5749edf06 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,29 +159,29 @@ sizes files - 254 + 256 characters - 485487 + 489336 nodes - 1296792 + 1309021 propositions theorems 85 lemmas - 1122 + 1125 total - 1207 + 1210 concepts declared 46 defined - 82 + 83 total - 128 + 129 @@ -288,9 +288,39 @@ dynamic typing + "big tree" parallel computation + yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) + yprs_yprs + ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) + ygt_ygt + +
+ + + + +
+ + "big tree" parallel reduction + ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) + ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) + +
+ + +
+ + +
+ + + + +
+ local env. ref. for stratified native validity lsubsv ( ? ⊢ ? ⊩:⊑[?] ? ) - lsubsv_ldrop lsubsv_ssta lsubsv_cpcs lsubsv_snv + lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv
@@ -471,26 +501,13 @@
- - -
- - "big tree" parallel computation - yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) - yprs_yprs - ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) - ygt_ygt - -
- -
decomposed extended computation dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) - dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs + dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs
@@ -684,23 +701,6 @@
- - -
- - "big tree" parallel reduction - ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) - ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) - -
- - -
- - -
- -
@@ -807,7 +807,7 @@ unwind iterated stratified static type assignment sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? ) - sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas + sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_sstas
@@ -820,23 +820,6 @@ static typing - local env. ref. for stratified static type assignment - lsubss ( ? •⊑[?] ? ) - lsubss_ldrop lsubss_ssta lsubss_lsubss - -
- - -
- - -
- - - - -
- stratified static type assignment ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta @@ -1371,6 +1354,6 @@

-
Last update: Mon, 11 Mar 2013 20:22:08 +0100
+
Last update: Fri, 15 Mar 2013 00:07:00 +0100
-- 2.39.2