X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2fd65b8cd1e980dca197760d1c519ce671381393;hb=8913001064f595c21ed4234884e7c370be2afb52;hp=cd756f629a03988a1c1d8f02cc8894a8acd341d6;hpb=640716b0624d2a7cd9f339b9ab975e85b3288a50;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index cd756f629..2fd65b8cd 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -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,21 +200,33 @@ + + - - - - - - - - - - - - - - - - - - - - - - + + @@ -351,11 +331,8 @@
- - - + + @@ -365,48 +342,9 @@ - - - - - - - - - - - - - - - - - - - - - - + + + @@ -419,11 +357,8 @@
- - - + + @@ -433,12 +368,9 @@ - - - - + + + @@ -447,49 +379,40 @@ - - - - - + + + - - - - - - - - + + + - - - - - - + + + @@ -504,14 +427,9 @@ - - - - + + + @@ -520,12 +438,9 @@ - - - - + + + @@ -537,15 +452,12 @@ - - - - - + + + @@ -554,12 +466,9 @@ - - - - + + + @@ -571,15 +480,10 @@ - - - - - + + + + @@ -588,12 +492,11 @@ - - - - + + @@ -605,13 +508,10 @@ - - - - - + + + + @@ -623,11 +523,8 @@ - - - + + @@ -640,14 +537,11 @@
- + - @@ -658,38 +552,17 @@ - + - - - - - - - - - - - - - - - + + + + @@ -704,11 +577,8 @@ - - - + + @@ -720,12 +590,9 @@ - - - - + + + @@ -737,12 +604,9 @@ - - - - + + + @@ -757,11 +621,8 @@ - - - + + @@ -773,12 +634,9 @@ - - - - + + + @@ -790,11 +648,12 @@ - - - - - + + + + @@ -803,14 +662,9 @@ - - - - + + + @@ -822,12 +676,9 @@ - - - - + + + @@ -842,11 +693,8 @@ - - - + + @@ -855,48 +703,37 @@ - - - - - - + + + - - - - - - - + + + - - + - - + @@ -911,27 +748,19 @@ - - - - - + + + + - - - - + + + @@ -943,12 +772,9 @@ - - - - + + + @@ -960,12 +786,9 @@ - - - - + + + @@ -977,12 +800,9 @@ - - - - + + + @@ -991,32 +811,38 @@ - - - - - - + + + - - - + + + - - - + + + + + + @@ -1029,11 +855,8 @@
- - - + + @@ -1048,11 +871,8 @@ - - - + + @@ -1070,9 +890,6 @@ - @@ -1087,9 +904,6 @@ - @@ -1106,9 +920,6 @@ - @@ -1121,24 +932,14 @@ - - + - - - - + + + @@ -1153,9 +954,6 @@ - @@ -1166,25 +964,7 @@ - - - - - - - - - - - + @@ -1202,9 +982,6 @@ - @@ -1221,21 +998,15 @@ - - - - - + + + @@ -1253,9 +1024,6 @@ - @@ -1266,10 +1034,7 @@ - - + @@ -1289,9 +1054,6 @@ - @@ -1306,8 +1068,7 @@ - - + - - + - @@ -1357,9 +1112,6 @@ - @@ -1398,6 +1150,6 @@

-
Last update: Sat, 20 Apr 2013 21:34:40 +0200
+
Last update: Sat, 12 Oct 2013 19:38:34 +0200
sizes files237 268 characters420425407502 nodes10631171213911
propositions theorems8583 lemmas946826 total1031909
concepts declared4544 defined8081 total 125

-
-
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 -
- 		-
- 		-
-
-
- 		-
- 		fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs -
- 		-
- 		-
-
-
- 		local env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_cpcs -
- 		decomposed extended equivalencecpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )cpes_cpds
context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs -
- 		cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc -
- 		context-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
-
- 		-
- 		fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc + computationcontext-sensitive extended evaluationcpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
+
+
-
- 		context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc +
+ context-sensitive evaluationcpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
+
computationfocalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs +
strongly normalizing computationcsx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa

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

decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs -
- 		"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fpbg

weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe -
- 		+
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fpbs

strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa -
- 		decomposed extended computationcpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )cpds_lift cpds_aaa cpds_cpds

-
- 		csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr -
- 		context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs

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_vector +
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs -
- 		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 -
- 		-
- 		-
-
-
- 		context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfprreduction"big tree" parallel reductionfpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbc_lift

fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr -
- 		fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift

context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif -
- 		context-sensitive extended normal formscnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )cnx_lift cnx_crx cnx_cix

revised context-sensitive reductionlpr ( ? ⊢ ➡ ? )lpr_ldrop lpr_cpr lpr_lpr -
- 		context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_aaa

cpr ( ? ⊢ ? ➡ ? )cpr_lift -
- 		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lift cpx_cix

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

context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_appendcontext-sensitive extended reducible formscrx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )crx_append crx_lift +
+

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ ) -
- 		-
- 		context-sensitive normal formscnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr -
- 		context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lpr

tpr ( ? ➡ ? )tpr_lift tpr_delift tpr_tpr -
- 		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_cir
unfoldrestricted parallel computationlpqs ( ? ⊢ ➤* ? )lpqs_ldrop lpqs_cpqs lpqs_lpqs +
+ context-sensitive irreducible formscir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )cir_append cir_lift
+
-
- 		-
- 		cpqs ( ? ⊢ ? ➤* ? )cpqs_lift +
+ context-sensitive reducible formscrr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )crr_append crr_lift
+
-
- 		unfold unfoldunfold ( ? ⊢ ? ⧫* ? ) -
- 		unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )

iterated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_lpss sstas_aaa sstas_sstas -
- 		-
- 		iterated static type assignmentlsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )lsstas_lift lsstas_aaa lsstas_lsstas
static typingstratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_lpss ssta_aaa ssta_ssta -
- 		local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba

local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba -
- 		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_da aaa_ssta aaa_aaa

atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_lpss aaa_aaa -
- 		stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ssta

parametersshsd -
- 		local env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⊑ ? )lsubd_da lsubd_lsubd
substitutionparallel substitutionlpss ( ? ⊢ ▶* ? )lpss_ldrop lpss_cpss lpss_lpss +
+ degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_da
+
+
+ parametersshsd
cpss ( ? ⊢ ? ▶* ? )cpss_lift +
substitutionrestricted local env. ref.lsubr ( ? ⊑ ? )lsubr_lsubr
iterated structural successor for closuresfsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )fsups_fsups -
- 		fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )fqus_fqus

fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )fsupp_fsupp -
- 		fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )fqup_fqup

-
-

-
-

-
-
gr2 ( @⦃?,?⦄ ≡ ? ) gr2_plus ( ? + ? ) gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2 -
- 		gr2_gr2
relocation structural successor for closuresfsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) -
- 		-
- 		-
- 		fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )

-
-
basic local env. slicing ldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_lpx_sn ldrop_lbotr ldrop_ldrop -
- 		-
- 		-
-
-
- 		local env. ref. for substitutionlsubr ( ? ⊑[?,?] ? )(lsubr_lsubr)lsubr_lbotr ( ⊒[?,?] ? )ldrop_append ldrop_lpx_sn ldrop_ldrop

-
-

-
-
grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf) -
- 		pointwise extension of a relationlpx_snlpx_sn_tc lpx_sn_lpx_sn

-
-
closures cl_shift ( ? @@ ? )cl_weight ( ♯{?,?} ) -
- 		cl_weight ( ♯{?,?,?} )

-
-
lenv lenv_weight ( ♯{?} ) lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_sn lenv_px_bilenv_append ( ? @@ ? )
@@ -1319,10 +1080,7 @@ term term_weight ( ♯{?} ) term_simple ( 𝐒⦃?⦄ )term_vector -
- 		term_vector
@@ -1338,9 +1096,6 @@
-
-

-
-