From: Ferruccio Guidi Date: Fri, 9 Mar 2012 17:38:40 +0000 (+0000) Subject: - update in Basic_2 X-Git-Tag: make_still_working~1865 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=011cf6478141e69822a5b40933f2444d0522532f;p=helm.git - update in Basic_2 - we added some information in thesunnary tables --- diff --git a/helm/www/lambda_delta/ld_apps_2.html b/helm/www/lambda_delta/ld_apps_2.html index 53c4433c9..fc3149597 100644 --- a/helm/www/lambda_delta/ld_apps_2.html +++ b/helm/www/lambda_delta/ld_apps_2.html @@ -32,7 +32,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
+
categoryobjects




volumefiles5



propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
@@ -57,6 +57,6 @@
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-27+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-03-09+01:00
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index da3ebdad3..d894aef11 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -29,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




propositionstheorems43lemmas422total465
conceptsdeclared32defined35total67
+
categoryobjects




volumefiles112



propositionstheorems45lemmas437total482
conceptsdeclared32defined38total70
@@ -53,12 +53,12 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
componentplanefiles




examples






native typing
nty




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




computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_lcpr_vectorcsn_aaa




csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr

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

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


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


reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift




context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_cpr





cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr

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



context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps




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




same head term formtshf ( ? ≈ ? )tshf_tshf




same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector



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




internal syntaxgenv






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




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



item





external syntaxaarity




+
componentplanefiles





examples







native typing
nty





equivalencecontext-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )





conversioncontext-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc




computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_lcpr_vectorcsn_aaa





csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr


context-sensitive computationlcprs ( ? ⊢ ➡* ? )lcprs_cprslcprs_lcprs





cprs (? ⊢ ? ➡* ?)cprs_liftcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

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



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



reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift





context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_cpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr


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




context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps





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





same head term formtshf ( ? ≈ ? )tshf_tshf





same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector




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





internal syntaxgenv







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





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




item






external syntaxaarity





Physical Structure of the Specification
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-27+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-03-09+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 4aa167747..3230de487 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 @@ -9,7 +9,7 @@ table { ] } ] - class "blue" + class "prune" [ { "examples" * } { [ { "" * } { [ "" * ] @@ -17,7 +17,7 @@ table { ] } ] - class "sky" + class "blue" [ { "native typing" * } { [ { "" * } { [ "nty" * ] @@ -25,10 +25,18 @@ table { ] } ] + class "sky" + [ { "equivalence" * } { + [ { "context-sensitive equivalence" * } { + [ "cpcs ( ? ⊢ ? ⬌* ? )" * ] + } + ] + } + ] class "cyan" [ { "conversion" * } { [ { "context-sensitive conversion" * } { - [ "cpcs ( ? ⊢ ? ⬌* ? )" * ] + [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] } ] } @@ -41,7 +49,8 @@ table { } ] [ { "context-sensitive computation" * } { - [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_tstc" "cprs_tstc_vector" * ] + [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_cprs" "lcprs_lcprs" * ] + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } { diff --git a/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl b/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl deleted file mode 100644 index db1af3954..000000000 --- a/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl +++ /dev/null @@ -1,44 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryobjects




propositionstheorems0lemmas23total23
conceptsdeclared22defined8total30
- - -