X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=bbde8e1cf45d067ed3727363a9d833c9768bac5a;hb=22d35425b8f5f7e479db3be59b73f76d77ae6711;hp=332935d9a7b08cd9bc04c72a0d07ad4c1a86c67f;hpb=5cdcab1eddf82a94fc9911cbadb1132ffc8ae4b6;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 332935d9a..bbde8e1cf 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + \lambda\delta version 2 @@ -133,6 +133,10 @@
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" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78].
@@ -159,27 +163,27 @@ - + - + - + - + - + - + - + - + @@ -196,22 +200,50 @@ + + + + - - - - - - - - - - - - - - - - - - - - - - + + @@ -343,11 +339,8 @@
- - - + + @@ -357,12 +350,9 @@ - - - - + + + @@ -374,14 +364,9 @@ - - - - + + + @@ -390,98 +375,96 @@ - - - - - - + + + + - - - - - - + + + - - - - - - - - + + + - - - + + + + - - - + + - + + + - - - - - - - + + - - - - - - + + + @@ -496,11 +479,20 @@ - - - + + + + + + + + + @@ -512,12 +504,11 @@ - - - - + + @@ -529,12 +520,11 @@ - - - - + + @@ -546,15 +536,12 @@ - - - - - + + + @@ -563,12 +550,9 @@ - - - - + + + @@ -580,15 +564,24 @@ - - - + + + - + + + + + + + @@ -597,10 +590,11 @@ - - - - + + + @@ -612,14 +606,23 @@ - + + + + - - - + + + + + @@ -632,14 +635,11 @@
- + - @@ -650,23 +650,17 @@ - + - - - - - - + + + + @@ -678,10 +672,9 @@ - - - - + + + @@ -693,14 +686,9 @@ - - - - + + + @@ -712,12 +700,11 @@ - - - - + + @@ -729,12 +716,9 @@ - - - - + + + @@ -746,11 +730,12 @@ - - - - - + + + + @@ -759,14 +744,23 @@ - - + + + - + + + + + + @@ -778,12 +772,11 @@ - - - - + + @@ -795,14 +788,23 @@ - + + + - - - + + + + + + @@ -811,10 +813,9 @@ - - - - + + + @@ -826,33 +827,25 @@ - - - - - - - + + + + - + - + - @@ -862,11 +855,8 @@
- - - + + @@ -878,12 +868,9 @@ - - - - + + + @@ -892,65 +879,53 @@ - - - - - - + + + - - - - - - - + + + - - - - - - - + + + - - - - - - - + + + + + @@ -959,13 +934,10 @@ - - - - - + + + + @@ -974,12 +946,9 @@ - - - - + + + @@ -991,12 +960,11 @@ - - - - + + @@ -1008,14 +976,9 @@ - - - - + + + @@ -1033,9 +996,6 @@ - @@ -1052,9 +1012,6 @@ - @@ -1067,19 +1024,27 @@ - - + + + + + + + + - - - - - + + + @@ -1091,12 +1056,23 @@ - - - + + + + + + + + + + @@ -1108,9 +1084,10 @@ - - - + + @@ -1125,10 +1102,9 @@ - - - - + + + @@ -1140,14 +1116,9 @@ - - - - + + + @@ -1165,9 +1136,6 @@ - @@ -1184,21 +1152,29 @@ - - - - + + + + + + + + + + @@ -1216,9 +1192,6 @@ - @@ -1228,11 +1201,8 @@
- - - + + @@ -1252,9 +1222,6 @@ - @@ -1269,8 +1236,7 @@ - - + - - + - @@ -1320,9 +1280,6 @@ - @@ -1361,6 +1318,6 @@

-
Last update: Mon, 18 Mar 2013 20:23:14 +0100
+
Last update: Mon, 24 Feb 2014 19:58:07 +0100
sizes files250 329 characters484808567347 nodes13048881610281
propositions theorems84105 lemmas11121114 total11961219
concepts declared4552 defined8376 total 128

-
-
dynamic typing"big tree" parallel computationyprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )yprs_yprsygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )ygt_ygt -
-
-
- 		"big tree" parallel reductionypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) -
- 		-
- 		-
-
-
- 		local env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⊑[?] ? )lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv -
- 		lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv
stratified native validitysnv ( ⦃?,?⦄ ⊢ ? ¡[?] )snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs -
- 		snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs
equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs -
- 		decomposed extended equivalencecpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )cpes_cpds

-
- 		fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs -
- 		context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
-
- 		local env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_cpcs -
- 		+ conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
+
-
- 		context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs + computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
+
+
conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc +
+ evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
+
+
+ strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx
fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc +

+ strongly normalizing extended computationlcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )lcosx_cpxs
+
+
context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc +
+ lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )lsx_ldrop lsx_cpxs lsx_csx
+
computationfocalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs + +
+
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa

fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs + csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lpx csx_lpxs csx_fpbs +
+

"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fpns fpbg_fpbg

decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs +
fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )fpbc_fpns fpbc_fpbs

weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe +
fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_fpns

strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa -
- 		+
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs fpbs_ext

-
- 		csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfprparallel computation for "big tree" normal formsfpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )fpns_fpns

context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vectordecomposed extended computationcpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )cpds_lift cpds_aaa cpds_cpds
+ +
+

context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs +
+ 		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs

+ context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )lprs_ldrop lprs_cprs lprs_lprs
tprs ( ? ➡* ?)tprs_lift tprs_tprs +

+
+ 		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc ( ? ⊢ ? ⊑[?] ? ) lsubc_ldrop lsubc_ldrops lsubc_lsuba
-
-
support for abstract computation properties acpacp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) acp_aaa -
-
reducibilitycontext-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr -
- 		reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa

context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfprnormal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix

-
- 		fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr -
- 		context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_cpys lpx_lleq lpx_aaa

context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif +
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lift cpx_cpys cpx_lleq cpx_cix

context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr -
- 		irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift

context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_appendreducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift +
+

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir
+ +
+

context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lpr

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr +
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_cir

+ irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
tpr ( ? ➡ ? )tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr + +
+

reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift
unwinditerated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_sstasunfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
static typingstratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta +
-
- 		+ iterated static type assignmentlsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )lsstas_lift lsstas_aaa lsstas_lsstas
-
- 		static typing local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba ( ? ⊢ ? ⁝⊑ ? ) lsuba_ldrop lsuba_aaa lsuba_lsuba
-
-
atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa -
- 		aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_da aaa_ssta aaa_aaa

parametersshsd -
- 		stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ssta
unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift +
+ local env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⊑ ? )lsubd_da lsubd_lsubd
+
+
inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift + degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_da
+
+
partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn + parametersshsd
+
-
- 		-
- 		ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx -
- 		-
- 		substitutionlazy equivalence for local environmentslleq ( ? ⋕[?,?] ? )lleq_alt ( ? ⋕⋕[?,?] ? )lleq_ldrop lleq_fqus lleq_lleq lleq_ext

-
- 		tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpsscontxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops -
- 		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )fqus_alt fqus_fqus

iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups +
fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )fqup_fqup

-
- 		frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp -
- 		iterated local env. slicingldrops ( ⇩*[?,?] ? ≡ ? )ldrops_ldrop ldrops_ldrops

-
-

-
-
gr2 ( @⦃?,?⦄ ≡ ? ) gr2_plus ( ? + ? ) gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2 + gr2_gr2
relocationcontxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_cpy +
+
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps +
restricted local env. ref.lsubr ( ? ⊑ ? )lsubr_lsubr

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdroplocal env. ref. for extended substitutionlsuby ( ? ⊑×[?,?] ? )lsuby_lsuby
+
+
+
+ 		structural successor for closuresfquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )

basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_lbotr ldrop_ldrop +
+ 		fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )

local env. ref. for substitutionlsubr ( ? ⊑[?,?] ? )(lsubr_lsubr)lsubr_lbotr ( ⊒[?,?] ? )global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop

restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ ) -
- 		-
- 		basic local env. slicingldrop ( ⇩[?,?,?] ? ≡ ? )ldrop_lpx_sn ldrop_leq ldrop_ldrop

-
-

-
-
grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)equivalence for local environmentsleq ( ? ≃[?,?] ? )leq_leq
+
+
+
+ 		pointwise extension of a relationlpx_snlpx_sn_tc lpx_sn_lpx_sn

-
-
closurescl_shift ( ? @@ ? )cl_weight ( ♯{?,?} ) -
- 		cl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} )

-
-
lenv lenv_weight ( ♯{?} ) lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bilenv_append ( ? @@ ? )
@@ -1282,10 +1248,7 @@ term term_weight ( ♯{?} ) term_simple ( 𝐒⦃?⦄ )term_vector -
- 		term_vector
@@ -1301,9 +1264,6 @@
-
-

-
-