From: Ferruccio Guidi Date: Tue, 31 May 2016 19:19:40 +0000 (+0000) Subject: - update in ground_2 and basic_2 X-Git-Tag: make_still_working~571 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=503426723b9fc786c69dc988d38726997ecb809a - update in ground_2 and basic_2 - updated documentation --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 9c0283b45..602ed2c57 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Sun, 22 May 2016 15:25:27 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 076412946..720fb0dee 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 95170e646..f6b288778 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Sun, 22 May 2016 15:25:27 +0200
+
Last update: Tue, 31 May 2016 21:18:48 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index cbfde33d8..5c8b09d63 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -144,29 +144,29 @@ sizes files - 143 + 150 characters - 116151 + 121855 nodes - 607262 + 618445 propositions theorems - 46 + 45 lemmas - 430 + 458 total - 476 + 503 concepts declared 23 defined - 33 + 34 total - 56 + 57 @@ -359,6 +359,22 @@ rt-transition uncounted context-sensitive rt-transition + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_fqup + +
+ + +
+ + + + +
+ + +
+ cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) cpx_simple cpx_drops cpx_lsubr @@ -484,7 +500,7 @@ context-sensitive free variables frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees + frees_weight frees_lreq frees_drops frees_frees
@@ -795,6 +811,6 @@

-
Last update: Sun, 22 May 2016 15:25:27 +0200
+
Last update: Tue, 31 May 2016 21:18:48 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index bca651cf1..0fedfb151 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -179,6 +179,18 @@
+ + + P2d. + + F. Guidi: Considerations on Automath in Light of the Grundlagen (2016-05). Presentation at University of Bologna (slides). + + + + +
+ + P2c. @@ -389,6 +401,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/download/ld_talk_9s.pdf b/helm/www/lambdadelta/download/ld_talk_9s.pdf new file mode 100644 index 000000000..3f7c2bee7 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_9s.pdf differ diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 5e9c1defa..bf75563e5 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Sun, 22 May 2016 15:25:27 +0200
+
Last update: Tue, 31 May 2016 21:18:48 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 4b32a65f6..fc266948a 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -132,29 +132,29 @@ sizes files - 86 + 90 characters - 109249 + 120841 nodes - 217872 + 247853 propositions theorems - 30 + 32 lemmas - 506 + 568 total - 536 + 600 concepts declared - 59 + 60 defined - 55 + 58 total - 114 + 118 @@ -248,6 +248,12 @@
+ +
+ + +
+
@@ -294,6 +300,12 @@
+ +
+ + +
+
@@ -303,6 +315,7 @@ rtmap rtmap_eq ( ? ≗ ? ) + rtmap_pushs ( ↑*[?]? ) rtmap_tl ( ⫱? ) rtmap_tls ( ⫱*[?]? ) rtmap_isid ( 𝐈⦃?⦄ ) @@ -316,7 +329,8 @@ rtmap_sor ( ? ⋓ ? ≡ ? ) rtmap_at ( @⦃?,?⦄ ≡ ? ) rtmap_istot ( 𝐓⦃?⦄ ) - rtmap_after ( ? ⊚ ? ≡ ? ) + rtmap_after ( ? ⊚ ? ≡ ? ) + rtmap_coafter ( ? ~⊚ ? ≡ ? ) @@ -329,6 +343,7 @@ nstream_eq + nstream_isid nstream_id ( 𝐈𝐝 ) @@ -340,7 +355,8 @@ nstream_istot ( ?@❴?❵ ) - nstream_after ( ? ∘ ? ) + nstream_after ( ? ∘ ? ) + @@ -386,6 +402,12 @@
+ +
+ + +
+
@@ -426,6 +448,12 @@
+ +
+ + +
+
@@ -470,6 +498,12 @@
+ +
+ + +
+
@@ -522,6 +556,12 @@
+ +
+ + +
+
@@ -574,6 +614,12 @@
+ +
+ + +
+
@@ -626,6 +672,12 @@
+ +
+ + +
+
@@ -674,6 +726,12 @@
+ +
+ + +
+
@@ -726,6 +784,12 @@
+ +
+ + +
+
@@ -759,6 +823,6 @@

-
Last update: Sun, 22 May 2016 15:25:27 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index c1593ebc3..6bf8c301f 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 36ac7c630..b3e330c9f 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -283,6 +283,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 6ea5beda9..6101558d2 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 4095590fb..ec0d85773 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Sun, 22 May 2016 15:25:26 +0200
+
Last update: Tue, 31 May 2016 21:18:47 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index c61d2b6a0..3e59b57e6 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -44,6 +44,14 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] + [ { name "ldP2d" "P2d." "" } { + "F. Guidi:" + + @@("download/ld_talk_9s.pdf" + "Considerations on Automath in Light of the Grundlagen") + + "(2016-05)." + + "Presentation at University of Bologna (slides)." + * } + ] [ { name "ldP2c" "P2c." "" } { "F. Guidi:" + @@("download/ld_talk_8s.pdf"