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=0ac117159aa947b5dca92fc7a97e369bb893493b;hpb=cb5ca7ea4e826e9331eabeaea44353caab00071e;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0ac117159..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 files332 362 characters558713430997 nodes15194261829107
propositions theorems107123 lemmas11361300 total12431423
concepts declared5054 defined7984 total129138
@@ -94,16 +95,23 @@ + @@ -201,7 +209,8 @@ -
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. @@ -212,24 +221,52 @@ - - - - + + + - - + + + + + + + + + + + + - - + + @@ -243,7 +280,7 @@ - + @@ -352,7 +389,7 @@ - + @@ -392,7 +429,7 @@
- + - + - - + + @@ -493,8 +532,10 @@ - - + + @@ -520,8 +561,8 @@
- - + + @@ -573,10 +614,8 @@ - - + + @@ -645,7 +684,7 @@ - + @@ -716,18 +755,18 @@
- - - + + + - - - + + + @@ -739,9 +778,9 @@ - - - + + + @@ -753,9 +792,9 @@ - - - + + + @@ -767,9 +806,9 @@ - - - + + + @@ -781,9 +820,9 @@ - - - + + + @@ -795,9 +834,9 @@ - - - + + + @@ -810,7 +849,7 @@
- + - + - + - - + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -847,12 +928,24 @@
+ + + + + + + + - + - + - - + + @@ -932,10 +1025,10 @@ - + - - + + @@ -950,7 +1043,7 @@ - + @@ -966,8 +1059,8 @@
- - + + @@ -979,11 +1072,9 @@ - - - + + + @@ -995,9 +1086,9 @@ - - - + + + @@ -1009,11 +1100,9 @@ - + - + @@ -1026,8 +1115,8 @@
- - + + @@ -1068,7 +1157,7 @@ - + - +
componentplanefiles + componentplanefiles
+
+ +
+
examples + ex_cpr_omega +
+ 		+
+ 		+
+
+ + + +
+ 		+
+
dynamic typing local env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⊑[?,?] ? )lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snvlsubsv ( ? ⊢ ? ¡⫃[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv
stratified native validity snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcssnv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve
lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_ldrop lsx_lpx lsx_lpxs llsx_csxlsx_drop lsx_lpx lsx_lpxs llsx_csx
"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) fpbg_lift fpbg_fleq fpbg_fpbg
@@ -408,7 +445,7 @@
fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ ) fpbc_fleq fpbc_fpbs
@@ -465,8 +502,10 @@ 		context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxslpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs +
+
context-sensitive computation lprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )lprs_ldrop lprs_cprs lprs_lprslprs_drop lprs_cprs lprs_lprs +
+
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsubalsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_lleq lpx_aaa -
- 		lpx_drop lpx_freeslpx_lleq lpx_aaa
context-sensitive reduction lpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lprlpr_drop lpr_lpr
iterated static type assignmentlsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )lsstas_lift lsstas_aaa lsstas_lsstaslstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )lstas_lift lstas_aaa lstas_da lstas_lstas
static typinglocal env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsubalocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⫃ ? )lsubd_da lsubd_lsubd

atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_da aaa_ssta aaa_aaadegree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_sta da_da

stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_lpx_sn ssta_sstastatic type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? )sta_lift sta_lpx_sn sta_aaa sta_sta

local env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⊑ ? )lsubd_da lsubd_lsubdparametersshsd

degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_dalocal env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⫃ ? )lsuba_aaa lsuba_lsuba

parametersshsdatomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
restricted local env. ref.lsubr ( ? ⊑ ? )lsubr ( ? ⫃ ? ) lsubr_lsubr
@@ -820,9 +859,9 @@
substitutionmultiple substitution lazy equivalencefleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) fleq_fleq
@@ -838,8 +877,50 @@
lleq ( ? ⋕[?,?] ? )lleq_alt lleq_leq lleq_ldrop lleq_fqus lleq_lleqlleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq +
+ 		+
+
+
+ 		lazy pointwise extension of a relationllpx_snllpx_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 environmentsllor ( ? ⩖[?,?] ? ≡ ? )llor_alt llor_drop +
+ 		+
+
+
+ 		context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift
+
+ 		contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys +
+

iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) fqus_alt fqus_fqus
@@ -868,7 +961,7 @@
fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) fqup_fqup
@@ -882,8 +975,8 @@
iterated local env. slicingldrops ( ⇩*[?,?] ? ≡ ? )ldrops_ldrop ldrops_ldropsdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops
gr2_gr2
relocationsubstitution structural successor for closuresfquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )

fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdropgget ( ⇩[?] ? ≡ ? )gget_gget

pointwise union for local environmentsllor ( ? ⩖[?] ? ≡ ? ) -
- 		contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy

pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_snlocal env. ref. for extended substitutionlsuby ( ? ⊑×[?,?] ? )lsuby_lsuby

-
- 		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_leq ldrop_ldropdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop
grammar equivalence for local environmentsleq ( ? ≃[?,?] ? )leq ( ? ⩬[?,?] ? ) leq_leq
@@ -1082,7 +1171,7 @@
same top term constructortstc ( ? ≃ ? )tstc ( ? ≂ ? ) tstc_tstc tstc_vector
@@ -1183,7 +1272,8 @@
-
Physical Structure of the Specification
+ +
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
@@ -1213,6 +1303,6 @@

-
Last update: Wed, 16 Apr 2014 18:29:12 +0200
+
Last update: Fri, 04 Jul 2014 19:56:33 +0200