From 265f584ad05c29694376127e46aef45cc546d43c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 2 Dec 2013 19:23:46 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 58 +++++++++++++++++++----------- helm/www/lambdadelta/ground_2.html | 8 ++--- 4 files changed, 43 insertions(+), 27 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index f335f8978..b154d7526 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Mon, 25 Nov 2013 15:44:49 +0100
+
Last update: Mon, 02 Dec 2013 20:23:02 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index cebe05066..b764cb425 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Mon, 25 Nov 2013 15:44:48 +0100
+
Last update: Mon, 02 Dec 2013 20:23:02 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 2a5efeb99..213361156 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,29 +163,29 @@ sizes files - 293 + 298 characters - 441375 + 466817 nodes - 1286916 + 1359471 propositions theorems - 91 + 89 lemmas - 888 + 910 total - 979 + 999 concepts declared - 49 + 50 defined - 85 + 73 total - 134 + 123 @@ -293,7 +293,7 @@
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. - A notation file covering the whole specification is provided. + Notation files covering the whole specification are provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).
@@ -538,7 +538,7 @@
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) - cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs + cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
@@ -648,7 +648,7 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_aaa lpx_lpx + lpx_ldrop lpx_lleq lpx_aaa
@@ -664,7 +664,7 @@
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpx_lift cpx_cix cpx_cpx + cpx_lift cpx_lleq cpx_cix
@@ -898,7 +898,7 @@ iterated structural successor for closures fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) - fqus_alt fqus_fqus + fqus_alt fqus_lleq fqus_fqus
@@ -914,7 +914,7 @@
fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) - fqup_fqup + fqup_lleq fqup_fqup
@@ -981,7 +981,7 @@ structural successor for closures fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) - fquq_fquq + fquq_lleq
@@ -994,7 +994,7 @@
fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) - fqu_fqu + fqu_lleq
@@ -1007,8 +1007,8 @@
lazy equivalence for local environments - lleq ( ? ⋕[?] ? ) - lleq_fleq + lleq ( ? ⋕[?,?] ? ) + lleq_lleq
@@ -1036,7 +1036,7 @@ basic local env. slicing ldrop ( ⇩[?,?] ? ≡ ? ) - ldrop_append ldrop_lpx_sn ldrop_ldrop + ldrop_append ldrop_lpx_sn ldrop_leq ldrop_ldrop
@@ -1076,6 +1076,22 @@ grammar + equivalence for local environments + leq ( ? ≃[?,?] ? ) + +
+ + +
+ + +
+ + + + +
+ pointwise extension of a relation lpx_sn lpx_sn_tc lpx_sn_lpx_sn @@ -1222,6 +1238,6 @@

-
Last update: Mon, 25 Nov 2013 15:44:49 +0100
+
Last update: Mon, 02 Dec 2013 20:23:02 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 560175fa4..842528303 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,11 +56,11 @@ sizes files - 26 + 24 characters - 65234 + 65135 nodes - 44240 + 40661 propositions @@ -214,6 +214,6 @@

-
Last update: Sun, 01 Dec 2013 22:28:19 +0100
+
Last update: Mon, 02 Dec 2013 20:23:02 +0100
-- 2.39.2