X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=abeab7da6b1b4610100f853ff8e61df7817e5726;hb=12fd764a3ab9df02fcea5403bdc50387bb648887;hp=dbd2291ad9ddf40a6f4bd677c862f97fcb2af10f;hpb=22ff568044ad894d0e2a48bae84c13f95ee2d637;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index dbd2291ad..abeab7da6 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + \lambda\delta version 2 @@ -23,114 +23,9 @@
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i
-
-
local typed declaration **Γ ⊢ -λWⓐV→βno#i
-
-
global typed declaration ***Γ ⊢ pλWnonono$p
-
-
native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i
-
-
local definition **Γ ⊢ -δVnolocal →δno#i
-
-
global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
-
Summary of the Specification
+ +
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" @@ -142,54 +37,56 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles301 characters472212nodes1393133sizesfiles359characters429628nodes1855731
propositionstheorems89lemmas913total1002propositionstheorems127lemmas1276total1403
conceptsdeclared50defined73total123conceptsdeclared54defined85total139
+ +
Stage "B"
+ +
Stage "A": "Weakening the Applicability Condition"
+ + + +