lambdadelta version 2

+
+

- - - - - - - - - - - - - - - - - - - + + + - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - + + + + - - - - - - + + + - + + + + + + + - - - - - - - - - - - - - - -

domain

block

leader

applicator (with âÎ¸)*

reduction

âÎ¶ *

reference *

{X | Î â¢ X : W}

local typed abstraction *

Î â¢ +Î»W

âV

âÎ²

+ home +

+ news +

+ specification +

local typed declaration **

Î â¢ -Î»W

âV

âÎ²

global typed declaration ***

Î â¢ pÎ»W

+ documentation +

+ implementation +

native type annotation *

Î â¢ âW

yes

{X | Î â¢ X = V}

local abbreviation *

Î â¢ +Î´V

local âÎ´

yes

+ foreword +

+ milestones +

+ version 2 +

(background - core - applications)

local definition **

Î â¢ -Î´V

local âÎ´

+ version 2 +

+ library +

(static LDDL directory)

+ citations +

+ visibility +

+ version 1 +

(background - core)

(static HELM directory)

+ version 1 +

+ helena +

global definition ***

Î â¢ pÎ´V

global âÎ´

sort ****

Î â¢ âk

* In terms only. + +

Summary of the Specification [spacer]

Here is a numerical account of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].

- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +

category

objects

sizes

files

277

characters

420332

nodes

1233320

sizes

files

360

characters

437272

nodes

1935835

propositions

theorems

lemmas

857

total

944

propositions

theorems

130

lemmas

1303

total

1433

concepts

declared

defined

total

129

concepts

declared

defined

total

143

Stage "B"

- In progress. + Ongoing. Context-sensitive subject equivalence for native type assignment.

Stage "A": "Extending the Applicability Condition"

+ 2014 October 28. + Î»Î´ version 2A is released. +

- In progress. - Closure of context-sensitive extended computation - for native validity. + 2014 September 9. + Iterated static type assignment defined (more elegantly) + as a primitive notion. +

+ 2014 June 18. + Preservation of stratified native validity + for context-sensitive computation on terms. +

+ 2014 June 9. + Strong qrst-normalization + for simply typed terms.

- 2013 August 7. + 2014 April 16. + Lazy equivalence on local environments + added as q-step to rst-computation on closures + (anniversary milestone). +

+ 2014 January 20. + Parametrized slicing of local environments + comprises both versions of this operation + (one from basic_1, the other used in basic_2 till now). +

+ 2013 August 7. Passive support for global environments.

- 2013 July 27. - Reaxiomatized Î²-reductum as in extended Î²-reduction + 2013 July 27. + Reaxiomatized Î²-reductum as in rt-reduction.

- 2013 July 20. - Context-sensitive extended strong normalization + 2013 July 20. + Context-sensitive strong rt-normalization for simply typed terms.

- 2013 April 16. + 2013 April 16. Reaxiomatized substitution and reduction commute with respect to subclosure (anniversary milestone).

- 2013 March 16. + 2013 March 16. Mutual recursive preservation of stratified native validity - for hyper computation on closures. + for rst-computation on closures.

- 2012 October 16. + 2012 October 16. Confluence for context-free parallel reduction on closures.

- 2012 July 26. - Term binders polarized to control Î¶-reduction. + 2012 July 26. + Term binders polarized to control Î¶-reduction (not released).

- 2012 April 16. + 2012 April 16. Context-sensitive subject equivalence for atomic arity assignment (anniversary milestone).

- 2012 March 15. + 2012 March 15. Context-sensitive strong normalization for simply typed terms.

- 2012 January 27. + 2012 January 27. Support for abstract candidates of reducibility.

- 2011 September 21. + 2011 September 21. Confluence for context-sensitive parallel reduction on terms.

- 2011 September 6. + 2011 September 6. Confluence for context-free parallel reduction on terms.

- 2011 April 17. + 2011 April 17. Specification starts.

Logical Structure of the Specification

The source files are grouped in planes and components - according to the following table. - A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +

Logical Structure of the Specification [spacer]

This table reports the specification's components and their planes.

- - - - + + + + + + + + + + + + + + + + - - - - - - - + + + + + + + + + + + + - - + - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - + + + - - - - - - - + + + - - - - - - - + + + + - - - - - + + + - - - - - - - + + + - - - - - - + + + - - + + + + + + + - - - + + + - - - - - - - + + + - - - - - + + + - - - - - - - + + + + - - - - - + + - - + + + + - - - - - - - - - - + + - - - - - - + + + - - - - - - - + + + + - - - - - - + + + + + - + + + + + - + + - - - + + + - - - - - - + + + - - - - - - - + + + - - + + + + + + + - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - - + + + - - - - - + + + - - + + + + - - - - + + + + + - + - + + + + + - - - - + + + + + + - - - - - - + + + - - - - - - + + + - - - - - - - + + + + - - - - - - + + + + - + + + + + - - - - + + + + + + - - + - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + + + + + + + + + - - + - - - - + + - - - + + + - - - - + + + + + + + - + - - - - + + - - - - - - + + + + + + + + + + + - - + + + - + + + + - - - + + + - - + + + + + - - - - - - - - - - - + + + + + - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - + + - - - - - - - - + + + + - - - - - - + + + + - - - - + - - - - - - + + - -

component	plane	files	+	component	plane	files	+ +	+ +	+ +
examples	terms with special features	ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta	+ +	+ +	+ +
+	+	+		+		+
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? Â¡â[?,?] ? )	lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv	+	dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? â«Â¡[?,?] ? )	lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv	+ +	+ +
+ +	stratified native validity	shnv ( â¦?,?â¦ â¢ ? Â¡[?,?,?] )	+ +		+
+	+ +		stratified native validity	snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )	snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs	+	snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )	snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve		+
equivalence	decomposed extended equivalence	cpes ( â¦?,?â¦ â¢ ? â¢â¬[?,?] ? )	cpes_cpds	+	equivalence	decomposed rt-equivalence	scpes ( â¦?,?â¦ â¢ ? â¢â¬[?,?,?,?] ? )	scpes_aaa scpes_cpcs scpes_scpes		+
+		context-sensitive equivalence	cpcs ( â¦?,?â¦ â¢ ? â¬* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs	+	context-sensitive equivalence	cpcs ( â¦?,?â¦ â¢ ? â¬* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs		+
conversion	context-sensitive conversion	cpc ( â¦?,?â¦ â¢ ? â¬ ? )	cpc_cpc	+	conversion	context-sensitive conversion	cpc ( â¦?,?â¦ â¢ ? â¬ ? )	cpc_cpc		+
computation	context-sensitive extended evaluation	cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )	+	computation	evaluation for context-sensitive rt-reduction	cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )		+		+
+		context-sensitive evaluation	cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )	cpre_cpre	+	evaluation for context-sensitive reduction	cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )	cpre_cpre		+
+		strongly normalizing "big tree" computation	fsb ( â¦?,?â¦ â¢ â¦¥[?,?] ? )	fsb_alt ( â¦?,?â¦ â¢ â¦¥â¦¥[?,?] ? )	fsb_csx	+	strongly normalizing qrst-computation	fsb ( â¦¥[?,?] â¦?,?,?â¦ )	fsb_alt ( â¦¥â¦¥[?,?] â¦?,?,?â¦ )	fsb_aaa fsb_csx
+		strongly normalizing extended computation	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_tstc_vector csx_aaa	+	strongly normalizing rt-computation	lcosx ( ? â¢ ~â¬*[?,?,?] ? )	lcosx_cpx		+
+		+		csx ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )	csx_lift csx_lpx	+	lsx ( ? â¢ â¬*[?,?,?,?] ? )	lsx_alt ( ? â¢ â¬â¬*[?,?,?,?] ? )	lsx_drop lsx_lpx lsx_lpxs llsx_csx
+		"big tree" parallel computation	fpbr ( â¦?,?,?â¦ ââ¥[?,?] â¦?,?,?â¦ )	fpbr_fpbr	+		+	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_tsts_vector csx_aaa	+ +
+		+	+ +	csx ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )	csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs	+ +
	fpbg ( â¦?,?,?â¦ >[?,?] â¦?,?,?â¦ )	fpbg_lift fpbg_fpbg	+	parallel qrst-computation	fpbg ( â¦?,?,?â¦ >â¡[?,?] â¦?,?,?â¦ )	fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg		+
+		+		fpbs ( â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )	fpbs_alt ( â¦?,?,?â¦ â¥â¥[?,?] â¦?,?,?â¦ )	fpbs_lift fpbs_fpbs	+	fpbs ( â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )	fpbs_alt ( â¦?,?,?â¦ â¥â¥[?,?] â¦?,?,?â¦ )	fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
+		decomposed extended computation	cpds ( â¦?,?â¦ â¢ ? â¢â¡[?,?] ? )	cpds_lift cpds_aaa cpds_cpds	+	decomposed rt-computation	scpds ( â¦?,?â¦ â¢ ? â¢â¡[?,?,?] ? )	scpds_lift scpds_aaa scpds_scpds		+
+		context-sensitive extended computation	lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )	lpxs_alt ( â¦?,?â¦ â¢ â¡â¡*[?,?] ? )	lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs	+	context-sensitive rt-computation	lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )	lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs	+ +
+		+		cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )	cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs	+	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		context-sensitive computation	lprs ( â¦?,?â¦ â¢ â¡* ? )	lprs_alt ( â¦?,?â¦ â¢ â¡â¡* ? )	lprs_ldrop lprs_cprs lprs_lprs	+
+		+		cprs ( â¦?,?â¦ â¢ ? â¡* ?)	cprs_lift cprs_cprs	+	cprs ( â¦?,?â¦ â¢ ? â¡* ?)	cprs_lift cprs_cprs		+
+		local env. ref. for abstract candidates of reducibility	lsubc ( ? â¢ ? â[?] ? )	lsubc_ldrop lsubc_ldrops lsubc_lsuba	+	local env. ref. for generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drop lsubc_drops lsubc_lsuba		+
+		support for abstract computation properties	acp	acp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	acp_aaa	+	support for generic computation properties	gcp	gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
reduction	"big tree" parallel reduction	fpbc ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpbc_lift	- -	+	reduction	parallel qrst-reduction	fpbq ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )	fpbq_alt ( â¦?,?,?â¦ â½â½[?,?] â¦?,?,?â¦ )	fpbq_lift fpbq_aaa
+	+ +	+ +	fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpb_lift fpb_lleq fpb_fleq	+ +		+
	fpb ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )	fpb_lift	+	normal forms for context-sensitive rt-reduction	cnx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	cnx_lift cnx_crx cnx_cix		+
+		context-sensitive extended normal forms	cnx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cnx_lift cnx_crx cnx_cix	+	context-sensitive rt-reduction	lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )	lpx_drop lpx_frees lpx_lleq lpx_aaa		+
+		context-sensitive extended reduction	lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )	lpx_ldrop lpx_aaa	+		+	cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix	+ +
+		+	irreducible forms for context-sensitive rt-reduction	cix ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	cix_lift	+ +	+ +
	cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpx_lift cpx_cix	+	reducible forms for context-sensitive rt-reduction	crx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	crx_lift		+
+		context-sensitive extended irreducible forms	cix ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cix_append cix_lift	+	normal forms for context-sensitive reduction	cnr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	cnr_lift cnr_crr cnr_cir		+
+		context-sensitive extended reducible forms	crx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	crx_append crx_lift	+	context-sensitive reduction	lpr ( â¦?,?â¦ â¢ â¡ ? )	lpr_drop lpr_lpr		+
+		context-sensitive normal forms	cnr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cnr_lift cnr_crr cnr_cir	+		+	cpr ( â¦?,?â¦ â¢ ? â¡ ? )	cpr_lift cpr_llpx_sn cpr_cir	+ +
+		context-sensitive reduction	lpr ( â¦?,?â¦ â¢ â¡ ? )	lpr_ldrop lpr_lpr	+	irreducible forms for context-sensitive reduction	cir ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	cir_lift		+
+	+ +	reducible forms for context-sensitive reduction	crr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	crr_lift		+		cpr ( â¦?,?â¦ â¢ ? â¡ ? )	cpr_lift cpr_cir	+
unfold	unfold	unfold ( â¦?,?â¦ â¢ ? â§«* ? )		+	+ +
+	+ +	iterated static type assignment	lstas ( â¦?,?â¦ â¢ ? â¢*[?,?] ? )	lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas	+ +		context-sensitive irreducible forms	cir ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cir_append cir_lift	+
static typing	local env. ref. for degree assignment	lsubd ( ? â¢ ? â«âª[?,?] ? )	lsubd_da lsubd_lsubd		+
+		context-sensitive reducible forms	crr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	crr_append crr_lift	+	degree assignment	da ( â¦?,?â¦ â¢ ? âª[?,?] ? )	da_lift da_aaa da_da		+
unfold	unfold	unfold ( â¦?,?â¦ â¢ ? â§«* ? )	+		+	parameters	sh	sd		+
+		iterated static type assignment	lsstas ( â¦?,?â¦ â¢ ? â¢*[?,?,?] ? )	lsstas_alt ( â¦?,?â¦ â¢ ? â¢â¢*[?,?,?] ? )	lsstas_lift lsstas_aaa lsstas_lsstas	+	local env. ref. for atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_aaa lsuba_lsuba	+ +
static typing	local env. ref. for atomic arity assignment	lsuba ( ? â¢ ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba	+		+	atomic arity assignment	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa	+ +
+	+ +	restricted local env. ref.	lsubr ( ? â« ? )	lsubr_lsubr	+ +		atomic arity assignment	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_lift aaa_lifts aaa_da aaa_ssta aaa_aaa	+
multiple substitution	lazy equivalence	fleq ( â¦?,?,?â¦ â¡[?] â¦?,?,?â¦ )	fleq_fleq		+
+	+ +		stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )	ssta_lift ssta_ssta	+	lleq ( ? â¡[?,?] ? )	lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq		+
+		local env. ref. for degree assignment	lsubd ( ? â¢ ? âªâ ? )	lsubd_da lsubd_lsubd	+	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		+
+		degree assignment	da ( â¦?,?â¦ â¢ ? âª[?,?] ? )	da_lift da_da	+	pointwise union for local environments	llor ( ? â[?,?] ? â¡ ? )	llor_alt llor_drop		+
+		parameters	sh	sd	+	context-sensitive exclusion from free variables	frees ( ? â¢ ? Ïµ ð*[?]â¦?â¦ )	frees_append frees_lreq frees_lift		+
substitution	restricted local env. ref.	lsubr ( ? â ? )	lsubr_lsubr	+	+ +	context-sensitive multiple rt-substitution	cpys ( â¦?,?â¦ â¢ ? â¶*[?,?] ? )	cpys_alt ( â¦?,?â¦ â¢ ? â¶â¶*[?,?] ? )	cpys_lift cpys_cpys	+ +
+ +	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_alt fqus_fqus		+
+	+ +		iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_alt fqus_fqus	+	fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_fqup		+
+		+	iterated local env. slicing	drops ( â¬*[?,?] ? â¡ ? )	drops_drop drops_drops		fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_fqup	+		+
+ +	generic term relocation	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lift_vector	+ +
+	+ +		generic local env. slicing	ldrops ( â©*[?] ? â¡ ? )	ldrops_ldrop ldrops_ldrops	+	lifts ( â¬*[?] ? â¡ ? )	lifts_lift lifts_lifts		+
+		generic term relocation	lifts_vector ( â§*[?] ? â¡ ? )	lifts_lift_vector	+	support for multiple relocation	mr2 ( @â¦?,?â¦ â¡ ? )	mr2_plus ( ? + ? )	mr2_minus ( ? â ? â¡ ? )	mr2_mr2
substitution	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )		+
+	+ +	+ +	fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )		+	+ +	+ +
	lifts ( â§*[?] ? â¡ ? )	lifts_lift lifts_lifts	+	global env. slicing	gget ( â¬[?] ? â¡ ? )	gget_gget		+
+	+ +	context-sensitive ordinary rt-substitution	cpy ( â¦?,?â¦ â¢ ? â¶[?,?] ? )	cpy_lift cpy_nlift cpy_cpy	+ +		support for generic relocation	gr2 ( @â¦?,?â¦ â¡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? â ? â¡ ? )	gr2_gr2
relocation	structural successor for closures	fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )	+	+ +	local env. ref. for rt-substitution	lsuby ( ? â[?,?] ? )	lsuby_lsuby	+ +
+		global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop	+	pointwise extension of a relation	lpx_sn	lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn		+
+		basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx_sn ldrop_ldrop	+	basic local env. slicing	drop ( â¬[?,?,?] ? â¡ ? )	drop_append drop_lreq drop_drop		+
+		basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	+	basic term relocation	lift_vector ( â¬[?,?] ? â¡ ? )	lift_lift_vector		+
+		+		lift ( â§[?,?] ? â¡ ? )	lift_lift	+	lift ( â¬[?,?] ? â¡ ? )	lift_neq lift_lift		+
grammar	pointwise extension of a relation	lpx_sn	lpx_sn_tc lpx_sn_lpx_sn	+	grammar	equivalence for local environments	lreq ( ? â©¬[?,?] ? )	lreq_lreq		+
+		same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector	+	same top term structure	tsts ( ? â ? )	tsts_tsts tsts_vector		+
+		closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?,?} )	+	closures	cl_weight ( â¯{?,?,?} )	cl_restricted_weight ( â¯{?,?} )		+
+		internal syntax	genv	+	internal syntax	genv		+		+
+		+		lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )	lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )
+		+		term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector	term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector ( â¶?.? )
+		+		item	+	item		+		+
+		external syntax	aarity	+	external syntax	aarity		+		+

- -

Physical Structure of the Specification

The source files are grouped in directories, - one for each component. -

@@ -1178,6 +1384,6 @@

Last update: Sat, 26 Oct 2013 19:48:51 +0200

- +

Last update: Wed, 02 Sep 2015 17:59:07 +0200