X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=765da98303a8e893763f1cf116374eb6bf280b96;hb=e866d78af74246133f5a14cb711a62af39308dee;hp=4ee92ddf065d71ef9bca67faea7b84c433b18471;hpb=65383ff6ec2236b0a61310b872ea4cd5fcc26fb7;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 4ee92ddf0..765da9830 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,108 +1,6 @@ - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - 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 +-->
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryobjects -
- 		-
- 		-
- 		-
- 		-
-
sizesfiles235characters225732nodes1092645
propositionstheorems61lemmas738total799
conceptsdeclared29defined66total95
-
-
Stage "B"
-
categoryobjects




sizesfiles213characters224056nodes1100545
propositionstheorems61lemmas743total804
conceptsdeclared29defined66total95
Stage "B"
-
Stage "A2": "Extending the Applicability Condition"
-
Stage "A2": "Extending the Applicability Condition"
- - - - - -
Stage "A1": "Extending the Applicability Condition"
-
Stage "A1": "Extending the Applicability Condition"
- - - - - - - - - - - - - - - - - - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
componentplanefiles -
-
rt-computationuncounted context-sensitive rt-transitioncsx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) -
-
-
- 		-
- 		csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_cnx csx_cpxs csx_csx
-
- 		-
- 		lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_fqup
-
- 		-
- 		cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transitionparallel qrst-transitionfpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) -
-
-
- 		t-bound context-sensitive rt-transitionlfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
-
- 		-
- 		cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )cpr_drops
-
- 		-
- 		cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
-
- 		uncounted context-sensitive rt-transitioncnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops
-
- 		-
- 		lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx
-
- 		-
- 		cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
-
- 		counted context-sensitive rt-transitioncpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr
iterated static typinggeneric extension on referred entrieslfxss ( ? ⦻**[?,?] ? ) -
-
static typinggeneric reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drops lsubc_lsubr lsubc_lsuba
-
- 		-
- 		gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
-
- 		-
- 		gcp -
-
-
- 		atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
-
- 		-
- 		aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
-
- 		degree-based equivalence on referred entriesffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )ffdeq_fqup ffdeq_ffdeq
-
- 		-
- 		lfdeq ( ? ≡[?,?,?] ? )lfdeq_length lfdeq_fqup lfdeq_lfdeq
-
- 		generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
-
- 		context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_frees
-
- 		-
- 		frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_drops frees_fqup frees_frees
-
- 		restricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
s-computationiterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_weight fqus_drops fqus_fqup fqus_fqus
-
- 		-
- 		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_weight fqup_drops fqup_fqup
s-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight
-
- 		-
- 		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) -
-
-
- 		-
- 		drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
-
- 		generic relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector
-
- 		-
- 		lifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_tdeq lifts_lifts
-
- 		ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq
-
- 		generic entrywise extensionlexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs
syntaxappend for local environmentsappend ( ? @@ ? )append_length
-
- 		degree-based equivalence for termsdeq ( ? ≡[?,?] ? ) deq_deq
-
- 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector
-
- 		closurescl_weight ( ♯{?,?,?} ) -
-
-
- 		-
- 		cl_restricted_weight ( ♯{?,?} ) -
-
-
- 		global environmentsgenv -
-
-
- 		local environmentslenv_length ( |?| ) -
-
-
- 		-
- 		lenv_weight ( ♯{?} ) -
-
-
- 		-
- 		lenv -
-
-
- 		termsterm_vector ( Ⓐ?.? ) -
-
-
- 		-
- 		term_simple ( 𝐒⦃?⦄ ) -
-
-
- 		-
- 		term_weight ( ♯{?} ) -
-
-
- 		-
- 		term -
-
-
- 		itemsitem_sd -
-
-
- 		-
- 		item_sh -
-
-
- 		-
- 		item -
-
-
- 		atomic aritiesaarity -
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Wed, 08 Mar 2017 22:36:31 +0100
- - +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. +
componentplanefiles
rt-computationuncounted context-sensitive rt-transitioncsx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )


csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_cnx csx_cpxs csx_csx


lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_fqup


cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transitionparallel qrst-transitionfpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )

t-bound context-sensitive rt-transitionlfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr


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


cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx

uncounted context-sensitive rt-transitioncnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops


lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx


cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs

counted context-sensitive rt-transitioncpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr
iterated static typingiterated extension on referred entriestc_lfxs ( ? ⦻**[?,?] ? )
static typinggeneric reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drops lsubc_lsubr lsubc_lsuba


gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa


gcp

atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba


aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfdeq aaa_aaa

degree-based equivalence on referred entriesffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )ffdeq_fqup ffdeq_ffdeq


lfdeq ( ? ≡[?,?,?] ? )lfdeq_length lfdeq_fqup lfdeq_lfdeq

generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs

context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_frees


frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_drops frees_fqup frees_frees

restricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
s-computationiterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_weight fqus_drops fqus_fqup fqus_fqus


fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_weight fqup_drops fqup_fqup
s-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight


fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )


drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops

generic relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector


lifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_tdeq lifts_lifts

ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq

generic entrywise extensionlexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs
syntaxappend for local environmentsappend ( ? @@ ? )append_length

degree-based equivalence for termsdeq ( ? ≡[?,?] ? ) deq_deq

same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector

closurescl_weight ( ♯{?,?,?} )


cl_restricted_weight ( ♯{?,?} )

global environmentsgenv

local environmentslenv_length ( |?| )


lenv_weight ( ♯{?} )


lenv

termsterm_vector ( Ⓐ?.? )


term_simple ( 𝐒⦃?⦄ )


term_weight ( ♯{?} )


term

itemsitem_sd


item_sh


item

atomic aritiesaarity
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100