From: Ferruccio Guidi Date: Thu, 2 Feb 2012 18:43:22 +0000 (+0000) Subject: - one file and three lemmas added to Basic 2 X-Git-Tag: make_still_working~1956 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=974799592f0614ee54def765fb1775f3c0e98668;p=helm.git - one file and three lemmas added to Basic 2 - bugfix in Makefile --- diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile index 3cf252d5c..ee86004f7 100644 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile @@ -17,7 +17,7 @@ LDSRCDIR = ../../etc/lambda_delta/ HOMEDIR = ../../ TBLS = $(SRCDIR)ld_basic_2_src.tbl $(LDSRCDIR)Basic_2/ld_Basic_2_sum.tbl -XSLS = xhtbl.xsl ld_basic_2_sum.xsl ld_basic_2_src.xsl +XSLS = xhtbl.xsl ld_Basic_2_sum.xsl ld_basic_2_src.xsl LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl %.html: BASEURL = --stringparam baseurl $(LDURL) diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 5d7b4e9f1..484bdf19d 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -18,7 +18,7 @@
Here is a numerical acount of the contribution's contents and its timeline.
-
categoryobjects


propositionstheorems39lemmas333
conceptsdeclared33defined46
+
categoryobjects


propositionstheorems39lemmas336
conceptsdeclared33defined46
@@ -37,11 +37,11 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )

static typingstatic type assignmentstysty_liftsty_sty

local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba

atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa

parameterssh


unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift


partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops

generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector



lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts

support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector



lift ( ⇧[?,?] ? ≡ ? )lift_lift

grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs


term hom.thomthom_thom


closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )


internal syntaxgenv




lenvlenv_weight ( #[?] )lenv_length ( |?| )


termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector


item



external syntaxaarity


+
componentplanefiles



functionalreduction and type machinertmrtm_step ( ? ⇨ ? )



unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )


examples





native typing
nty



conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )



computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa


context-sensitive computationcprs (? ⊢ ? ➡* ?)




local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa

reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )





cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_tpsscpr_ltprcpr_cpr

context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif


context-free reductionltpr ( ? ➡ ? )ltpr_ldrop




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )


static typingstatic type assignmentstysty_liftsty_sty


local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba

atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa

parameterssh



unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift



partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops


generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector




lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts


support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps


global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop



basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop



basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector




lift ( ⇧[?,?] ? ≡ ? )lift_lift


grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs



term hom.thomthom_thom



closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )



internal syntaxgenv





lenvlenv_weight ( #[?] )lenv_length ( |?| )



termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector


item




external syntaxaarity



Physical structure of the contribution
The source files are grouped in directories, one for each component.
-
[Spacer]

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

Last update: 2012-02-01+01:00
+
[Spacer]

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

Last update: 2012-02-02+01:00
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl index 6c3b47928..636c0db74 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl @@ -69,7 +69,7 @@ table { [ { "reducibility" * } { [ { "context-sensitive reduction" * } { [ "lcpr ( ? ⊢ ➡ ? )" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_tpss" "cpr_ltpr" "cpr_cpr" * ] } ] [ { "context-free normal forms" * } {