X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=eb181a3ee3f03ecdb06c2591641e3997f9c7a045;hb=cc072ef7058246bbc0deaf3e44a75b0e5977df65;hp=3955a057459b0ef7f4c297e492f4c705c749a301;hpb=65c5a379db69f0df0c803f4b24bb3219c9da752a;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3955a0574..eb181a3ee 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,1374 @@ - + - - - - - + + + + + lambdadelta version 2 - - - - + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
+
+ [Spacer] +
+
System's Syntax and Behavior
+
This is a summary of the "block structure" of the System's syntactic items and reductions.
-
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i

local typed declaration **Γ ⊢ -λWⓐV→βno#i

global typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i

local definition **Γ ⊢ -δVnolocal →δno#i

global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
* In terms only. - ** In terms and local environments only. +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i
+
+ 		local typed declaration **Γ ⊢ -λWⓐV→βno#i
+
+ 		global typed declaration ***Γ ⊢ pλWnonono$p
+
+ 		native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i
+
+ 		local definition **Γ ⊢ -δVnolocal →δno#i
+
+ 		global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
+
+
* In terms only. + ** In terms and local environments only. *** In global environments only. - **** Sort level k in terms only. + **** Sort level k in terms only.
- -
Summary of the Specification
-
Here is a numerical acount of the specification's contents + +
Summary of the Specification
+
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles252characters483454nodes1296744
propositionstheorems85lemmas1119total1204
conceptsdeclared46defined82total128
-
  • In progress. +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    categoryobjects +
    +     		+
    +     		+
    +     		+
    +     		+
    +
    sizesfiles252characters483453nodes +
    propositionstheorems85lemmas1119total1204
    conceptsdeclared46defined82total128
    +
    +
      +
    • + In progress. Context-sensitive subject equivalence - for native type assignment. -
    -
    • In progress. + for native type assignment. +
      • +
    +
      +
    • + In progress. Closure of extended context-sensitive computation - for native validity. -
    -
    • In progress. + for native validity. +
      • +
    +
      +
    • + In progress. Extended context-sensitive strong normalization - for simply typed terms. -
    -
    • 2012 October 16. + for simply typed terms. +
      • +
    +
      +
    • + 2012 October 16. Confluence for context-free parallel reduction on closures. -
    -
    • 2012 July 26. +
      • +
    +
      +
    • + 2012 July 26. Term binders polarized to control ζ reduction. -
    -
    • 2012 April 16. +
      • +
    +
      +
    • + 2012 April 16. Context-sensitive subject equivalence - for atomic arity assignment - (anniversary milestone). -
    -
    • 2012 March 15. + for atomic arity assignment + (anniversary milestone). +
      • +
    +
      +
    • + 2012 March 15. Context-sensitive strong normalization - for simply typed terms. -
    -
    • 2012 January 27. + for simply typed terms. +
      • +
    +
      +
    • + 2012 January 27. Support for abstract candidates of reducibility. -
    -
    • 2011 September 21. +
      • +
    +
      +
    • + 2011 September 21. Confluence for context-sensitive parallel reduction on terms. -
    -
    • 2011 September 6. +
      • +
    +
      +
    • + 2011 September 6. Confluence for context-free parallel reduction on terms. -
    -
    • 2011 April 17. +
      • +
    +
      +
    • + 2011 April 17. Specification starts. -
    +
    • +
-
Logical Structure of the Specification
-
The source files are grouped in planes and components +
Logical Structure of the Specification
+
The source files are grouped in planes and components according to the following table. A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).
-
componentplanefiles



dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⊩:⊑[?] ? )lsubsv_ldroplsubsv_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


equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs




fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs



local env. ref. for context-sensitive equivalencelsubse ( ? ⊢•⊑[?] ? )lsubse_ldrop lsubse_ssta lsubse_cpcs



context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs


conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc




fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc



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


computationfocalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs




fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs



"big tree" parallel computationyprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )yprs_yprsygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )ygt_ygt

decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs



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



strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa




csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr


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



context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs



tprs ( ? ➡* ?)tprs_lift tprs_tprs



local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba



support for abstract computation propertiesacpacp_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_lfpr



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



"big tree" parallel reductionypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )



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



context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr



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

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




context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr




tpr ( ? ➡ ? )tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr


unwinditerated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas


static typinglocal env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_lsubss



stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa



parametersshsd


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



inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift


partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn



ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx




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

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



iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups




frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp



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




lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts



support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps



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



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



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


restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )




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




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


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



same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector



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



internal syntaxgenv





lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi


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


item




external syntaxaarity



+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+ 		+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⊩:⊑[?] ? )lsubsv_ldroplsubsv_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 +
+ 		+
+ 		+
+
equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs +
+ 		+
+ 		+
+
+
+ 		+
+ 		fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs +
+ 		+
+ 		+
+
+
+ 		local env. ref. for context-sensitive equivalencelsubse ( ? ⊢•⊑[?] ? )lsubse_ldrop lsubse_ssta lsubse_cpcs +
+ 		+
+ 		+
+
+
+ 		context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs +
+ 		+
+ 		+
+
conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc +
+ 		+
+ 		+
+
+
+ 		+
+ 		fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc +
+ 		+
+ 		+
+
+
+ 		context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc +
+ 		+
+ 		+
+
computationfocalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs +
+ 		+
+ 		+
+
+
+ 		+
+ 		fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs +
+ 		+
+ 		+
+
+
+ 		"big tree" parallel computationyprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )yprs_yprsygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )ygt_ygt +
+
+
+ 		decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs +
+ 		+
+ 		+
+
+
+ 		weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe +
+ 		+
+ 		+
+
+
+ 		strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa +
+ 		+
+ 		+
+
+
+ 		+
+ 		csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr +
+ 		+
+
+
+ 		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 +
+ 		+
+ 		+
+
+
+ 		context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs +
+ 		+
+
+
+ 		+
+ 		tprs ( ? ➡* ?)tprs_lift tprs_tprs +
+ 		+
+ 		+
+
+
+ 		local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba +
+ 		+
+ 		+
+
+
+ 		support for abstract computation propertiesacpacp_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_lfpr +
+ 		+
+
+
+ 		+
+ 		fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr +
+ 		+
+ 		+
+
+
+ 		"big tree" parallel reductionypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) +
+ 		+
+ 		+
+
+
+ 		context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif +
+ 		+
+ 		+
+
+
+ 		context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr +
+ 		+
+ 		+
+
+
+ 		context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append +
+
+
+ 		context-free normal formsthnf ( 𝐇𝐍⦃?⦄ ) +
+ 		+
+ 		+
+ 		+
+
+
+ 		context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr +
+ 		+
+ 		+
+
+
+ 		+
+ 		tpr ( ? ➡ ? )tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr +
+ 		+
+ 		+
+
unwinditerated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas +
+ 		+
+ 		+
+
static typinglocal env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_lsubss +
+ 		+
+ 		+
+
+
+ 		stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta +
+ 		+
+ 		+
+
+
+ 		local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba +
+ 		+
+ 		+
+
+
+ 		atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa +
+ 		+
+ 		+
+
+
+ 		parametersshsd +
+ 		+
+ 		+
+
unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift +
+ 		+
+ 		+
+
+
+ 		inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift +
+ 		+
+
+
+ 		partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn +
+ 		+
+
+
+ 		+
+ 		ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx +
+ 		+
+ 		+
+
+
+ 		+
+ 		tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss +
+
+
+ 		generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops +
+ 		+
+ 		+
+
+
+ 		iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups +
+ 		+
+ 		+
+
+
+ 		+
+ 		frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp +
+ 		+
+ 		+
+
+
+ 		generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector +
+ 		+
+ 		+
+
+
+ 		+
+ 		lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts +
+ 		+
+ 		+
+
+
+ 		support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2 +
+
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps +
+ 		+
+ 		+
+
+
+ 		global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop +
+ 		+
+ 		+
+
+
+ 		basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop +
+ 		+
+ 		+
+
+
+ 		local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? ) +
+ 		+
+
+
+ 		restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ ) +
+ 		+
+ 		+
+ 		+
+
+
+ 		basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector +
+ 		+
+ 		+
+
+
+ 		+
+ 		lift ( ⇧[?,?] ? ≡ ? )lift_lift +
+ 		+
+ 		+
+
grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf) +
+ 		+
+ 		+
+
+
+ 		same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector +
+ 		+
+ 		+
+
+
+ 		closurescl_shift ( ? @@ ? )cl_weight ( ♯{?,?} ) +
+ 		+
+ 		+
+
+
+ 		internal syntaxgenv +
+ 		+
+ 		+
+ 		+
+
+
+ 		+
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector +
+
+
+ 		+
+ 		item +
+ 		+
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+ 		+
+ 		+
+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, +
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: 2013-03-09T23:27:52+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: Mon, 11 Mar 2013 13:47:08 +0100