X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=4ae950012685910fb47fd74ea7401ba4f3706880;hb=aeb003ab531d9b9faffd46c47204b564009063cf;hp=0bd2b8a1e03b769b355f55478d394263972f88bd;hpb=baba23b670cb20eb478975fa9cb419c7ae58f7bc;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0bd2b8a1e..4ae950012 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,969 @@ - + - - - - - - lambdadelta version 2 - - - - + + + + + + \lambda\delta home page + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" + +
+ + [\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 and its timeline.
-
categoryobjects




sizesfiles228characters430859nodes1197040
propositionstheorems82lemmas1004total1086
conceptsdeclared43defined76total119
- + +
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes.
-
[Spacer]

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

Last update: 2013-02-06T21:56:05+01:00
- +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
rt-conversioncontext-sensitive r-conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )cpc_cpc
rt-computationuncounted context-sensitive rt-computationlfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs
+
+ 		+
+ 		cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_aaa cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transitionuncounted rst-transitionfpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )fpbq_aaa
+
+ 		+
+ 		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lfdeq
+
+ 		t-bound context-sensitive rt-transitionlfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
+
+ 		+
+ 		cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) +
+
+
+ 		+
+ 		cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )cpr_drops
+
+ 		+
+ 		cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
+
+ 		uncounted context-sensitive rt-transitioncnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops cnx_cnx
+
+ 		+
+ 		lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx
+
+ 		+
+ 		cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) +
+
+
+ 		+
+ 		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 ( ? ⦻**[?,?] ? )tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_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_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
+
+ 		generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
+
+ 		context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_lsubr lsubf_frees lsubf_lsubf
+
+ 		+
+ 		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_ext2 drops_lexs drops_lreq drops_drops
+
+ 		generic relocationlifts_bind ( ⬆*[?] ? ≡ ? )lifts_weight_bind lifts_lifts_bind
+
+ 		+
+ 		lifts_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
+
+ 		head equivalence for termstheq ( ? ⩳[?,?] ? )theq_simple theq_tdeq theq_theq theq_simple_vector
+
+ 		degree-based equivalencetdeq_ext ( ? ≡[?,?] ? ) ( ? ⊢ ? ≡[?,?] ? ) +
+
+
+ 		+
+ 		tdeq ( ? ≡[?,?] ? )tdeq_tdeq
+
+ 		closurescl_weight ( ♯{?,?,?} ) +
+
+
+ 		+
+ 		cl_restricted_weight ( ♯{?,?} ) +
+
+
+ 		global environmentsgenv +
+
+
+ 		local environmentslenv_ext2 +
+
+
+ 		+
+ 		lenv_length ( |?| ) +
+
+
+ 		+
+ 		lenv_weight ( ♯{?} ) +
+
+
+ 		+
+ 		lenv +
+
+
+ 		binders for local environmentsext2ext2_ext2
+
+ 		+
+ 		bindbind_weight
+
+ 		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, 25 Oct 2017 21:44:35 +0200
+