X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=4fb7ca3042dac77076ca9a106af119f97a90ad74;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=d0349b2ad3aa0340d882488d3ce467308f6096ed;hpb=e866d78af74246133f5a14cb711a62af39308dee;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index d0349b2ad..4fb7ca304 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -1,18 +1,918 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + + Open Symbolic Notation (OSN) +
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+
Summary of the Specification [butterfly] +
+
Here is a numerical account of the specification's contents and its timeline. -
categoryobjects




sizesfiles93characters135543nodes314125
propositionstheorems38lemmas647total685
conceptsdeclared63defined67total130
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryunits +
+ 		+
+ 		+
+ 		+
+ 		+
+
sizescharacters (files)145725 (104)nodes (objects)337452 (911)intrinsic loss factor2.3
propositionstheorems42lemmas693total735
conceptsdeclared66defined73total139
+
+ + + + + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles
















generic rt-transition counterrtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )rtc_shift ( ↓? )rtc_max ( ? ∨ ? )rtc_plus ( ? + ? )












multiple relocationrtmaprtmap_eq ( ? ≗ ? )rtmap_pushs ( ↑*[?]? )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 ( ? ⊚ ? ≡ ? )rtmap_coafter ( ? ~⊚ ? ≡ ? )


nstream ( ↑? ) ( ⫯? )nstream_eqnstream_isidnstream_id ( 𝐈𝐝 )nstream_sandnstream_istot ( ?@❴?❵ )nstream_after ( ? ∘ ? )nstream_coafter ( ? ~∘ ? )


mr2mr2_at ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )













natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_plus ( ? + ? )











extensions to the librarystream ( ? @ ? )stream_eq ( ? ≐ ? )stream_hdtl ( ↓? )stream_tls ( ↓*[?]? )















list ( ◊ ) ( ? @ ? ) ( |?| )list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

















bool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )

















starlstar















generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ )

































[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
generic rt-transition counter + rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )rtc_shift ( ↓? )rtc_max ( ? ∨ ? )rtc_plus ( ? + ? ) +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
multiple relocation + rtmaprtmap_eq ( ? ≗ ? )rtmap_pushs ( ↑*[?]? )rtmap_nexts ( ⫯*[?]? )rtmap_tl ( ⫱? )rtmap_tls ( ⫱*[?]? )rtmap_isid ( 𝐈⦃?⦄ )rtmap_idrtmap_isdiv ( 𝛀⦃?⦄ )rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )rtmap_isfin ( 𝐅⦃?⦄ )rtmap_isuni ( 𝐔⦃?⦄ )rtmap_uni ( 𝐔❴?❵ )rtmap_sle ( ? ⊆ ? )rtmap_sdj ( ? ∥ ? )rtmap_sand ( ? ⋒ ? ≡ ? )rtmap_sor ( ? ⋓ ? ≡ ? )rtmap_at ( @⦃?,?⦄ ≡ ? )rtmap_istot ( 𝐓⦃?⦄ )rtmap_after ( ? ⊚ ? ≡ ? )rtmap_coafter ( ? ~⊚ ? ≡ ? )
+
+ 		+
+ 		nstream ( ↑? ) ( ⫯? )nstream_eq + + + + nstream_isidnstream_id ( 𝐈𝐝 ) + + + + + + + + nstream_sor + nstream_istot ( ?@❴?❵ )nstream_after ( ? ∘ ? )nstream_coafter ( ? ~∘ ? )
+
+ 		+
+ 		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 + stream ( ? @ ? )stream_eq ( ? ≐ ? )stream_hdtl ( ↓? )stream_tls ( ↓*[?]? ) +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
+
+ 		+
+ 		list ( ◊ ) ( ? @ ? ) ( |?| )list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
+
+ 		+
+ 		bool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
+
+ 		+
+ 		relations ( ? ⊆ ? )starlstar +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
generated logical decomposables + xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
+ + +
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+ 		+
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
+ +