X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=951778d1e289212b14d9d995b7823c31330dec76;hb=1e89c373698e2b5e55661291f25dc5238e9f13fd;hp=e79d3468bea28bbf5373ecd887404bead7c5ecc6;hpb=e1f8310bce558bdf2c0bd24666b6e1bb1794e10c;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index e79d3468b..a281ef3ab 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,888 @@ - + - - - - - - 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




sizesfiles225characters423665nodes1282212
propositionstheorems82lemmas984total1066
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-01-28T19:34:41+01:00
- +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+
rt-transitiont-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_cpx +
+ 		+
+
+
+ 		uncounted context-sensitive rt-transitionlfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa +
+ 		+
+
+
+ 		+
+ 		cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_lsubr +
+ 		+
+
+
+ 		counted context-sensitive rt-transitioncpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr +
+ 		+
+
static typingparametersshsd +
+ 		+
+
+
+ 		restricted ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba +
+ 		+
+
+
+ 		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfeq aaa_aaa +
+ 		+
+
+
+ 		equivalence for closures on referred entriesffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )ffeq_freq +
+ 		+
+
+
+ 		equivalence for local environments on referred entrieslfeq ( ? ≡[?] ? )lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq +
+ 		+
+
+
+ 		generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs +
+ 		+
+
+
+ 		restricted ref. for context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_frees +
+ 		+
+
+
+ 		context-sensitive free variablesfrees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_weight frees_lreq 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_lifts +
+ 		+
+
+
+ 		ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq +
+ 		+
+
+
+ 		generic entrywise extensionlexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs +
+ 		+
+
grammarappend for local environmentsappend ( ? @@ ? )append_length +
+ 		+
+
+
+ 		context-sensitive equivalences for termsceqceq_ceq +
+ 		+
+
+
+ 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector +
+ 		+
+
+
+ 		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) +
+ 		+
+
+
+ 		internal syntaxgenv +
+ 		+
+ 		+
+
+
+ 		+
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| ) +
+
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+ 		+
+ 		item +
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+ 		+
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 21 Jan 2017 15:35:26 +0100
+