From 93f99278ea89f14e36f9b55aa3e14fada40345ea Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Mar 2014 18:38:22 +0000 Subject: [PATCH] update in ground_2 and basic_2 ... --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 94 +++++++++++------------------- helm/www/lambdadelta/ground_2.html | 12 ++-- 4 files changed, 41 insertions(+), 69 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 768246fd8..044df3ac0 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Tue, 04 Mar 2014 00:00:09 +0100
+
Last update: Tue, 11 Mar 2014 19:37:30 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 07fb2766f..8ff256800 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Tue, 04 Mar 2014 00:00:09 +0100
+
Last update: Tue, 11 Mar 2014 19:37:30 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 25de9f611..88c3e88eb 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,29 +163,29 @@ sizes files - 329 + 319 characters - 570962 + 529971 nodes - 1619084 + 1452933 propositions theorems - 108 + 96 lemmas - 1122 + 1068 total - 1230 + 1164 concepts declared - 52 + 49 defined - 76 + 77 total - 128 + 126 @@ -594,7 +594,7 @@
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) - cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs + cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
@@ -688,7 +688,7 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_cpys lpx_lleq lpx_aaa + lpx_ldrop lpx_lleq lpx_aaa
@@ -704,7 +704,7 @@
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpx_lift cpx_cpys cpx_lleq cpx_cix + cpx_leq cpx_lift cpx_lleq cpx_cix
@@ -936,33 +936,9 @@ substitution - lazy equivalence for local environments - lleq ( ? ⋕[?,?] ? ) - lleq_alt ( ? ⋕⋕[?,?] ? ) - lleq_ldrop lleq_fqus lleq_lleq lleq_ext - -
- - - - -
- - contxt-sensitive extended multiple substitution - cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) - cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) - cpys_lift cpys_cpys - -
- - - - -
- iterated structural successor for closures fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) - fqus_alt fqus_fqus + fqus_alt fqus_lleq fqus_fqus
@@ -978,7 +954,7 @@
fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) - fqup_fqup + fqup_lleq fqup_fqup
@@ -1042,12 +1018,10 @@ relocation - contxt-sensitive extended ordinary substitution - cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) - cpy_lift cpy_cpy - -
- + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) + fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + fquq_lleq
@@ -1056,9 +1030,11 @@
- local env. ref. for extended substitution - lsuby ( ? ⊑×[?,?] ? ) - lsuby_lsuby + +
+ + fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) + fqu_lleq
@@ -1070,9 +1046,9 @@
- structural successor for closures - fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) - fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + global env. slicing + gdrop ( ⇩[?] ? ≡ ? ) + gdrop_gdrop
@@ -1084,13 +1060,9 @@
- -
- - fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) - -
- + lazy equivalence for local environments + lleq ( ? ⋕[?,?] ? ) + lleq_leq lleq_ldrop lleq_lleq
@@ -1102,9 +1074,9 @@
- global env. slicing - gdrop ( ⇩[?] ? ≡ ? ) - gdrop_gdrop + lazy pointwise extension of a relation + llpx_sn + llpx_sn_leq llpx_sn_ldrop
@@ -1318,6 +1290,6 @@

-
Last update: Tue, 04 Mar 2014 00:00:09 +0100
+
Last update: Tue, 11 Mar 2014 19:37:30 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 10b1cdd58..24b659ee1 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,20 +56,20 @@ sizes files - 29 + 31 characters - 72188 + 72551 nodes - 57742 + 58038 propositions theorems 2 lemmas - 171 + 173 total - 173 + 175 concepts @@ -234,6 +234,6 @@

-
Last update: Tue, 04 Mar 2014 00:00:09 +0100
+
Last update: Tue, 11 Mar 2014 19:37:30 +0100
-- 2.39.2