From: Ferruccio Guidi Date: Fri, 1 Apr 2016 21:31:50 +0000 (+0000) Subject: update in ground_2 and basic_2 ... X-Git-Tag: make_still_working~616 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ecb63d645415784352a937f8320f84c23da327f7;p=helm.git update in ground_2 and basic_2 ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 8202086a4..7f46bd1ef 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:30 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 35fdff6e8..a0d1206ed 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 789062b5c..f4d023145 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:53 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 4003948a1..5ae7da306 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 83 + 102 characters - 55955 + 69295 nodes - 191279 + 245853 propositions theorems - 33 + 34 lemmas - 211 + 256 total - 244 + 290 concepts declared - 15 + 21 defined - 23 + 29 total - 38 + 50 @@ -343,40 +343,80 @@ - relocation - ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq - + static typing + parameters + sh + sd +
- +
- +
- context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr +
- +
- +
- generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - + ranged equivalence for closures + freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + freq_freq +
+ +
+ + + + +
+ + context-sensitive free variables + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_weight frees_lreq frees_frees + +
+ + +
+ + + + s-computation + + +
+ + +
+ + +
+ + +
+ + + + s-transition + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight
@@ -391,8 +431,8 @@
- drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight
@@ -401,72 +441,86 @@ - + relocation + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) +
- generic relocation for terms - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector - +
- +
- +
- +
- lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts - + drops ( ⬇*[?,?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops +
- +
- +
- ranged equivalence for local environments - lreq ( ? ≡[?] ? ) - lreq_length lreq_lreq - + generic relocation for terms + lifts_vector ( ⬆*[?] ? ≡ ? ) + lifts_lifts_vector +
- +
- +
- generic entrywise extension of context-sensitive relations for terma - lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs - +
- + lifts ( ⬆*[?] ? ≡ ? ) + lifts_simple lifts_weight lifts_lifts + +
+ +
- - - +
+ ranged equivalence for local environments + lreq ( ? ≡[?] ? ) + lreq_length lreq_lreq
+ +
+ + + + +
+ + generic entrywise extension of context-sensitive relations for terma + lexs ( ? ⦻*[?,?,?] ? ) + lexs_length lexs_lexs
@@ -476,6 +530,20 @@ grammar + append for local environments + append ( ? @@ ? ) + append_length + +
+ + +
+ + + + +
+ context-sensitive equivalences for terms ceq ceq_ceq @@ -540,7 +608,9 @@ lenv lenv_weight ( ♯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
+ @@ -617,6 +687,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:53 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index e00c7ab8e..29a1e83cb 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -389,6 +389,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index d3e660577..a29a85f85 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:53 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 598ae85dc..e66ca0d4b 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -132,29 +132,29 @@ sizes files - 77 + 79 characters - 93671 + 96249 nodes - 198031 + 206180 propositions theorems 23 lemmas - 472 + 495 total - 495 + 518 concepts declared 53 defined - 49 + 50 total - 102 + 103 @@ -239,6 +239,9 @@
+ +
+
@@ -276,6 +279,9 @@
+ +
+
@@ -292,6 +298,7 @@ rtmap_fcla ( 𝐂⦃?⦄ ≡ ? ) rtmap_isfin ( 𝐅⦃?⦄ ) rtmap_isuni ( 𝐔⦃?⦄ ) + rtmap_uni ( 𝐔❴?❵ ) rtmap_sle ( ? ⊆ ? ) rtmap_sand ( ? ⋒ ? ≡ ? ) rtmap_sor ( ? ⋓ ? ≡ ? ) @@ -316,6 +323,7 @@ + nstream_sand @@ -363,6 +371,9 @@
+ +
+
@@ -404,6 +415,9 @@
+ +
+
@@ -453,6 +467,9 @@
+ +
+
@@ -502,6 +519,9 @@
+ +
+
@@ -551,6 +571,9 @@
+ +
+
@@ -596,6 +619,9 @@
+ +
+
@@ -645,6 +671,9 @@
+ +
+
@@ -678,6 +707,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index c9551cd11..eda6bd935 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -291,6 +291,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 14c85248a..d14a8519b 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -276,6 +276,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 11a934d11..3971c904e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 1a8dae817..41de39477 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -382,6 +382,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Fri, 01 Apr 2016 23:30:52 +0200