X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=9fc459b3337e1abf5ce98f6255d408d8383de3eb;hb=7e80b8d7a4b2c38729512dee28b3e0ecf9595c2a;hp=ee8bd0394eee6f167c0adce81cab804014f6819b;hpb=3bd1c05c93a76bb696aa93a2c8a104cad4dfc475;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index ee8bd0394..9fc459b33 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -16,12 +16,12 @@
- [lambdadelta home] + [\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
- [Spacer] + [Spacer]

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)
-
Summary of the Specification [spacer] +
Summary of the Specification [spacer]
Here is a numerical account of the specification's contents and its timeline. @@ -132,33 +132,39 @@ sizes files - 68 + 86 characters - 83858 + 109249 nodes - 168408 + 217872 propositions theorems - 14 + 30 lemmas - 388 + 506 total - 402 + 536 concepts declared - 42 + 59 defined - 44 + 55 total - 86 + 114
+ -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [spacer]
This table reports the specification's components and their planes.
@@ -227,19 +233,126 @@
+ +
+ + +
+ + +
+ + +
+ + +
+
- natural numbers with infinity + generic rt-transition counter + + rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 ) + rtc_shift ( ↓? ) + rtc_plus ( ? + ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + multiple relocation - ynat ( ∞ ) - ynat_pred ( ⫰? ) - ynat_succ ( ⫯? ) - ynat_le ( ? ≤ ? ) - ynat_lt ( ? < ? ) - ynat_plus ( ? + ? ) + rtmap + rtmap_eq ( ? ≗ ? ) + rtmap_tl ( ⫱? ) + rtmap_tls ( ⫱*[?]? ) + rtmap_isid ( 𝐈⦃?⦄ ) + rtmap_id + rtmap_fcla ( 𝐂⦃?⦄ ≡ ? ) + rtmap_isfin ( 𝐅⦃?⦄ ) + rtmap_isuni ( 𝐔⦃?⦄ ) + rtmap_uni ( 𝐔❴?❵ ) + rtmap_sle ( ? ⊆ ? ) + rtmap_sand ( ? ⋒ ? ≡ ? ) + rtmap_sor ( ? ⋓ ? ≡ ? ) + rtmap_at ( @⦃?,?⦄ ≡ ? ) + rtmap_istot ( 𝐓⦃?⦄ ) + rtmap_after ( ? ⊚ ? ≡ ? ) + + + +
+ + +
+ + nstream ( ↑? ) ( ⫯? ) + nstream_eq + + + nstream_isid + nstream_id ( 𝐈𝐝 ) + + + + + + nstream_sand + + + nstream_istot ( ?@❴?❵ ) + nstream_after ( ? ∘ ? ) + + + +
+ + +
+ + mr2 + mr2_at ( @⦃?,?⦄ ≡ ? ) + mr2_plus ( ? + ? ) + mr2_minus ( ? ▭ ? ≡ ? )
@@ -252,55 +365,49 @@
- +
- - - multiple relocation - - rtmap - rtmap_eq ( ? ≗ ? ) - rtmap_tl ( ↓? ) - rtmap_minus ( ? - ? ) - rtmap_isid ( 𝐈⦃?⦄ ) - rtmap_id - rtmap_sle ( ? ⊆ ? ) - rtmap_sand ( ? ⋒ ? ≡ ? ) - rtmap_at ( @⦃?,?⦄ ≡ ? ) - rtmap_istot ( 𝐓⦃?⦄ ) - rtmap_after ( ? ⊚ ? ≡ ? ) - - - + +
+ + +
+ + +
+ + +
+ +
- + +
+ +
- nstream ( ↑? ) ( ⫯? ) - nstream_eq - - - nstream_isid - nstream_id ( 𝐈𝐝 ) - - nstream_sand - - nstream_istot ( ?@❴?❵ ) - nstream_after ( ? ∘ ? ) - + natural numbers with infinity + + ynat ( ∞ ) + ynat_pred ( ⫰? ) + ynat_succ ( ⫯? ) + ynat_le ( ? ≤ ? ) + ynat_lt ( ? < ? ) + ynat_plus ( ? + ? ) +
- + +
+ +
- mr2 - mr2_at ( @⦃?,?⦄ ≡ ? ) - mr2_plus ( ? + ? ) - mr2_minus ( ? ▭ ? ≡ ? )
@@ -326,8 +433,19 @@ extensions to the library - stream ( ? @ ? ) ( ? ≐ ? ) - stream_hdtl + stream ( ? @ ? ) + stream_eq ( ? ≐ ? ) + stream_hdtl ( ↓? ) + stream_tls ( ↓*[?]? ) + +
+ + +
+ + +
+
@@ -389,6 +507,21 @@
+ +
+ + +
+ + +
+ + +
+ + +
+
@@ -401,7 +534,22 @@
bool ( Ⓕ ) ( Ⓣ ) - arith ( ?^? ) ( ⫯? ) ( ⫰? ) + arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) + +
+ + +
+ + +
+ + +
+ + +
+
@@ -463,6 +611,21 @@
+ +
+ + +
+ + +
+ + +
+ + +
+
@@ -496,6 +659,21 @@
+ +
+ + +
+ + +
+ + +
+ + +
+
@@ -533,6 +711,21 @@
+ +
+ + +
+ + +
+ + +
+ + +
+
@@ -541,7 +734,7 @@
- [Spacer] + [Spacer]

@@ -566,6 +759,6 @@

-
Last update: Fri, 04 Mar 2016 16:15:58 +0100
+
Last update: Thu, 19 May 2016 12:17:40 +0200