[\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - syntax - core - applications)
version 2 helena Open Symbolic Notation (OSN)
citations visibility version 1 (background - core) (static HELM directory) version 1 library (static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category units




sizes characters (files) 272615 (243) nodes (objects) 1256612 (984) intrinsic loss factor 4.6
propositions theorems 49 lemmas 805 total 854
concepts declared 8 defined 33 total 41
Stage "B"
Stage "A"
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
component section plane files
iterated dynamic typing context-sensitive iterated native type assignment for terms ntas ( ⦃?,?⦄ ⊢ ? :[?,?,?] ? ) ( ⦃?,?⦄ ⊢ ? :[?,?] ? ) ( ⦃?,?⦄ ⊢ ? :*[?,?] ? )
dynamic typing context-sensitive native type assignment for terms nta ( ⦃?,?⦄ ⊢ ? :[?,?] ? ) ( ⦃?,?⦄ ⊢ ? :[?] ? ) ( ⦃?,?⦄ ⊢ ? :*[?] ? ) nta_drops nta_aaa nta_fsb nta_cpms nta_cpcs nta_preserve nta_preserve_cpcs nta_ind

context-sensitive native validity restricted refinement for lenvs lsubv ( ? ⊢ ? ⫃![?,?] ? ) lsubv_drops lsubv_lsubr lsubv_lsuba lsubv_cpms lsubv_cpcs lsubv_cnv lsubv_lsubv


for terms cnv ( ⦃?,?⦄ ⊢ ? ![?,?] ) ( ⦃?,?⦄ ⊢ ? ![?] ) ( ⦃?,?⦄ ⊢ ? !*[?] ) cnv_drops cnv_fqus cnv_aaa cnv_fsb cnv_cpm_trans cnv_cpm_conf cnv_cpm_tdeq cnv_cpm_tdeq_trans cnv_cpm_tdeq_conf cnv_cpms_tdeq cnv_cpms_conf cnv_cpms_tdeq_conf cnv_cpcs cnv_preserve_sub cnv_preserve
rt-equivalence context-sensitive parallel r-equivalence for terms cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? ) cpcs_drops cpcs_lsubr cpcs_aaa cpcs_cprs cpcs_lprs cpcs_cpc cpcs_cpcs
rt-conversion context-sensitive parallel eta-conversion for lenvs on all entries lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )


for binders cpce_ext ( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )


for terms cpce ( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )

context-sensitive parallel r-conversion for terms cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? ) cpc_cpc
rt-computation context-sensitive parallel r-computation for lenvs on all entries lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? ) lprs_tc lprs_ctc lprs_length lprs_drops lprs_aaa lprs_lpr lprs_lpxs lprs_cpms lprs_cprs lprs_lprs


for binders cprs_ext ( ⦃?,?⦄ ⊢ ? ➡*[?] ?)


for terms cprs ( ⦃?,?⦄ ⊢ ? ➡*[?] ?) cprs_ctc cprs_drops cprs_cpr cprs_lpr cprs_cprs

t-bound context-sensitive parallel rt-computation for terms cpms ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) cpms_drops cpms_lsubr cpms_rdeq cpms_aaa cpms_lpr cpms_cpxs cpms_fpbs cpms_fpbg cpms_cpms

unbound context-sensitive parallel rst-computation strongly normalizing for closures fsb ( ≥[?,?] 𝐒⦃?,?,?⦄ ) fsb_fdeq fsb_aaa fsb_csx fsb_fpbg


proper for closures fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) fpbg_fqup fpbg_cpxs fpbg_lpxs fpbg_fpbs fpbg_fpbg


for closures fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) fpbs_fqup fpbs_fqus fpbs_aaa fpbs_cpx fpbs_fpb fpbs_cpxs fpbs_lpxs fpbs_csx fpbs_fpbs

unbound context-sensitive parallel rt-computation refinement for lenvs on selected entries lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? ) lsubsx_lfsx lsubsx_lsubsx


strongly normalizing for lenvs on referred entries rdsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ ) rdsx_length rdsx_drops rdsx_fqup rdsx_cpxs rdsx_csx rdsx_rdsx


strongly normalizing for term vectors csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_cnx_vector csx_csx_vector


strongly normalizing for terms csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_simple csx_simple_theq csx_drops csx_fqus csx_lsubr csx_rdeq csx_fdeq csx_aaa csx_gcp csx_gcr csx_lpx csx_cnx csx_fpbq csx_cpxs csx_lpxs csx_csx


for lenvs on all entries lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? ) lpxs_length lpxs_drops lpxs_rdeq lpxs_fdeq lpxs_aaa lpxs_lpx lpxs_cpxs lpxs_lpxs


for binders cpxs_ext ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )


for terms cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_rdeq cpxs_fdeq cpxs_aaa cpxs_lpx cpxs_cnx cpxs_cpxs
rt-transition unbound parallel rst-transition for closures fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) fpbq_aaa fpbq_fpb


proper for closures fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) fpb_rdeq fpb_fdeq

context-sensitive parallel r-transition for lenvs on all entries lpr ( ⦃?,?⦄ ⊢ ➡[?] ? ) lpr_length lpr_drops lpr_fquq lpr_aaa lpr_lpx lpr_lpr


for binders cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )


for terms cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) cpr_drops cpr_cpr

t-bound context-sensitive parallel rt-transition for terms cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) cpm_simple cpm_tdeq cpm_drops cpm_lsubr cpm_fsle cpm_aaa cpm_cpx

unbound context-sensitive parallel rt-transition normal form for terms cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) cnx_simple cnx_drops cnx_cnx


for lenvs on referred entries rpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) rpx_length rpx_drops rpx_fqup rpx_fsle rpx_rdeq rpx_lpx rpx_rpx


for lenvs on all entries lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? ) lpx_length lpx_drops lpx_fquq lpx_fsle lpx_rdeq lpx_aaa


for binders cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )


for terms cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_req cpx_rdeq cpx_fdeq

bound context-sensitive parallel rt-transition for terms cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) cpg_simple cpg_drops cpg_lsubr
[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Thu, 08 Nov 2018 17:30:53 +0100