X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e1e8448af4e74e60b2ba048f7cfdc6a484f2b5bf;hb=6ce2552192c2727eb5f7d17f52b949549e1e6ad1;hp=bbde8e1cf45d067ed3727363a9d833c9768bac5a;hpb=22d35425b8f5f7e479db3be59b73f76d77ae6711;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index bbde8e1cf..e1e8448af 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - \lambda\delta version 2 + + \lambda\delta home page @@ -19,1280 +19,1346 @@ [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 + + news + + specification +
local typed declaration **Γ ⊢ -λWⓐV→βno#i
+
global typed declaration ***Γ ⊢ pλWnonono$p
+ + documentation + + implementation +
native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i
+ + foreword + + milestones + + version 2 + (background - core - applications)
local definition **Γ ⊢ -δVnolocal →δno#i + version 2 + + library + (static LDDL directory)
+ + citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + helena +
global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
* In terms only. + +
Summary of the Specification [spacer] +
+
Here is a numerical account 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].
-
+
- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles329 characters567347nodes1610281sizesfiles360characters437272nodes1935835
propositionstheorems105lemmas1114total1219propositionstheorems130lemmas1303total1433
conceptsdeclared52defined76total128conceptsdeclared54defined89total143
-
    +
    Stage "B"
    +
    • - In progress. + Ongoing. Context-sensitive subject equivalence for native type assignment.
    -
      +
      Stage "A": "Extending the Applicability Condition"
      +
        +
      • + 2014 October 28. + λδ version 2A is released. +
        • +
      +
        +
      • + 2014 September 9. + Iterated static type assignment defined (more elegantly) + as a primitive notion. +
        • +
      +
        +
      • + 2014 June 18. + Preservation of stratified native validity + for context-sensitive computation on terms. +
        • +
      +
        +
      • + 2014 June 9. + Strong qrst-normalization + for simply typed terms. +
        • +
      +
      • - In progress. - Closure of context-sensitive extended computation - for native validity. + 2014 April 16. + Lazy equivalence on local environments + added as q-step to rst-computation on closures + (anniversary milestone).
      -
        +
        • - 2014 January 20. - Parametrized slicing for local environments + 2014 January 20. + Parametrized slicing of local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now).
        -
          +
          • - 2013 August 7. + 2013 August 7. Passive support for global environments.
          -
            +
            • - 2013 July 27. - Reaxiomatized β-reductum as in extended β-reduction + 2013 July 27. + Reaxiomatized β-reductum as in rt-reduction.
            -
              +
              • - 2013 July 20. - Context-sensitive extended strong normalization + 2013 July 20. + Context-sensitive strong rt-normalization for simply typed terms.
              -
                +
                • - 2013 April 16. + 2013 April 16. Reaxiomatized substitution and reduction commute with respect to subclosure (anniversary milestone).
                -
                  +
                  • - 2013 March 16. + 2013 March 16. Mutual recursive preservation of stratified native validity - for "big tree" computation on closures. + for rst-computation on closures.
                  -
                    +
                    • - 2012 October 16. + 2012 October 16. Confluence for context-free parallel reduction on closures.
                    -
                      +
                      • - 2012 July 26. - Term binders polarized to control ζ-reduction. + 2012 July 26. + Term binders polarized to control ζ-reduction (not released).
                      -
                        +
                        • - 2012 April 16. + 2012 April 16. Context-sensitive subject equivalence for atomic arity assignment (anniversary milestone).
                        -
                          +
                          • - 2012 March 15. + 2012 March 15. Context-sensitive strong normalization for simply typed terms.
                          -
                            +
                            • - 2012 January 27. + 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 - according to the following table. - Notation files covering the whole specification are 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.
                                  -
                                  +
                                  - - - - + + + - - - - - - - + + + + - - - - - - - - - - - - + + + + - - - - - - + + - + - - - - - - - - - - - - + + - + + + + + + + - - - - - - + + + - - + + + + - - - - - - + + + - - - - - - - + + + - - - - - - - - - - + + + + - - + + + - - - - - - - - - - + + + - - - - - + + - - - - - - - + + + - - + + + - - - - - - - - - - + + + - - - - - + + + - - - - - - - + + + + - - - - - + + - - + + + + - - - - - - - - - - + + - - - - - - + + + - - - - - - - + + + + + + + + + + + + - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - + + + - - - + + + + - - - - - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - - + + + + + - + - - - - - + + + - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - + + + + + + + - - - - - + + - - - - - - - - - - - - - - + + + - - - - - - + + + - - - - - - - + + + - - - - - + + + + + + + + + + + - - - - - + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - + + + + + - + + - - - + + + - - - - - - + + + + - - + - - - - + + - - + + + + - - - - - + + + + + + + - - - - - + + + - - - - - + + - - - - - - - - + + + + - - - - - - + + + + - - - - + - - - - - - + + - -
                                  componentplanefiles + componentplanefiles
                                  		+
                                  		+
                                  dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⊑[?,?] ? )lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv + examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta +
                                  +
                                  		+
                                  + + + +
                                  		stratified native validitysnv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs +
                                  		+
                                  equivalencedecomposed extended equivalencecpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )cpes_cpds + dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv
                                  		+
                                  +
                                  		context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs + stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )
                                  		+ +
                                  +
                                  conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc +
                                  		+
                                  computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) + snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve
                                  		+ +
                                  +
                                  equivalencedecomposed rt-equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes
                                  		+
                                  +
                                  		evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre + context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
                                  		+
                                  + conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
                                  		strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx +
                                  + computationevaluation for context-sensitive rt-reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
                                  		strongly normalizing extended computationlcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )lcosx_cpxs +
                                  		+
                                  +
                                  		+ evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
                                  		lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )lsx_ldrop lsx_cpxs lsx_csx -
                                  -                                   		+
                                  -
                                  -                                   		+
                                  		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa -
                                  -                                   		+ strongly normalizing qrst-computationfsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )fsb_aaa fsb_csx
                                  +
                                  		+ strongly normalizing rt-computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx
                                  		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lpx csx_lpxs csx_fpbs +
                                  +
                                  		"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fpns fpbg_fpbg +
                                  		+ lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx
                                  +
                                  		+
                                  		fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )fpbc_fpns fpbc_fpbs + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa
                                  		+
                                  -
                                  -                                   		+
                                  		fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_fpns +
                                  		+ csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
                                  +
                                  		+ parallel qrst-computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg
                                  		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs fpbs_ext +
                                  +
                                  		parallel computation for "big tree" normal formsfpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )fpns_fpns +
                                  		+ fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
                                  +
                                  		decomposed extended computationcpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )cpds_lift cpds_aaa cpds_cpds + decomposed rt-computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds
                                  		+
                                  +
                                  		context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + context-sensitive rt-computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs +
                                  +
                                  +
                                  		+
                                  		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs + 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
                                  		context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )lprs_ldrop lprs_cprs lprs_lprs +
                                  +
                                  		+
                                  		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs + cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs
                                  		+
                                  +
                                  		local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba + local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
                                  		+
                                  +
                                  		support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa + support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa +
                                  +
                                  reductionparallel qrst-reductionfpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa
                                  reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa + +
                                  +                                   		+
                                  +                                   		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq
                                  		+
                                  +
                                  		normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix + normal forms for context-sensitive rt-reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix
                                  		+
                                  +
                                  		context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_cpys lpx_lleq lpx_aaa + context-sensitive rt-reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa
                                  		+
                                  +
                                  		+
                                  		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lift cpx_cpys cpx_lleq cpx_cix + cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
                                  		+
                                  +
                                  		irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift + irreducible forms for context-sensitive rt-reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift
                                  		+
                                  +
                                  		reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift + reducible forms for context-sensitive rt-reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift
                                  		+
                                  +
                                  		normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir + normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir
                                  		+
                                  +
                                  		context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lpr + context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr
                                  		+
                                  +
                                  		+
                                  		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_cir + cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir
                                  		+
                                  +
                                  		irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift + irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
                                  		+
                                  +
                                  		reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift + reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift
                                  		+
                                  unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) + unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
                                  		+
                                  		+
                                  + +
                                  +                                   		iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
                                  		iterated static type assignmentlsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )lsstas_lift lsstas_aaa lsstas_lsstas +
                                  static typinglocal env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba + static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd
                                  		+
                                  +
                                  		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_da aaa_ssta aaa_aaa + degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da
                                  		+
                                  +
                                  		stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ssta + parametersshsd
                                  		+
                                  +
                                  		local env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⊑ ? )lsubd_da lsubd_lsubd + local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba
                                  		+
                                  +
                                  		degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_da + atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
                                  		+
                                  +
                                  		parametersshsd + restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
                                  		+
                                  substitutionlazy equivalence for local environmentslleq ( ? ⋕[?,?] ? )lleq_alt ( ? ⋕⋕[?,?] ? )lleq_ldrop lleq_fqus lleq_lleq lleq_ext + multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq +
                                  +
                                  + +
                                  +
                                  		contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys + lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq +
                                  +
                                  +
                                  		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )fqus_alt fqus_fqus + 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
                                  		+
                                  -
                                  -                                   		+
                                  		fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )fqup_fqup + pointwise union for local environmentsllor ( ? ⋓[?,?] ? ≡ ? )llor_alt llor_drop
                                  		+
                                  +
                                  		iterated local env. slicingldrops ( ⇩*[?,?] ? ≡ ? )ldrops_ldrop ldrops_ldrops + context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_lreq frees_lift
                                  		+
                                  +
                                  		generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector + context-sensitive multiple rt-substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys
                                  		+
                                  +
                                  +                                   		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus +
                                  +
                                  +
                                  		+
                                  		lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup
                                  		+
                                  +
                                  		support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
                                  relocationcontxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_cpy + iterated local env. slicingdrops ( ⬇*[?,?] ? ≡ ? )drops_drop drops_drops
                                  		+
                                  +
                                  		restricted local env. ref.lsubr ( ? ⊑ ? )lsubr_lsubr + generic term relocationlifts_vector ( ⬆*[?] ? ≡ ? )lifts_lift_vector
                                  		+
                                  +
                                  		local env. ref. for extended substitutionlsuby ( ? ⊑×[?,?] ? )lsuby_lsuby +
                                  		+ lifts ( ⬆*[?] ? ≡ ? )lifts_lift lifts_lifts +
                                  +
                                  +
                                  		structural successor for closuresfquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
                                  substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
                                  		+
                                  +
                                  		+
                                  		fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
                                  		+
                                  		+
                                  +
                                  		global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop + global env. slicinggget ( ⬇[?] ? ≡ ? )gget_gget
                                  		+
                                  +
                                  		basic local env. slicingldrop ( ⇩[?,?,?] ? ≡ ? )ldrop_lpx_sn ldrop_leq ldrop_ldrop + context-sensitive ordinary rt-substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy
                                  		+
                                  +
                                  		basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector + local env. ref. for rt-substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby
                                  		+
                                  + +
                                  +                                   		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
                                  		+
                                  grammarequivalence for local environmentsleq ( ? ≃[?,?] ? )leq_leq + +
                                  +                                   		basic term relocationlift_vector ( ⬆[?,?] ? ≡ ? )lift_lift_vector
                                  		+
                                  + +
                                  +
                                  		pointwise extension of a relationlpx_snlpx_sn_tc lpx_sn_lpx_sn + lift ( ⬆[?,?] ? ≡ ? )lift_neq lift_lift
                                  		+
                                  + grammarequivalence for local environmentslreq ( ? ⩬[?,?] ? )lreq_lreq
                                  		same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector +
                                  		+
                                  +
                                  +                                   		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector +
                                  +
                                  +
                                  		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) + closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} )
                                  		+
                                  +
                                  		internal syntaxgenv + internal syntaxgenv
                                  		+
                                  		+
                                  +
                                  		+
                                  		lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
                                  +
                                  		+
                                  		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vectortermterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
                                  +
                                  		+
                                  		item + item
                                  		+
                                  		+
                                  +
                                  		external syntaxaarity + external syntaxaarity
                                  		+
                                  		+
                                  - -
                                  Physical Structure of the Specification
                                  -
                                  The source files are grouped in directories, - one for each component. -
                                  -
                                  +
                                  [Spacer]
                                  @@ -1318,6 +1384,6 @@

                                  -
                                  Last update: Mon, 24 Feb 2014 19:58:07 +0100
                                  - +
                                  Last update: Wed, 02 Sep 2015 17:59:07 +0200
                                  +