From ab8006e4e28764820462d5963b0e87c210376ccd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 6 Mar 2017 22:23:40 +0000 Subject: [PATCH] update in basic_2 and apps_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 38 ++++--- helm/www/lambdadelta/basic_1.html | 2 +- helm/www/lambdadelta/basic_2.html | 126 ++++++++++++++--------- helm/www/lambdadelta/core.html | 2 +- helm/www/lambdadelta/documentation.html | 2 +- helm/www/lambdadelta/ground_1.html | 2 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/home.html | 2 +- helm/www/lambdadelta/implementation.html | 2 +- helm/www/lambdadelta/news.html | 2 +- helm/www/lambdadelta/osn.html | 2 +- helm/www/lambdadelta/specification.html | 2 +- 13 files changed, 112 insertions(+), 74 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index f2b625761..5fadd3479 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:43 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 8c3fad8d7..833ac4194 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -154,27 +154,27 @@ files 1 characters - 217 + 377 nodes - 0 + 779 propositions theorems - 0 + 2 lemmas - 0 + 1 total - 0 + 3 concepts declared 0 defined - 0 + 3 total - 0 + 3 @@ -214,17 +214,25 @@ - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) + functional + reduction and type machine + rtm + rtm_step ( ? ⇨ ? ) - + +
+ + relocation + lift ( ↑[?,?] ? ) +
- relocation - lift ( ↑[?,?] ? ) + + + examples + terms with special features + ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
@@ -258,6 +266,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:44 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 832e067ad..4fbd0a621 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:43 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d5b7548b3..e65261bbb 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 225 + 210 characters - 220639 + 220382 nodes - 1075226 + 1078173 propositions theorems 61 lemmas - 714 + 728 total - 775 + 789 concepts declared 29 defined - 63 + 66 total - 92 + 95 @@ -369,92 +369,122 @@ - rt-computation - uncounted context-sensitive rt-transition - csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) - csx_cnx csx_cpxs csx_csx + rt-computation + uncounted context-sensitive rt-transition + csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + +
+ - +
- +
- cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) - cpxs_tdeq cpxs_cpxs + csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_cnx csx_cpxs csx_csx - rt-transition - parallel qrst-transition - fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) - + +
+ +
+ lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) + lfpxs_length lfpxs_fqup - + +
+ +
- t-bound context-sensitive rt-transition - lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr + cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + cpxs_tdeq cpxs_cpxs - + rt-transition + parallel qrst-transition + fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) +
- + + +
- cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) - cpr_drops + t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr - +
- +
- cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops - +
- uncounted context-sensitive rt-transition - cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) - cnx_simple cnx_drops + +
+ + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx - +
- + uncounted context-sensitive rt-transition + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops + + + +
+ +
- lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) - lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa - + +
+ +
- + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs + + +
- cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) - cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr - + iterated static typing + generic extension on referred entries + lfxss ( ? ⦻**[?,?] ? ) +
- counted context-sensitive rt-transition - cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) - cpg_simple cpg_drops cpg_lsubr static typing @@ -845,6 +875,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:45 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index 03278d614..36bd2a675 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -7116,6 +7116,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:44 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 95387eecc..f51a73d9c 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -401,6 +401,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:42 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index f7a9db8ad..b6383c254 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:43 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 56fb90473..e63a6fd4b 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -819,6 +819,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:44 +0100
+
Last update: Mon, 06 Mar 2017 23:23:03 +0100
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index bf6d9cd50..579c245dc 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -290,6 +290,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:41 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index a7c573459..73f15d1e8 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:42 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 77f249673..1d82fca1e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:41 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index c3e33db5d..ef9bd6b70 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -197,6 +197,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:42 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 985c7341a..65855b2b7 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Sun, 05 Mar 2017 18:09:43 +0100
+
Last update: Mon, 06 Mar 2017 23:23:02 +0100
-- 2.39.2