X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e3a69b03a9227da834d3dc86be104bcb8dbdb824;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=3ab92f7d00d16fb9d75441d97ef771abd524b392;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3ab92f7d0..e3a69b03a 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -16,12 +16,12 @@
- [lambdadelta home] + [\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
- [Spacer] + [Spacer]

@@ -31,23 +31,23 @@ - home + home news - - documentation - - + specification - +
- +
+ + documentation + implementation @@ -57,47 +57,47 @@ - foreword + foreword milestones - - version 2 - - + version 2 - (background - core - applications) - + (background - core - applications) +
+ + version 2 + - library + helena + + + Open Symbolic Notation (OSN) - (static LDDL directory) - citations + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - (background - core) - (static HELM directory) - - helena - - -
+ library + (static LDDL directory) @@ -114,7 +114,7 @@ **** Sort level k in terms only. --> -
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -124,7 +124,7 @@ category - objects + units
@@ -142,31 +142,31 @@ - sizes - files - 360 - characters - 433402 - nodes - 1874778 + sizes + characters (files) + 315581 (309) + nodes (objects) + 1458870 (1431) + intrinsic loss factor + 4.6 propositions theorems - 130 + 92 lemmas - 1286 + 1085 total - 1416 + 1177 - concepts - declared - 54 - defined - 89 - total - 143 + concepts + declared + 34 + defined + 93 + total + 127 @@ -179,11 +179,79 @@ for native type assignment. -
Stage "A": "Extending the Applicability Condition"
+
Stage "A2": "Extending the Applicability Condition"
+
    +
  • + 2017 October 17. + Exclusion binder in local environments. + Syntactic component updated: + syntax, relocation, s_transition, s_computation, static, i_static. +
    • +
+
    +
  • + 2017 April 16. + Strong rt-normalization + for simply typed terms + (anniversary milestone). +
    • +
+
    +
  • + 2017 March 16. + First behavioral component reconstructed: + rt_transition. +
    • +
+
    +
  • + 2017 February 19. + Generic candidates of reducibility. +
    • +
+
    +
  • + 2017 January 17. + Confluence for parallel r-transition on referred entries of local environments. +
    • +
+
    +
  • + 2016 September 15. + Confluence for context-sensitive parallel r-transition on terms. +
    • +
+
    +
  • + 2016 April 16. + Syntactic component reconstructed: + syntax, relocation, s_transition, s_computation, static + (anniversary milestone). +
    • +
+
    +
  • + 2016 March 25. + Relocation with reference transforming maps (rtmap). +
    • +
+
    +
  • + 2015 October 9. + λδ version 2A2 is started. +
    • +
+
Stage "A1": "Extending the Applicability Condition"
+
    +
  • + 2015 August 27. + λδ version 2A1 appears too complex and is dismissed. +
    • +
  • 2014 October 28. - λδ version 2A is released. + λδ version 2A1 is released.
    @@ -218,7 +286,7 @@
    • 2014 January 20. - Parametrized slicing of local environments + Parametrized slicing on local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now).
      • @@ -287,7 +355,7 @@
      • 2012 January 27. - Support for abstract candidates of reducibility. + Generic candidates of reducibility.
        @@ -305,10 +373,10 @@
        • 2011 April 17. - Specification starts. + λδ version 2 is started.
        -
        Logical Structure of the Specification [spacer] +
        Logical Structure of the Specification [butterfly]
        This table reports the specification's components and their planes.
        @@ -317,222 +385,131 @@ component + section plane files - -
        - - -
        -
        - examples - terms with special features - ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta - -
        - - -
        - - -
        - + rt-conversion + context-sensitive parallel r-conversion + for terms + cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? ) + cpc_cpc - - - - -
        - - -
        - - -
        - + rt-computation + uncounted context-sensitive parallel rt-computation + refinement for lenvs + lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? ) + lsubsx_lfsx lsubsx_lsubsx - dynamic typing - local env. ref. for stratified native validity - lsubsv ( ? ⊢ ? ⫃¡[?,?] ? ) - lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv - +
        - +
        + strongly normalizing for lenvs on referred entries + lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ ) + lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx - -
        - - stratified native validity - shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) - +
        - -
        - - +
        + strongly normalizing for term vectors + csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_cnx_vector csx_csx_vector - -
        - - -
        - - snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) - snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve - +
        - +
        + strongly normalizing for terms + csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) + csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx - equivalence - decomposed rt-equivalence - scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) - scpes_aaa scpes_cpcs scpes_scpes - +
        - +
        + for lenvs on referred entries + lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) + lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs - +
        - context-sensitive equivalence - cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) - cpcs_aaa cpcs_cprs cpcs_cpcs - -
        - - -
        - - - - conversion - context-sensitive conversion - cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) - cpc_cpc - +
        + for lenvs on all entries + lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )
        - computation - evaluation for context-sensitive rt-reduction - cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) - +
        - -
        - - +
        + for terms + cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) + cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs - -
        - - evaluation for context-sensitive reduction - cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) - cpre_cpre - -
        - - -
        - + rt-transition + uncounted parallel rst-transition + for closures + fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) + fpbq_aaa
        - strongly normalizing qrst-computation - fsb ( ⦥[?,?] ⦃?,?,?⦄ ) - fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ ) - fsb_aaa fsb_csx - -
        - - -
        - strongly normalizing rt-computation - lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) - lcosx_cpx - -
        - - -
        - + proper for closures + fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ ) + fpb_lfdeq
        - -
        - - lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) - lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? ) - lsx_drop lsx_lpx lsx_lpxs llsx_csx - -
        - + context-sensitive parallel r-transition + for lenvs on referred entries + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
        - -
        - - csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csx_tsts_vector csx_aaa - -
        - - -
        - - -
        - -
        - - csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) - csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs + for binders + cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )
        @@ -541,100 +518,51 @@
        - parallel qrst-computation - fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) - fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg - -
        - - -
        - - -
        - -
        - - fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) - fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) - fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs - -
        - + for terms + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops
        - decomposed rt-computation - scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) - scpds_lift scpds_aaa scpds_scpds - -
        - - -
        - + t-bound context-sensitive parallel rt-transition + for terms + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
        - context-sensitive rt-computation - lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) - lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs - -
        - - -
        - + uncounted context-sensitive parallel rt-transition + normal form for terms + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops cnx_cnx
        - -
        - - cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) - cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs - -
        - - -
        - - -
        - context-sensitive computation - lprs ( ⦃?,?⦄ ⊢ ➡* ? ) - lprs_drop lprs_cprs lprs_lprs - -
        - - -
        - + for lenvs on referred entries + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx
        - -
        - - cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) - cprs_lift cprs_cprs - +
        + for lenvs on all entries + lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )
        @@ -643,12 +571,11 @@
        - local env. ref. for generic reducibility - lsubc ( ? ⊢ ? ⫃[?] ? ) - lsubc_drop lsubc_drops lsubc_lsuba - +
        + for binders + cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )
        @@ -657,598 +584,411 @@
        - support for generic computation properties - gcp - gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) - gcp_aaa - +
        + for terms + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq - reduction - parallel qrst-reduction - fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) - fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ ) - fpbq_lift fpbq_aaa - +
        + counted context-sensitive parallel rt-transition + for terms + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr - -
        - - -
        - - fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) - fpb_lift fpb_lleq fpb_fleq - -
        - - -
        - + iterated static typing + iterated generic extension of a context-sensitive relation + for lenvs on referred entries + tc_lfxs ( ? ⦻**[?,?] ? ) + tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs - -
        - - normal forms for context-sensitive rt-reduction - cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) - cnx_lift cnx_crx cnx_cix - -
        - - -
        - + static typing + generic reducibility + restricted refinement for lenvs + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drops lsubc_lsubr lsubc_lsuba - -
        - - context-sensitive rt-reduction - lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_drop lpx_frees lpx_lleq lpx_aaa - +
        - +
        + candidates + gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa - -
        - - +
        - cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix - +
        - + computation properties + gcp +
        - -
        - - irreducible forms for context-sensitive rt-reduction - cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) - cix_lift - -
        - - +
        + atomic arity assignment + restricted refinement for lenvs + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba - -
        - - reducible forms for context-sensitive rt-reduction - crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) - crx_lift - +
        - +
        + for terms + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa - -
        - - normal forms for context-sensitive reduction - cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ ) - cnr_lift cnr_crr cnr_cir - -
        - - +
        + degree-based equivalence + for closures on referred entries + ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ ) + ffdeq_fqup ffdeq_ffdeq - -
        - - context-sensitive reduction - lpr ( ⦃?,?⦄ ⊢ ➡ ? ) - lpr_drop lpr_lpr - +
        - +
        + for lenvs on referred entries + lfdeq ( ? ≛[?,?,?] ? ) + lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq - -
        - - -
        - - cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) - cpr_lift cpr_llpx_sn cpr_cir - -
        - - +
        + syntactic equivalence + for lenvs on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_fqup lfeq_lfeq - -
        - - irreducible forms for context-sensitive reduction - cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) - cir_lift - -
        - - +
        + generic extension of a context-sensitive relation + for lenvs on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs - -
        - - reducible forms for context-sensitive reduction - crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) - crr_lift - -
        - - +
        + context-sensitive free variables + restricted refinement for lenvs + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_lsubr lsubf_frees lsubf_lsubf - unfold - unfold - unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) - -
        - - +
        - +
        + for terms + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_drops frees_fqup frees_frees
        - iterated static type assignment - lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? ) - lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas - -
        - - -
        - + local environments + restricted refinement + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr - static typing - local env. ref. for degree assignment - lsubd ( ? ⊢ ? ⫃▪[?,?] ? ) - lsubd_da lsubd_lsubd - -
        - - -
        - + s-computation + iterated structural successor + for closures + fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) + fqus_weight fqus_drops fqus_fqup fqus_fqus
        - degree assignment - da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) - da_lift da_aaa da_da - -
        - - -
        - - -
        - parameters - sh - sd - -
        - - -
        - + proper for closures + fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) + fqup_weight fqup_drops fqup_fqup - -
        - - local env. ref. for atomic arity assignment - lsuba ( ? ⊢ ? ⫃⁝ ? ) - lsuba_aaa lsuba_lsuba - -
        - - -
        - + s-transition + structural successor + for closures + fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight - -
        - - atomic arity assignment - aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa - +
        - +
        + proper for closures + fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight - -
        - - restricted local env. ref. - lsubr ( ? ⫃ ? ) - lsubr_lsubr - -
        - - -
        - + relocation + generic slicing + for lenvs + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector - multiple substitution - lazy equivalence - fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) - fleq_fleq - -
        - - +
        + generic relocation + for binders + lifts_bind ( ⬆*[?] ? ≡ ? ) + lifts_weight_bind lifts_lifts_bind - -
        - - -
        - - lleq ( ? ≡[?,?] ? ) - lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq - +
        - +
        + for term vectors + lifts_vector ( ⬆*[?] ? ≡ ? ) + lifts_lifts_vector - -
        - - lazy pointwise extension of a relation - llpx_sn - llpx_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 - +
        - +
        + for terms + lifts ( ⬆*[?] ? ≡ ? ) + lifts_simple lifts_weight lifts_tdeq lifts_lifts - -
        - - pointwise union for local environments - llor ( ? ⋓[?,?] ? ≡ ? ) - llor_alt llor_drop - -
        - - +
        + syntactic equivalence + for lenvs on selected entries + lreq ( ? ≡[?] ? ) + lreq_length lreq_lreq - -
        - - context-sensitive exclusion from free variables - frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ ) - frees_append frees_lreq frees_lift - -
        - - +
        + generic entrywise extension + for lenvs of one contex-sensitive relation + lex ( ? ⦻[?] ? ) + lex_tc - +
        - context-sensitive multiple rt-substitution - cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) - cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) - cpys_lift cpys_cpys - +
        + for lenvs of two contex-sensitive relations + lexs ( ? ⦻*[?,?,?] ? ) + lexs_tc lexs_length lexs_lexs - -
        - - iterated structural successor for closures - fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) - fqus_alt fqus_fqus - -
        - - -
        - + syntax + append for local environments + + append ( ? @@ ? ) + append_length - -
        - - -
        - - fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) - fqup_fqup - -
        - - +
        + head equivalence for terms + + theq ( ? ⩳[?,?] ? ) + theq_simple theq_tdeq theq_theq theq_simple_vector - -
        - - iterated local env. slicing - drops ( ⬇*[?,?] ? ≡ ? ) - drops_drop drops_drops - +
        - + degree-based equivalence + + tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? ) +
        - -
        - - generic term relocation - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector - +
        - +
        + + tdeq ( ? ≛[?,?] ? ) + tdeq_tdeq - -
        - - -
        - - lifts ( ⬆*[?] ? ≡ ? ) - lifts_lift lifts_lifts - +
        - + closures + + cl_weight ( ♯{?,?,?} ) +
        - +
        - support for multiple relocation - mr2 ( @⦃?,?⦄ ≡ ? ) - mr2_plus ( ? + ? ) - mr2_minus ( ? ▭ ? ≡ ? ) - mr2_mr2 - - - substitution - structural successor for closures - fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) - fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) - +
        - + + cl_restricted_weight ( ♯{?,?} ) +
        - -
        - - -
        - - fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - -
        - - +
        - + global environments + + genv +
        - -
        - - global env. slicing - gget ( ⬇[?] ? ≡ ? ) - gget_gget - -
        - - +
        + local environments + + ceq_ext + ceq_ext_ceq_ext - +
        - context-sensitive ordinary rt-substitution - cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) - cpy_lift cpy_nlift cpy_cpy - +
        - + + cext2 +
        - +
        - local env. ref. for rt-substitution - lsuby ( ? ⊆[?,?] ? ) - lsuby_lsuby - +
        - + + lenv_length ( |?| ) +
        - +
        - pointwise extension of a relation - lpx_sn - lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn - +
        - + + lenv_weight ( ♯{?} ) +
        - +
        - basic local env. slicing - drop ( ⬇[?,?,?] ? ≡ ? ) - drop_append drop_lreq drop_drop - +
        - + + lenv +
        - -
        - - basic term relocation - lift_vector ( ⬆[?,?] ? ≡ ? ) - lift_lift_vector - -
        - - +
        + binders for local environments + + ext2 + ext2_tc ext2_ext2 - -
        - - -
        - - lift ( ⬆[?,?] ? ≡ ? ) - lift_neq lift_lift - +
        - +
        + + bind + bind_weight - grammar - equivalence for local environments - lreq ( ? ⩬[?,?] ? ) - lreq_lreq - +
        + terms + + term_vector ( Ⓐ?.? )
        @@ -1257,12 +997,11 @@
        - same top term structure - tsts ( ? ≂ ? ) - tsts_tsts tsts_vector - +
        + + term_simple ( 𝐒⦃?⦄ )
        @@ -1271,12 +1010,11 @@
        - closures - cl_weight ( ♯{?,?,?} ) - cl_restricted_weight ( ♯{?,?} ) - +
        + + term_weight ( ♯{?} )
        @@ -1285,14 +1023,11 @@
        - internal syntax - genv - -
        - - +
        + + term
        @@ -1301,40 +1036,35 @@
        - + items + + item_sd +
        - lenv - lenv_weight ( ♯{?} ) - lenv_length ( |?| ) - lenv_append ( ? @@ ? )
        - + +
        + + + item_sh +
        - term - term_weight ( ♯{?} ) - term_simple ( 𝐒⦃?⦄ ) - term_vector ( Ⓐ?.? )
        - +
        + item - -
        - - -
        -
        @@ -1343,14 +1073,9 @@
        - external syntax + atomic arities + aarity - -
        - - -
        -
        @@ -1359,7 +1084,7 @@
        - [Spacer] + [Spacer]

        @@ -1384,6 +1109,6 @@

        -
        Last update: Fri, 06 Mar 2015 17:53:24 +0100
        +
        Last update: Fri, 24 Nov 2017 21:00:01 +0100