X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=5075e40e11bcc0bf86bc321623e146c661b17625;hb=3080bf8226d155d017c5ec5c4e852d952f5b878c;hp=67fa008564be4286675b8ed904e713f3c65294ec;hpb=3fb2d167ba8463e0fa80efe42ee9be1a15e282a0;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 67fa00856..5075e40e1 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + \lambda\delta home page @@ -19,118 +19,81 @@ [lambdadelta home] -
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
+
cic:/matita/lambdadelta/basic_2/ (core λδ 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
-
+ 		+ home local typed declaration **Γ ⊢ -λWⓐV→βno#i
-
+ 		+ news global typed declaration ***Γ ⊢ pλWnonono$p
+ + documentation + + specification +
native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i + implementation +
-
+ 		+ foreword + + milestones + + version 2 + + version 2 + (background - core - applications) + library local definition **Γ ⊢ -δVnolocal →δno#i
+ + citations + + visibility + + version 1 + + version 1 +
global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono + helena +
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
-
Summary of the Specification
+ +
Summary of the Specification [spacer] +
Here is a numerical acount of the specification's contents and its timeline.
@@ -138,97 +101,157 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles262 characters527314nodes1440935sizesfiles360characters433402nodes1874774
propositionstheorems95lemmas1170total1265propositionstheorems130lemmas1286total1416
conceptsdeclared49defined87total136conceptsdeclared54defined89total143
+ +
Stage "B"
+ +
Stage "A": "Extending the Applicability Condition"
+ + + + + + + + -
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). +
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes.
- - - - + + + - - - - - - - - - - + + + + + - - - - - - - + + + + + + + - - - - - + + - - - - - - - - + + - - - - - - - + + + + - - - + + + - - - - + + + + + + - - - - - - + + + - - - - - - - - + + + - - - - - - - - + + + + - - + + + - - - - + + - + + + + - - - - - - + + - - - - - - - - + + + - - + + + - - - - + + - - - - + + + - - - - + + - + + + - - - - - - - + + + - - - - - - - + + - - - + + + - - - - - - - - - - - + + - - - - - - - + + + - - - - - - - + + + + - + + + + + + + - - - - - - + + - - - - - - - + + + - - - - - - - + + + - - - - - - - - - - - + + - - - - + + - + + + - - - - - - + + + - - - - - - - - + + + - - - - - - - - + + + - - - - - - + + - - + + - - - - - - - + + + - - - + + + - - - - - - - - - - + + + - - - - - - - + + + - - - - - - - + + + + - - - - - - - - + + + - - - - - - - + + + - - - - - - - + + + - - - - - - + + + - - - - - - - - + + + - - - - - - - + + + + - - - - - - - + + - - - - - - + + + - - - - - - - - + + + - - - + + + - - - - + + - + + + + - - + + + - - - - - - - - - - - + + - - - - - - - + + + - - - - - - + + + - - - - - - - - + + - - - - - - - - + + + + + - - - - - + + + + - - - - - - - + - - - - - - - - + + + - - - - - - - + + + - - - - - - - + + + - - - - - - + + + - - - - - - - - + + + - - - - - - - + + + - - - - - - - + + - - + + + + - - - - - + + + + + + - - - - - + + + - - + + - + + - - - - - - - - - - - - - - - - + + + + - - - - + + + + + + - - + - - - - - - - + + - + + - - @@ -1382,10 +1340,6 @@
componentplanefiles + componentplanefiles
+
-
- 		+
dynamic typing"big tree" parallel computationyprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )yprs_yprsygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )ygt_ygt + examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta +
+ 		+
+
+ + + +
"big tree" parallel reductionypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) +
+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv +
+
+
local env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⊑[?] ? )lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv + stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )
+
+
+
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_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve
+
equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs -
- 		+ equivalencedecomposed rt-equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes
+
+
+ context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs +
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
+
-
- 		local env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_cpcs + computationevaluation for context-sensitive rt-reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
+
+
-
- 		context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs +
+ evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
+
conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc +
-
- 		+ strongly normalizing qrst-computationfsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )fsb_aaa fsb_csx
+
+ strongly normalizing rt-computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx
fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc +
+

+ +
+ 		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx
+
context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc +
+ csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa
+
computationfocalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs +
+
+ csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
+
+ parallel qrst-computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg
fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs +
+

+
+ fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs +

+ decomposed rt-computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds
+
-
- 		weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe +
+ context-sensitive rt-computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
+
+
strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa +
+ cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
+
+
+ context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs
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 +
+ cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs
+
+
context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs + local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
+
-
- 		-
- 		tprs ( ? ➡* ?)tprs_lift tprs_tprs +
+ support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
+
reductionparallel qrst-reductionfpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa
+
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba +
+ fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq
+
+
support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )acp_aaa + normal forms for context-sensitive rt-reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix
+
reducibilitycontext-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr +
+ context-sensitive rt-reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa
+
-
- 		context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr +
+
+ cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
+
fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr +

+ irreducible forms for context-sensitive rt-reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift
+
+
context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif + reducible forms for context-sensitive rt-reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift
-
- 		+
-
- 		context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr +
+ normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir
+
+
context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append + context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr
+
context-free normal formsthnf ( 𝐇𝐍⦃?⦄ ) +

+
+ cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir
+
-
- 		context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr +
+ irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
+
+
+ reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift
tpr ( ? ➡ ? )tpr_lift tpr_delift tpr_tpr -
- 		-
- 		+
restricted computationrestricted parallel computationlpqs ( ? ⊢ ➤* ? )lpqs_ldrop lpqs_cpqs lpqs_lpqs + unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
+
+
-
- 		+
cpqs ( ? ⊢ ? ➤* ? )cpqs_lift + iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
-
- 		+
unwinditerated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_sstas + static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd
-
- 		+
static typingstratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta +
+ degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da
+
-
- 		local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba +
+ parametersshsd
+
-
- 		atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa +
+ local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba
+
+
parametersshsd + atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
-
- 		+
unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift +
+ restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
+
-
- 		inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift + multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq
+
+
revised parallel substitutionlpss ( ? ⊢ ▶* ? )lpss_ldrop lpss_cpss lpss_lpss +
+ lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq
+
-
- 		+
cpss ( ? ⊢ ? ▶* ? )cpss_lift + lazy pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
-
- 		+
+
partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn + pointwise union for local environmentsllor ( ? ⋓[?,?] ? ≡ ? )llor_alt llor_drop
+
+
+ context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_lreq frees_lift
ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx +
+

+ contxt-sensitive multiple rt-substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys
+
+ iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus
tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss +
+
iterated structural successor for closuresfsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )fsupp_fsupp +
+ fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup
+
-
- 		generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops +
+ iterated local env. slicingdrops ( ⬇*[?,?] ? ≡ ? )drops_drop drops_drops
+
+
generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector + generic term relocationlifts_vector ( ⬆*[?] ? ≡ ? )lifts_lift_vector
-
- 		+
-
- 		+
lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts +
+ lifts ( ⬆*[?] ? ≡ ? )lifts_lift lifts_lifts
+
-
- 		support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2 +
support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps + substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
-
- 		+
+
structural successor for closuresfsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) +
+ fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
+
+
-
- 		global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop +
+ global env. slicinggget ( ⬇[?] ? ≡ ? )gget_gget
+
-
- 		basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_lpx_sn ldrop_lbotr ldrop_ldrop +
+ contxt-sensitive ordinary rt-substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy
+
+
local env. ref. for substitutionlsubr ( ? ⊑[?,?] ? )(lsubr_lsubr)lsubr_lbotr ( ⊒[?,?] ? ) + local env. ref. for rt-substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby
+
+
basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector + pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
-
- 		+
-
- 		-
- 		lift ( ⇧[?,?] ? ≡ ? )lift_lift +
+ basic local env. slicingdrop ( ⬇[?,?,?] ? ≡ ? )drop_append drop_lreq drop_drop
+
grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf) +
+ basic term relocationlift_vector ( ⬆[?,?] ? ≡ ? )lift_lift_vector
+
+
same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector +
+ lift ( ⬆[?,?] ? ≡ ? )lift_neq lift_lift
+
+ grammarequivalence for local environmentslreq ( ? ⩬[?,?] ? )lreq_lreq
closurescl_shift ( ? @@ ? )cl_weight ( ♯{?,?} ) +
+
+
+ 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector
+
+
internal syntaxgenv + closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} )
+
+

+ internal syntaxgenv
+
+
lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_sn lenv_px_bi
-
- 		+
termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector +
lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+
item + termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )

 +
+ item
+
+
external syntaxaarity +

+ external syntaxaarity
+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
[Spacer]
@@ -1412,6 +1366,6 @@

-
Last update: Sun, 07 Apr 2013 23:37:37 +0200
+
Last update: Tue, 04 Nov 2014 16:21:23 +0100