From: Ferruccio Guidi Date: Sat, 29 Sep 2012 17:33:22 +0000 (+0000) Subject: - updates in basic_2 X-Git-Tag: make_still_working~1501 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c66eccc53d2b3000a905f9172b66cf6f9e2131a6;p=helm.git - updates in basic_2 --- diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html index df98ff499..010147746 100644 --- a/helm/www/lambda_delta/BTM.html +++ b/helm/www/lambda_delta/BTM.html @@ -18,8 +18,8 @@
This table shows how the first 45 positive integers are distributed in the four classes.
-
classcontents














p
147101316192225283134374043
q
5111517232933354145




s
268141820242632384244


t
39122127303639






+
-
[Spacer]

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

Last update: 2012-08-24T19:13:53+02: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-09-29T19:32:27+02:00
diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index 7527557c9..9ebf3a8e0 100644 --- a/helm/www/lambda_delta/apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -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-08-24T19:07:32+02: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-09-29T19:32:27+02:00
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 1ea8c5b09..01f3ea9d6 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -74,12 +74,12 @@ The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).
-
componentplanefiles







dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_liftsnv_aaa





equivalencecontext-sensitive equivalencelcpcs ( ? ⊢ ⬌* ? )lcpcs_aaalcpcs_lcprslcpcs_lcpcs






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc








cpc ( ? ⊢ ? ⬌ ? )cpc_cpc






computationextended computationxprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )xprs_liftxprs_aaaxprs_cprs





weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe







strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa






csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_liftcsn_cprcsn_lcpr




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






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_ltprcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldropltprs_ltprs






tprs ( ? ➡* ?)tprs_lifttprs_tprs






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





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





reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )xpr_liftxpr_aaa






context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift


cnf_cif



context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_aaalcpr_cprlcpr_lcpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_deliftcpr_ltprcpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append





context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )








context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_aaaltpr_ltpr




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr



unwind









static typinglocal env. ref. for stratified static type assignmentlsubss ( ? ⁝⊑ ? )lsubss_ldroplsubss_sstalsubss_lsubss





stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_liftssta_ltpssssta_aaassta_ssta




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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpssaaa_aaa




parametersshsd






unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldropthin_delift






inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift



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





tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss





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 substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps






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







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




local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )lsubs_lsubslsubs_sfr ( ≽[?,?] ? )






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








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






grammarsame head term formtshf ( ? ≈ ? )tshf_tshf







same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector






closurescl_shift ( ? @@ ? )cl_weight ( #{?,?} )







internal syntaxgenv









lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px





termterm_weight ( #{?} )term_simple ( 𝐒⦃?⦄ )term_vector






item








external syntaxaarity







+
componentplanefiles







dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_liftsnv_aaa





equivalencecontext-sensitive equivalencelcpcs ( ? ⊢ ⬌* ? )lcpcs_aaalcpcs_lcprslcpcs_lcpcs






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc








cpc ( ? ⊢ ? ⬌ ? )cpc_cpc






computationextended computationxprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )xprs_liftxprs_aaaxprs_cprs





weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe







strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa






csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_liftcsn_cprcsn_lcpr




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






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_ltprcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldropltprs_ltprs






tprs ( ? ➡* ?)tprs_lifttprs_tprs






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





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





reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )xpr_liftxpr_aaa






context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift


cnf_cif



context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_aaalcpr_cprlcpr_lcpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_deliftcpr_ltprcpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append





focalized reductionlfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )









fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )








context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )








context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpss_dxltpr_ltpss_snltpr_aaaltpr_ltpr



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr



unwind









static typinglocal env. ref. for stratified static type assignmentlsubss ( ? ⁝⊑ ? )lsubss_ldroplsubss_sstalsubss_lsubss





stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_liftssta_ltpss_dxssta_ltpss_snssta_aaassta_ssta



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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpss_dxaaa_ltpss_snaaa_aaa



parametersshsd






unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldropthin_delift






inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift



partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_ldropltpss_sn_tpsltpss_sn_tpssltpss_sn_ltpss_snltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )




ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldropltpss_dx_tpsltpss_dx_tpssltpss_dx_ltpss_dx





tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss





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 substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps






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







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




local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? )






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








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






grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)







same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector






closurescl_shift ( ? @@ ? )cl_weight ( #{?,?} )







internal syntaxgenv









lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_pxlenv_px_bi




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-08-24T19:07:32+02: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-09-29T19:32:27+02:00
diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl index 4584f08f2..30591ab89 100644 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -127,7 +127,7 @@ table { } ] [ { "context-free reduction" * } { - [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss" "ltpr_aaa" "ltpr_ltpr" * ] + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss_dx" "ltpr_ltpss_sn" "ltpr_aaa" "ltpr_ltpr" * ] [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_delift" "tpr_tpr" * ] } ]