From 24ccb1f19b64d27f0f3c766e2b1503bd8e3b4786 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 May 2013 20:55:35 +0000 Subject: [PATCH] partial commit in basic_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 54 +++++++------------------------ 3 files changed, 14 insertions(+), 44 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 25acf49f8..f95a482db 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 05 May 2013 20:24:23 +0200
+
Last update: Thu, 09 May 2013 22:55:12 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 736d0367c..62e6d2148 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -199,6 +199,6 @@

-
Last update: Sun, 05 May 2013 20:24:24 +0200
+
Last update: Thu, 09 May 2013 22:55:12 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index df81e0374..727194157 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,20 +159,20 @@ sizes files - 195 + 187 characters - 365052 + 363451 nodes - 984918 + 982229 propositions theorems - 84 + 85 lemmas 781 total - 865 + 866 concepts @@ -448,39 +448,9 @@ computation - focalized computation - lfprs ( ⦃?⦄ ➡* ⦃?⦄ ) - lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs - -
- - -
- - - - -
- - -
- - fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ ) - fprs_aaa fprs_fprs - -
- - -
- - - - -
- decomposed extended computation dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) - dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs + dxprs_lift dxprs_lpss dxprs_aaa dxprs_dxprs
@@ -508,7 +478,7 @@ strongly normalizing computation csn_vector ( ? ⊢ ⬊* ? ) - csn_cpr_vector csn_tstc_vector csn_aaa + csn_tstc_vector csn_aaa
@@ -525,7 +495,7 @@ csn ( ? ⊢ ⬊* ? ) csn_alt ( ? ⊢ ⬊⬊* ? ) - csn_lift csn_cpr csn_lfpr + csn_lift csn_lpr
@@ -537,7 +507,7 @@ context-sensitive computation lprs ( ? ⊢ ➡* ? ) lprs_alt ( ? ⊢ ➡➡* ? ) - lprs_ldrop lprs_aaa lprs_cprs lprs_lprs + lprs_ldrop lprs_lpss lprs_aaa lprs_cprs lprs_lprs
@@ -550,7 +520,7 @@
cprs ( ? ⊢ ? ➡* ?) - cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_aaa cprs_lpr cprs_cprs cprs_tstc cprs_tstc_vector + cprs_tstc cprs_tstc_vector cprs_lift cprs_lpss cprs_aaa cprs_cprs
@@ -602,7 +572,7 @@ context-sensitive reduction lpr ( ? ⊢ ➡ ? ) - lpr_ldrop lpr_cpss lpr_lpss lpr_aaa lpr_cpr lpr_lpr + lpr_ldrop lpr_lpss lpr_aaa lpr_lpr
@@ -1094,6 +1064,6 @@

-
Last update: Sun, 05 May 2013 20:24:24 +0200
+
Last update: Thu, 09 May 2013 22:55:12 +0200
-- 2.39.2