X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=f00ca8e1a767ad574c21dacc0b23716b23c9d0b5;hb=f8bf3abd773864388fef5efe599ac77f292a6b9d;hp=c1357bb4fe5a7c0cc6c6ca72c5800d9e1747f72c;hpb=63c047cae0056da7a69cb0740336d12259fbeb1a;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c1357bb4f..f00ca8e1a 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -25,7 +25,8 @@ -
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" @@ -37,50 +38,50 @@ - - - + + - - - - - + - + - + - + - + - + - + - +
categoryobjects + categoryobjects
+
+
+
+
sizes files361362 characters651753430997 nodes18193051829107
propositions theorems121123 lemmas12931300 total14141423
concepts declared 54 defined8184 total135138
@@ -94,9 +95,9 @@ -
Logical Structure of the Specification
+ +
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. Notation files covering the whole specification are provided. @@ -219,16 +221,44 @@ - - - - + + + + + + + + + + + + + + + - - @@ -236,7 +266,7 @@ - + @@ -359,7 +389,7 @@ - + @@ -472,7 +502,7 @@ - + @@ -502,7 +532,7 @@ - + @@ -532,7 +562,7 @@ - + @@ -584,7 +614,7 @@ - + - + @@ -725,8 +755,8 @@
- - + + - - + + - + @@ -862,7 +892,7 @@ - + @@ -876,7 +906,7 @@ - + @@ -945,8 +975,8 @@
- - + + @@ -1072,7 +1102,7 @@ - + @@ -1085,8 +1115,8 @@
- - + + @@ -1127,7 +1157,7 @@ - + - +
componentplanefiles + componentplanefiles +
+ 		+
+ 		+
+
examples + ex_cpr_omega +
+ 		+
+ 		+
+
+ + +
+
+
dynamic typing local env. ref. for stratified native validity lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )lsubsv_lsubd lsubsv_lsuba lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snvlsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv
lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_ldrop lsx_lpx lsx_lpxs llsx_csxlsx_drop lsx_lpx lsx_lpxs llsx_csx
context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxslpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
context-sensitive computation lprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_ldrop lprs_cprs lprs_lprslprs_drop lprs_cprs lprs_lprs
local env. ref. for abstract candidates of reducibility lsubc ( ? ⊢ ? ⫃[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsubalsubc_drop lsubc_drops lsubc_lsuba
context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_freeslpx_drop lpx_frees lpx_lleq lpx_aaa
@@ -654,7 +684,7 @@ 		context-sensitive reduction lpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lprlpr_drop lpr_lpr
iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? ) lstas_lift lstas_aaa lstas_da lstas_lstas
@@ -762,8 +792,8 @@
stratified static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? ) sta_lift sta_lpx_sn sta_aaa sta_sta
@@ -848,7 +878,7 @@
lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleqlleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq
lazy pointwise extension of a relation llpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llorllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
pointwise union for local environments llor ( ? ⩖[?,?] ? ≡ ? )llor_alt llor_ldropllor_alt llor_drop
iterated local env. slicingldrops ( ⇩*[?,?] ? ≡ ? )ldrops_ldrop ldrops_ldropsdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops
pointwise extension of a relation lpx_snlpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
basic local env. slicingldrop ( ⇩[?,?,?] ? ≡ ? )ldrop_append ldrop_leq ldrop_ldropdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop
grammar equivalence for local environmentsleq ( ? ≃[?,?] ? )leq ( ? ⩬[?,?] ? ) leq_leq
@@ -1141,7 +1171,7 @@
same top term constructortstc ( ? ≃ ? )tstc ( ? ≂ ? ) tstc_tstc tstc_vector
@@ -1242,7 +1272,8 @@
-
Physical Structure of the Specification
+ +
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
@@ -1272,6 +1303,6 @@

-
Last update: Sat, 14 Jun 2014 22:17:35 +0200
+
Last update: Fri, 04 Jul 2014 19:56:33 +0200