X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=bb02948198fcc45300fd42b197368b3a4e26026d;hb=b1c1894b6ee9a48c3b0bacd09be00938d8e20341;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..bb0294819 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -16,14 +16,14 @@
- [lambdadelta home] + [\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
- [Spacer] + [Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,15 +62,21 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + +
@@ -74,29 +86,28 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)
- -
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,74 @@ - + - + - + - + - + - + - + - + - +
sizes files3086 characters68581109249 nodes62380217872
propositions theorems230 lemmas187506 total189536
concepts declared4059 defined2555 total65114
-
    +
      +
    • + 2016 April 18. + Generic rt-transition counter (rtc). +
      • +
    +
      +
    • + 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 +227,444 @@ + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - + + + + + + + + + + + + @@ -232,10 +679,35 @@ - + - + + + + + + + + + @@ -261,9 +733,8 @@

      		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      natural numbers with infinitygeneric rt-transition counter + rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )rtc_shift ( ↓? )rtc_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 ( ? ▭ ? ≡ ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      natural numbers with infinity + ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_plus ( ? + ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      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 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      +
      +       		+
      +       		bool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      +
      +       		+
      +       		starlstar +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      extensions to the librarygenerated logical decomposables - starlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? )list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      generated logical decomposables - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +       		+
      +
      - -
      - [Spacer] +
      + [Spacer]

      @@ -288,6 +759,6 @@

      -
      Last update: Tue, 04 Nov 2014 16:21:23 +0100
      - +
      Last update: Sat, 21 May 2016 22:22:39 +0200
      +