From: Ferruccio Guidi Date: Thu, 7 Aug 2014 17:19:49 +0000 (+0000) Subject: - update in basic_2 X-Git-Tag: make_still_working~859 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abd0169d8025bf4d613a612231ad5b0c4c1db009;p=helm.git - update in basic_2 - minor updates in the web site, including css bugfix --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index f60e245c4..30791b955 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -31,165 +31,165 @@ - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + - - + - - - - - - - - - - - + + + + + + + + + + - - - - - - + - - - - - - - - - - - - - + + + + + + + + + + + + - - - - + - - - - - - - - - + + + + + + + + - - - - - - @@ -223,6 +223,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 96254d846..455542b95 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -55,50 +55,50 @@
classcontents + classcontents
+
+
+
+
+
+
+
+
+
+
+
+
+
+
p -
- 		147101316192225283134374043p +
+ 		147101316192225283134374043
q + q
5111517232933354145 + 5111517232933354145
+
+
+
+
s + s
268141820242632384244 + 268141820242632384244
+
+
t + t
39122127303639 + 39122127303639
+
+
+
+
+
+
- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles4characters2567nodes3637sizesfiles4characters2567nodes3637
propositionstheorems2lemmas1total3propositionstheorems2lemmas1total3
conceptsdeclared3defined9total12conceptsdeclared3defined9total12
@@ -134,26 +134,26 @@ - - - - + + + - - - - + + + + - - - - + + @@ -191,6 +191,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 10a18c27f..d8633e5ff 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -37,50 +37,50 @@
componentplanefiles + componentplanefiles
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
+
relocationlift ( ↑[?,?] ? ) + relocationlift ( ↑[?,?] ? )
- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles367characters432045nodes1831215sizesfiles367characters431848nodes1830463
propositionstheorems128lemmas1303total1431propositionstheorems128lemmas1303total1431
conceptsdeclared55defined82total137conceptsdeclared55defined84total139
@@ -219,1066 +219,1070 @@ - - - - + + + - - - - - - + + + - - - - - - - - - - + + + + - - - - - - + + + - - - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - + + + - - - - - - - + + + - - - - - - - + + + + - - - - - + + + - - - - - - - + + + - - - - - + + - - - - - - - + + + - - - - - + + + - - - - - - + + - - - - - - - + + + - - - - - - + + + - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - - + + + + - - - - - + + + + - - - - - - + + + - - + + + + - - - - - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - + + + - - - - - - - - + + + + - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - - + + + + - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - - + + + + + - - - - - + + + + - - - - - + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - + + - - - - - - - - + + + + - - - - - - + + + + - - - - + - - - - - - + + - - @@ -1316,6 +1320,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index 7ee236c53..de85f44d0 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -46,6 +46,13 @@ div.head2dx { font-size: x-large; } +div.head3sn { + margin: 0.5em 0; + text-align: left; + font-weight: bold; + font-size: large; +} + div.text { margin: 1em 0; text-align: left; @@ -58,6 +65,20 @@ span.date { font-size: medium; } +/* tables *******************************************************************/ + +table { + margin-left: auto; + margin-right: auto; + width: 100%; +} + +td { + border-color:#000000; + border-width:1px; + color:#000000; +} + /* inline decorations *******************************************************/ img.icon32 { @@ -85,20 +106,6 @@ img.w3c { height: 32px; /* this should be 31px */ } -/* alignment ****************************************************************/ - -td.top { - vertical-align: top; -} - -td.middle { - vertical-align: middle; -} - -td.bottom { - vertical-align: bottom; -} - /* background colors ********************************************************/ .gray { diff --git a/helm/www/lambdadelta/css/xhtbl.css b/helm/www/lambdadelta/css/xhtbl.css index f58db47c3..5ef81f018 100644 --- a/helm/www/lambdadelta/css/xhtbl.css +++ b/helm/www/lambdadelta/css/xhtbl.css @@ -1,46 +1,5 @@ @charset "UTF-8"; -/* positioning **************************************************************/ - -table { - margin-left: auto; - margin-right: auto; - width: 100%; -} - -td { - border-color:#000000; - border-width:1px; - color:#000000; -} - -/* content types ************************************************************/ - -.text { - font-style: normal; -} - -.component { - font-style: italic; - text-transform: capitalize; -} - -.plane { - font-style: italic; - text-transform: lowercase; -} - -.file { - font-style: normal; - text-transform: lowercase; -} - -.number { - text-align: right; - font-style: italic; - text-transform: lowercase; -} - /* cell borders *************************************************************/ td.nnnn { @@ -106,3 +65,57 @@ td.sssn { td.ssss { border-style:solid solid solid solid; } + +/* text alignment ***********************************************************/ + +td.left { + text-align: left; +} + +td.center { + text-align: center; +} + +td.right { + text-align: right; +} + +td.justify { + text-align: justify; +} + +td.top { + vertical-align: top; +} + +td.middle { + vertical-align: middle; +} + +td.bottom { + vertical-align: bottom; +} + +/* text style ***************************************************************/ + +td.capitalize { + text-transform: capitalize; +} + +td.lowercase { + text-transform: lowercase; +} + +td.uppercase { + text-transform: uppercase; +} + +/* font style ***************************************************************/ + +td.upright { + font-style: normal; +} + +td.italic { + font-style: italic; +} diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index c4fd0e37f..9dcf6aaf2 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -30,19 +30,19 @@
componentplanefiles + componentplanefiles
+
+
examplesterms with special featuresex_cpr_omega + examplesterms with special featuresex_cpr_omega
+
+
- - - + + + +
+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv + dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv
+
+
stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )shnv_aaa + stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )shnv_aaa
+
+
+
snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve + snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve
+
equivalencedecomposed extended equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes + equivalencedecomposed extended equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes
+
+
context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs + context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc + conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
+
computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) + computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
+
+
+
evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre + evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
+
+
strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx + strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx
+
strongly normalizing extended computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx + strongly normalizing extended computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx
+
+
+
lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx + lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx
+
+
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa
+
+
+
csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs + csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
+
"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbg + "big tree" parallel computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbg
+
+
+
fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq fpbc_fpbs + fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq fpbc_fpbs
+
+
+
fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleqfpbu_fleq + fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleq fpbu_fleq +
+
+
+
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext + fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext
+
decomposed extended computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds + decomposed extended computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds
+
+
context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
+
+
+
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs + cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
+
+
context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs + context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs
+
+
+
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs + cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs
+
+
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba + local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
+
+
support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa + support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa
reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa + reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa
+
+
normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix + normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix
+
+ +
+ 		context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa
context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_freeslpx_lleq lpx_aaa +
+
+
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix + cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
+
+
irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift + irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift
+
+
reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift + reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift
+
+
normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir + normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir
+
+
context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr + context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr
+
+
+
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir + cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir
+
+
irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift + irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
+
+
reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift + reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift
+
unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) + unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
+
+
+
iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )lstas_lift lstas_aaa lstas_da lstas_lstas + iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )lstas_lift lstas_aaa lstas_da lstas_lstas
static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd + static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd
+
+
degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_sta da_da + degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_sta da_da
+
+
static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? )sta_lift sta_lpx_sn sta_aaa sta_sta + static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? )sta_lift sta_lpx_sn sta_aaa sta_sta
+
+
parametersshsd + parametersshsd
+
+
local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba + local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba
+
+
atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa + atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
+
+
restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr + restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
+
multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq + multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq
+
+
+
lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq + lleq ( ? ≡[?,?] ? )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 + 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 + pointwise union for local environmentsllor ( ? ⩖[?,?] ? ≡ ? )llor_alt llor_drop
+
+
context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift + context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift
+
+
contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys + contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys
+
iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus + iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus
+
+
+
fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup
+
+
iterated local env. slicingdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops + iterated local env. slicingdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops
+
+
generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector + generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector
+
+
+
lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts + lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts
+
+
support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) + substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
+
+
+
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
+
+
+
global env. slicinggget ( ⇩[?] ? ≡ ? )gget_gget + global env. slicinggget ( ⇩[?] ? ≡ ? )gget_gget
+
+
contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy + contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy
+
+
local env. ref. for extended substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby + local env. ref. for extended substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby
+
+
pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn + pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
+
+
basic local env. slicingdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop + basic local env. slicingdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop
+
+
basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector + basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector
+
+
+
lift ( ⇧[?,?] ? ≡ ? )lift_neq lift_lift + lift ( ⇧[?,?] ? ≡ ? )lift_neq lift_lift
+
grammarequivalence for local environmentsleq ( ? ⩬[?,?] ? )leq_leq + grammarequivalence for local environmentsleq ( ? ⩬[?,?] ? )leq_leq
+
+
same top term constructortstc ( ? ≂ ? )tstc_tstc tstc_vector + same top term constructortstc ( ? ≂ ? )tstc_tstc tstc_vector
+
+
closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) + closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} )
+
+
internal syntaxgenv + internal syntaxgenv
+
+
+
+
lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+
termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+
item + item
+
+
+
external syntaxaarity + external syntaxaarity
+
+
- - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -333,6 +333,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz index 92c594dfc..1ddea2156 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index fbbf1bc61..463a398fe 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -35,50 +35,50 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles31characters46619nodes61911sizesfiles31characters46619nodes61911
propositionstheorems2lemmas185total187propositionstheorems2lemmas185total187
conceptsdeclared40defined25total65conceptsdeclared40defined25total65
@@ -107,96 +107,96 @@ - - - + + - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - + + - - - - - - - - - - - + + + - - - - - - @@ -234,6 +234,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 5d255e3fe..450f6a6ba 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -30,19 +30,19 @@
planefiles + planefiles
+
+
+
+
+
+
+
natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minnatural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_min
extensions to the libraryarith.ma ( ?^? ) + extensions to the libraryarith.ma ( ?^? )
+
+
+
+
+
+
+
generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) + generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ )
+
+
+
+
+
+
- - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -90,39 +90,42 @@ - - - - - - - + + + + + + + + - - - + - - - - + + + + + - - - + - - - - + + + +
versionnamedeveloped withstartedannouncedreleaseddismissedversionnamedeveloped withstagestartedannouncedreleaseddismissed
2 - basic_2 + + Version 2 + "basic_2" Matita 0.99.2 April 2011July 2014Planned in 2014Not planned yet"a"April 2011July 2014Planned in 2014Not planned yet
1 - basic_1 + + Version 1 + "basic_1" Coq 7.3.1 May 2004January 2006November 2006May 2008 + May 2004January 2006November 2006May 2008
@@ -263,6 +266,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 791c7fbb2..944beb7ba 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -30,19 +30,19 @@ - - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -135,6 +135,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index f6c7dee91..76152d9c5 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -30,19 +30,19 @@ - - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -303,6 +303,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:28 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index ea0501e2a..90e8326b3 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -30,19 +30,19 @@ - - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -167,6 +167,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index e8b2cd74a..bbd38fe2f 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -30,19 +30,19 @@ - - - - - +
+ home + news + documentation + implementation (specifications - library - Helena)(specifications - library - Helena)
@@ -131,6 +131,6 @@

-
Last update: Wed, 06 Aug 2014 20:50:29 +0200
+
Last update: Thu, 07 Aug 2014 19:13:43 +0200
diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index df44a964b..6f9092683 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -31,6 +31,6 @@ table [ } ] -class "component" [ 0 ] +class "capitalize italic" [ 0 ] ext ".html" [ * ] diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index 590c8e11c..e8bb5117b 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -3,17 +3,19 @@ name "versions" table { class "gray" [ "version" "name" "developed with" - "started" "announced" "released" "dismissed" + "stage" "started" "announced" "released" "dismissed" ] class "orange" - [ "2" @@("version_2" "basic_2") @("http://matita.cs.unibo.it/" "Matita 0.99.2") - "April 2011" "July 2014" "Planned in 2014" "Not planned yet" + [ @@("version_2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") + "\"a\"" "April 2011" "July 2014" "Planned in 2014" "Not planned yet" ] class "red" - [ "1" @@("version_1" "basic_1") @("http://coq.inria.fr/" "Coq 7.3.1") - "May 2004" "January 2006" "November 2006" "May 2008" ] + [ @@("version_1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1") + "" "May 2004" "January 2006" "November 2006" "May 2008" ] } -class "component" [ 0 ] +class "top" { * } + +class "capitalize italic" [ 0 ] ext ".html" { 1 }