X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=e66ca0d4bfa6f3d328e47411770ce5a5512bb167;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=94be6097921cb578b4aaee1beca22acf72f081c8;hpb=3080bf8226d155d017c5ec5c4e852d952f5b878c;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 94be60979..e66ca0d4b 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,29 +84,30 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - helena -
- -
Summary of the Specification [spacer] +
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
-
+
@@ -121,51 +132,68 @@ - + - + - + - + - + - + - + - + - +
sizes files3079 characters6858196249 nodes62380206180
propositions theorems223 lemmas187495 total189518
concepts declared4053 defined2550 total65103
-
    +
      +
    • + 2016 March 4. + Platform-independent multiple relocation (rtmap). +
      • +
    +
      +
    • + 2016 January 20. + Multiple relocation with streams of naturals. +
      • +
    +
      +
    • + 2015 October 11. + Multiple relocation with lists of booleans. +
      • +
    +
    • 2013 November 27. - Natural numbers with infinity. + Natural numbers with infinity (ynat).
    -
      +
      • 2011 August 10. Specification starts.
      - -
      Logical Structure of the Specification [spacer] +
      Logical Structure of the Specification [spacer]
      -
      This table reports the specification's components and their planes. +
      This table reports the specification's components and their planes.
      -
      +
      @@ -193,31 +221,398 @@ + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + + + + + + + + + + + + @@ -232,10 +627,35 @@ - + - + + + + + + + + + @@ -261,8 +681,7 @@

      		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      natural numbers with infinitynatural numbers with infinity + ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_plus ( ? + ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      multiple relocation + rtmaprtmap_eq ( ? ≗ ? )rtmap_tl ( ⫱? )rtmap_tls ( ⫱*[?]? )rtmap_isid ( 𝐈⦃?⦄ )rtmap_idrtmap_fcla ( 𝐂⦃?⦄ ≡ ? )rtmap_isfin ( 𝐅⦃?⦄ )rtmap_isuni ( 𝐔⦃?⦄ )rtmap_uni ( 𝐔❴?❵ )rtmap_sle ( ? ⊆ ? )rtmap_sand ( ? ⋒ ? ≡ ? )rtmap_sor ( ? ⋓ ? ≡ ? )rtmap_at ( @⦃?,?⦄ ≡ ? )rtmap_istot ( 𝐓⦃?⦄ )rtmap_after ( ? ⊚ ? ≡ ? )
      +
      +       		+
      +       		nstream ( ↑? ) ( ⫯? )nstream_eq + + nstream_isidnstream_id ( 𝐈𝐝 ) + + + + + nstream_sand + + nstream_istot ( ?@❴?❵ )nstream_after ( ? ∘ ? )
      +
      +       		+
      +       		mr2mr2_at ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      extensions to the library - ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minstream ( ? @ ? )stream_eq ( ? ≐ ? )stream_hdtl ( ↓? )stream_tls ( ↓*[?]? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      +
      +       		+
      +       		list ( ◊ ) ( ? @ ? ) ( |?| )list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      extensions to the library +
      +       		+
      +       		bool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      +
      +       		+
      +       		starlstar +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      generated logical decomposables - starlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? )list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      generated logical decomposables - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      - -
      +
      [Spacer]
      @@ -288,6 +707,6 @@

      -
      Last update: Tue, 04 Nov 2014 16:21:23 +0100
      - +
      Last update: Fri, 01 Apr 2016 23:30:52 +0200
      +