BTM

Date: Sat, 11 Mar 2017 18:32:41 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/BTM.html | 226 +- helm/www/lambdadelta/apps_2.html | 279 +- helm/www/lambdadelta/basic_1.html | 830 ++- helm/www/lambdadelta/basic_2.html | 854 ++- helm/www/lambdadelta/core.html | 7120 +++++++++++++++++++++- helm/www/lambdadelta/documentation.html | 405 +- helm/www/lambdadelta/ground_1.html | 296 +- helm/www/lambdadelta/ground_2.html | 824 ++- helm/www/lambdadelta/home.html | 240 +- helm/www/lambdadelta/implementation.html | 245 +- helm/www/lambdadelta/news.html | 366 +- helm/www/lambdadelta/osn.html | 169 +- helm/www/lambdadelta/specification.html | 348 +- 13 files changed, 11996 insertions(+), 206 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index b6c0bdac6..e63f9accc 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -1,5 +1,227 @@ -BTM

$[\lambda\delta home]$

cic:/matita/BTM/

$\lambda\delta rainbow rule$

Character classes

This table shows how the first 45 positive integers + + + + + + + + BTM + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/matita/BTM/

+ $\lambda\delta rainbow rule$ +

Character classes

This table shows how the first 45 positive integers are distributed in the four classes. -

class	contents
p		1	4	7	10	13	16	19	22	25	28	31	34	37	40	43
q		5	11	15	17	23	29	33	35	41	45
s		2	6	8	14	18	20	24	26	32	38	42	44
t		3	9	12	21	27	30	36	39

$\lambda\delta rainbow rule$

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

class	contents	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +
p	+ +	1	4	7	10	13	16	19	22	25	28	31	34	37	40	43
q	+ +	5	11	15	17	23	29	33	35	41	45	+ +	+ +	+ +	+ +	+ +
s	+ +	2	6	8	14	18	20	24	26	32	38	42	44	+ +	+ +	+ +
t	+ +	3	9	12	21	27	30	36	39	+ +	+ +	+ +	+ +	+ +	+ +	+ +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:41 +0100

+ + diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index e23bd8edd..e754a6e29 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,26 +1,283 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

$\lambda\delta rainbow rule$

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)

Contents of the Specification $\lambda\delta butterfly$

This specification comprises a collection of checked + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Contents of the Specification $\lambda\delta butterfly$ +

This specification comprises a collection of checked applications of Î»Î´ version 2. In particular it contains the components below. -

MLTT1. +

+ MLTT1. Martin-LÃ¶f's Type Theory with one universe using Î»Î´ as theory of expressions. -

Functional. +

+ Functional. The validation algorithm for Î»Î´ as implemented in Helena 0.8. -

Examples. +

+ Examples. Terms of Î»Î´ with special features. -

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents + + +

Summary of the Specification $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	1	characters	377	nodes	775
propositions	theorems	2	lemmas	1	total	3
concepts	declared	0	defined	3	total	3

2017 March 6. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	1	characters	377	nodes	779
propositions	theorems	2	lemmas	1	total	3
concepts	declared	0	defined	3	total	3

+ 2017 March 6. The Examples component is moved from the Core directory. -

2012 February 24. +

+ 2012 February 24. The Applications directory is started. -

2011 December 20. +

+ 2011 December 20. The Functional component is started inside the specification of Î»Î´ version 2. -

2011 December 12. +

+ 2011 December 12. The MLTT1 component is started. -

Logical Structure of the Specification $\lambda\delta butterfly$

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

component	plane	files
functional	reduction and type machine	rtm	rtm_step ( ? â¨ ? )
	relocation	lift ( â[?,?] ? )
examples	terms with special features	ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta

$\lambda\delta rainbow rule$

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

+ + +

Logical Structure of the Specification $\lambda\delta butterfly$ +

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + +

component	plane	files	+ +
functional	reduction and type machine	rtm	rtm_step ( ? â¨ ? )
+ +	relocation	lift ( â[?,?] ? )	+ +
examples	terms with special features	ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta	+ +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 8560a6fcf..d160de5dd 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -1,18 +1,828 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/BOLOGNA/lambdadelta/basic_1/ (core Î»Î´ version 1)

$\lambda\delta rainbow rule$

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)

Abstract Syntax and Behavior $\lambda\delta butterfly$

This is a summary of available syntactic items and reductions (block structure). -

domain	block	leader	âÎ¶ *	annotator (with âÏµ *)	applicator (with âÎ¸ *)	reference *	reduction
{X \| Î â¢ â¤}	exclusion	Î â¢ Ï	yes	no	no	no	no
{X \| Î â¢ X : W}	typed abstraction	Î â¢ Î»W	no	<W>	(V)	#i	âÎ² *
{X \| Î â¢ X = V}	abbreviation	Î â¢ Î´V	yes	no	no	#i	âÎ´
no	sort	Î â¢ âk	no	no	no	no	no

* In terms only. -

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/BOLOGNA/lambdadelta/basic_1/ (core Î»Î´ version 1)

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Abstract Syntax and Behavior $\lambda\delta butterfly$ +

This is a summary of available syntactic items and reductions (block structure). +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

domain	block	leader	âÎ¶ *	annotator (with âÏµ *)	applicator (with âÎ¸ *)	reference *	reduction
{X \| Î â¢ â¤}	exclusion	Î â¢ Ï	yes	no	no	no	no
{X \| Î â¢ X : W}	typed abstraction	Î â¢ Î»W	no	<W>	(V)	#i	âÎ² *
{X \| Î â¢ X = V}	abbreviation	Î â¢ Î´V	yes	no	no	#i	âÎ´
no	sort	Î â¢ âk	no	no	no	no	no

* In terms only. +

Summary of the Specification $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	120	characters	198089	nodes	1449099
propositions	theorems	81	lemmas	618	total	699
concepts	declared	39	defined	47	total	86

January 2015. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	120	characters	198089	nodes	1449099
propositions	theorems	81	lemmas	618	total	699
concepts	declared	39	defined	47	total	86

+ January 2015. Update with backports from the abandoned specification of Î»Î´ version 2. -

May 2008. +

+ May 2008. Specification is concluded. -

November 2006. +

+ November 2006. Decidability of native type assignment, Î»Î´ version 1 is released. -

December 2005. +

+ December 2005. Preservation of native type by reduction, Î»Î´ version 1 is announced. -

May 2004. +

+ May 2004. Specification starts. -

Logical Structure of the Specification $\lambda\delta butterfly$

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

component	plane	files
examples	terms with special features	levels_ex0 ty3_ex1 nf2_ex2

dynamic typing	well-formed contexts	wf3_defs	wf3_props
	context ref. for native type assignment	csubt_defs	csubt_props csubt_arity_props
	native type assignment	ty3_defs	ty3_props ty3_gen ty3_gen_context ty3_gen_nf2 ty3_lift ty3_subst0 ty3_arity_props ty3_nf2_gen ty3_sred ty3_sred_props ty3_dec
equivalence	context-sensitive equivalence	pc3_defs	pc3_props pc3_gen pc3_gen_context pc3_subst0
	context-free equivalence	pc1_defs	pc1_props

computation	context ref. for reducibility	csubc_defs	csubc_props
	reducibility	sc3_defs	sc3_props sc3_arity
	strongly normalizing computation	sn3_defs	sn3_gen sn3_props
	context-sensitive computation	pr3_defs	pr3_props pr3_gen pr3_gen_context pr3_iso pr3_subst1 pr3_confluence
	context-free computation	pr1_defs	pr1_props pr1_confluence
reduction	normal forms for context-sensitive reduction	nf2_defs	nf2_props nf2_gen nf2_dec
	context-sensitive reduction	pr2_defs	pr2_gen pr2_gen_context pr2_lift pr2_subst1 pr2_confluence
	normal forms for context-free reduction		nf0_dec
	context-free reduction	wcpr0_defs
		pr0_defs	pr0_gen pr0_lift pr0_subst0 pr0_subst1 pr0_confluence
unfold	iterated static type assignment	sty1_defs	sty1_props
static typing	static type assignment	sty0_defs	sty0_props
	context ref. for binary arity assignment	csuba_defs	csuba_props
	binary arity assignment	arity_defs	arity_props arity_gen arity_subst0 arity_sred
	binary arity	levels_defs llt_defs aprem_defs
	parameters	parameter_defs
	basic context ref.	csubv_defs
multiple substitution	iterated context slicing	drop1_defs	drop1_props
	generic term relocation	lift1_defs	lift1_props
substitution	ordinary substitution	subst_defs	subst_props
		csubst1_defs	csubst1_props
		subst1_defs	subst1_gen subst1_lift subst1_subst1 subst1_confluence
	normal forms for ordinary strict substitution		dnf_dec
	ordinary strict substitution	fsubst0_defs
		csubst0_defs
		subst0_defs	subst0_gen subst0_tlt subst0_lift subst0_subst0 subst0_confluence
	basic local env. slicing	getl_defs	getl_props
		drop_defs	drop_props
	basic term relocation	lift_defs	lift_props lift_gen lift_tlt
grammar	closures	flt_defs
	contexts	contexts_defs clt_defs ctail_defs app_defs cnt_defs
	terms	tlist_defs
		terms_defs tlt_defs iso_defs

$\lambda\delta rainbow rule$

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

+ + +

Logical Structure of the Specification $\lambda\delta butterfly$ +

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

component	plane	files	+ +
examples	terms with special features	+ levels_ex0 + ty3_ex1 + nf2_ex2 +	+ +
+	+	+	+ +
dynamic typing	well-formed contexts	+ wf3_defs +	+ wf3_props +
+ +	context ref. for native type assignment	+ csubt_defs +	+ csubt_props + csubt_arity_props +
+ +	native type assignment	+ ty3_defs +	+ ty3_props + ty3_gen + ty3_gen_context + ty3_gen_nf2 + ty3_lift + ty3_subst0 + ty3_arity_props + ty3_nf2_gen + ty3_sred + ty3_sred_props + ty3_dec +
equivalence	context-sensitive equivalence	+ pc3_defs +	+ pc3_props + pc3_gen + pc3_gen_context + pc3_subst0 +
+ +	context-free equivalence	+ pc1_defs +	+ pc1_props +
+	+	+	+ +
computation	context ref. for reducibility	+ csubc_defs +	+ csubc_props +
+ +	reducibility	+ sc3_defs +	+ sc3_props + sc3_arity +
+ +	strongly normalizing computation	+ sn3_defs +	+ sn3_gen + sn3_props +
+ +	context-sensitive computation	+ pr3_defs +	+ pr3_props + pr3_gen + pr3_gen_context + pr3_iso + pr3_subst1 + pr3_confluence +
+ +	context-free computation	+ pr1_defs +	+ pr1_props + pr1_confluence +
reduction	normal forms for context-sensitive reduction	+ nf2_defs +	+ nf2_props + nf2_gen + nf2_dec +
+ +	context-sensitive reduction	+ pr2_defs +	+ pr2_gen + pr2_gen_context + pr2_lift + pr2_subst1 + pr2_confluence +
+ +	normal forms for context-free reduction	+	+ nf0_dec +
+ +	context-free reduction	+ wcpr0_defs +	+ +
+ +	+ +	+ pr0_defs +	+ pr0_gen + pr0_lift + pr0_subst0 + pr0_subst1 + pr0_confluence +
unfold	iterated static type assignment	+ sty1_defs +	+ sty1_props +
static typing	static type assignment	+ sty0_defs +	+ sty0_props +
+ +	context ref. for binary arity assignment	+ csuba_defs +	+ csuba_props +
+ +	binary arity assignment	+ arity_defs +	+ arity_props + arity_gen + arity_subst0 + arity_sred +
+ +	binary arity	+ levels_defs + llt_defs + aprem_defs +	+ +
+ +	parameters	+ parameter_defs +	+ +
+ +	basic context ref.	+ csubv_defs +	+ +
multiple substitution	iterated context slicing	+ drop1_defs +	+ drop1_props +
+ +	generic term relocation	+ lift1_defs +	+ lift1_props +
substitution	ordinary substitution	+ subst_defs +	+ subst_props +
+ +	+ +	+ csubst1_defs +	+ csubst1_props +
+ +	+ +	+ subst1_defs +	+ subst1_gen + subst1_lift + subst1_subst1 + subst1_confluence +
+ +	normal forms for ordinary strict substitution	+	+ dnf_dec +
+ +	ordinary strict substitution	+ fsubst0_defs +	+ +
+ +	+ +	+ csubst0_defs +	+ +
+ +	+ +	+ subst0_defs +	+ subst0_gen + subst0_tlt + subst0_lift + subst0_subst0 + subst0_confluence +
+ +	basic local env. slicing	+ getl_defs +	+ getl_props +
+ +	+ +	+ drop_defs +	+ drop_props +
+ +	basic term relocation	+ lift_defs +	+ lift_props + lift_gen + lift_tlt +
grammar	closures	+ flt_defs +	+ +
+ +	contexts	+ contexts_defs + clt_defs + ctail_defs + app_defs + cnt_defs +	+ +
+ +	terms	+ tlist_defs +	+ +
+ +	+ +	+ terms_defs + tlt_defs + iso_defs +	+ +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:41 +0100

+ + diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 765da9830..c694c00df 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,6 +1,108 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/basic_2/ (core Î»Î´ version 2)

$\lambda\delta rainbow rule$

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 $\lambda\delta butterfly$

Here is a numerical account of the specification's contents +--> +

Summary of the Specification $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	213	characters	224056	nodes	1100545
propositions	theorems	61	lemmas	743	total	804
concepts	declared	29	defined	66	total	95

Stage "B"

Ongoing. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	213	characters	224345	nodes	1097549
propositions	theorems	61	lemmas	743	total	804
concepts	declared	29	defined	65	total	94

Stage "B"

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

Stage "A2": "Extending the Applicability Condition"

2017 February 19. +

Stage "A2": "Extending the Applicability Condition"

+ 2017 February 19. Generic candidates of reducibility. -

2017 January 17. +

+ 2017 January 17. Confluence for parallel r-transition on referred entries of local environments. -

2016 September 15. +

+ 2016 September 15. Confluence for context-sensitive parallel r-transition on terms. -

2016 April 16. +

+ 2016 April 16. Grammatical component reconstructed: grammar, relocation, s_transition, s_computation, static (anniversary milestone). -

2016 March 25. +

+ 2016 March 25. Relocation with reference transforming maps (rtmap). -

2015 October 9. +

+ 2015 October 9. Î»Î´ version 2A2 is started. -

Stage "A1": "Extending the Applicability Condition"

2015 August 27. +

Stage "A1": "Extending the Applicability Condition"

+ 2015 August 27. Î»Î´ version 2A1 appears too complex and is dismissed. -

2014 October 28. +

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

2014 September 9. +

+ 2014 September 9. Iterated static type assignment defined (more elegantly) as a primitive notion. -

2014 June 18. +

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

2014 June 9. +

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

2014 April 16. +

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

2014 January 20. +

+ 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. +

+ 2013 August 7. Passive support for global environments. -

2013 July 27. +

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

2013 July 20. +

+ 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 rst-computation on closures. -

2012 October 16. +

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

2012 July 26. +

+ 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. Generic 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. Î»Î´ version 2 is started. -

Logical Structure of the Specification $\lambda\delta butterfly$

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

component	plane	files
rt-computation	uncounted context-sensitive rt-transition	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )
		csx ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )	csx_cnx csx_cpxs csx_csx
		lfpxs ( â¦?,?â¦ â¢ â¬*[?,?] ? )	lfpxs_length lfpxs_fqup
		cpxs ( â¦?,?â¦ â¢ ? â¬*[?] ? )	cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transition	parallel qrst-transition	fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )
	t-bound context-sensitive rt-transition	lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )	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-transition	cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )	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-transition	cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
iterated static typing	iterated extension on referred entries	tc_lfxs ( ? â¦»**[?,?] ? )
static typing	generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
		gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
		gcp
	atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
		aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
	degree-based equivalence on referred entries	ffdeq ( â¦?,?,?â¦ â¡[?,?] â¦?,?,?â¦ )	ffdeq_fqup ffdeq_ffdeq
		lfdeq ( ? â¡[?,?,?] ? )	lfdeq_length lfdeq_fqup lfdeq_lfdeq
	generic extension on referred entries	lfxs ( ? â¦»*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
	context-sensitive free variables	lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )	lsubf_frees
		frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_drops frees_fqup frees_frees
	restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr
s-computation	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
		fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_weight fqup_drops fqup_fqup
s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight
		fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight
relocation	generic slicing for local environments	drops_vector ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )
		drops ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
	generic relocation for terms	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector
		lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
	ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq
	generic entrywise extension	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
syntax	append for local environments	append ( ? @@ ? )	append_length
	degree-based equivalence for terms	deq ( ? â¡[?,?] ? )	deq_deq
	same top term structure	tsts ( ? â ? )	tsts_tsts tsts_vector
	closures	cl_weight ( â¯{?,?,?} )
		cl_restricted_weight ( â¯{?,?} )
	global environments	genv
	local environments	lenv_length ( \|?\| )
		lenv_weight ( â¯{?} )
		lenv
	terms	term_vector ( â¶?.? )
		term_simple ( ðâ¦?â¦ )
		term_weight ( â¯{?} )
		term
	items	item_sd
		item_sh
		item
	atomic arities	aarity

$\lambda\delta rainbow rule$

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

+ + +

Logical Structure of the Specification $\lambda\delta butterfly$ +

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

component	plane	files	+ +
rt-computation	uncounted context-sensitive rt-transition	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )	+ +
+ +	+ +	csx ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )	csx_cnx csx_cpxs csx_csx
+ +	+ +	lfpxs ( â¦?,?â¦ â¢ â¬*[?,?] ? )	lfpxs_length lfpxs_fqup lfpxs_cpxs
+ +	+ +	cpxs ( â¦?,?â¦ â¢ ? â¬*[?] ? )	cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transition	parallel qrst-transition	fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	+ +
+ +	t-bound context-sensitive rt-transition	lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )	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-transition	cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )	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-transition	cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
iterated static typing	iterated extension on referred entries	tc_lfxs ( ? â¦»**[?,?] ? )	+ +
static typing	generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
+ +	+ +	gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
+ +	+ +	gcp	+ +
+ +	atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
+ +	+ +	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
+ +	degree-based equivalence on referred entries	ffdeq ( â¦?,?,?â¦ â¡[?,?] â¦?,?,?â¦ )	ffdeq_fqup ffdeq_ffdeq
+ +	+ +	lfdeq ( ? â¡[?,?,?] ? )	lfdeq_length lfdeq_fqup lfdeq_lfdeq
+ +	generic extension on referred entries	lfxs ( ? â¦»*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
+ +	context-sensitive free variables	lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )	lsubf_frees
+ +	+ +	frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_drops frees_fqup frees_frees
+ +	restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr
s-computation	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
+ +	+ +	fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_weight fqup_drops fqup_fqup
s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight
+ +	+ +	fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight
relocation	generic slicing for local environments	drops_vector ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	+ +
+ +	+ +	drops ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
+ +	generic relocation for terms	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector
+ +	+ +	lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
+ +	ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq
+ +	generic entrywise extension	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
syntax	append for local environments	append ( ? @@ ? )	append_length
+ +	degree-based equivalence for terms	deq ( ? â¡[?,?] ? )	deq_deq
+ +	same top term structure	tsts ( ? â ? )	tsts_tsts tsts_vector
+ +	closures	cl_weight ( â¯{?,?,?} )	+ +
+ +	+ +	cl_restricted_weight ( â¯{?,?} )	+ +
+ +	global environments	genv	+ +
+ +	local environments	lenv_length ( \|?\| )	+ +
+ +	+ +	lenv_weight ( â¯{?} )	+ +
+ +	+ +	lenv	+ +
+ +	terms	term_vector ( â¶?.? )	+ +
+ +	+ +	term_simple ( ðâ¦?â¦ )	+ +
+ +	+ +	term_weight ( â¯{?} )	+ +
+ +	+ +	term	+ +
+ +	items	item_sd	+ +
+ +	+ +	item_sh	+ +
+ +	+ +	item	+ +
+ +	atomic arities	aarity	+ +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:41 +0100

+ + diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index a82d853eb..170d355dd 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -1,3 +1,7121 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/basic_2/ (core Î»Î´ version 2)

$\lambda\delta rainbow rule$

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 $\lambda\delta butterfly$

Version 2A1	Version 2A2
aarity	aarity
destruct_apair_apair_aux	destruct_apair_apair_aux
discr_apair_xy_x	discr_apair_xy_x
discr_tpair_xy_y	discr_apair_xy_y
eq_aarity_dec	eq_aarity_dec
item0	item0
bind2	bind2
flat2	flat2
item2	item2
destruct_sort_sort_aux	destruct_sort_sort_aux
eq_item0_dec	eq_item0_dec
eq_bind2_dec	eq_bind2_dec
eq_flat2_dec	eq_flat2_dec
eq_item2_dec	eq_item2_dec
sh	sh
sh_N	sh_N
nexts_le	nexts_le
nexts_lt	nexts_lt
nexts_dec	nexts_dec
nexts_inj	nexts_inj
sd	sd
deg_O	deg_O
sd_O	sd_O
deg_SO	deg_SO
deg_SO_inv_pos_aux	deg_SO_inv_succ_aux
deg_SO_inv_pos	deg_SO_inv_succ
deg_SO_refl	deg_SO_refl
deg_SO_gt	deg_SO_gt
sd_SO	sd_SO
sd_d	sd_d
deg_inv_pred	deg_inv_pred
deg_inv_prec	deg_inv_prec
deg_iter	deg_iter
deg_next_SO	deg_next_SO
sd_d_SS	sd_d_SS
sd_d_correct	sd_d_correct
term	term
eq_term_dec	eq_term_dec
destruct_tatom_tatom_aux	destruct_tatom_tatom_aux
destruct_tpair_tpair_aux	destruct_tpair_tpair_aux
discr_tpair_xy_x	discr_tpair_xy_x
discr_tpair_xy_y	discr_tpair_xy_y
eq_false_inv_tpair_sn	eq_false_inv_tpair_sn
eq_false_inv_tpair_dx	eq_false_inv_tpair_dx
tw	tw
tw_pos	tw_pos
simple	simple
simple_inv_bind_aux	simple_inv_bind_aux
simple_inv_bind	simple_inv_bind
simple_inv_pair	simple_inv_pair
lenv	lenv
eq_lenv_dec	eq_lenv_dec
destruct_lpair_lpair_aux	destruct_lpair_lpair_aux
discr_lpair_x_xy	discr_lpair_x_xy
	discr_lpair_xy_x
	ceq
	cfull
lw	lw
lw_pair	lw_pair
length	length
length_inv_zero_dx	length_inv_zero_dx
length_inv_zero_sn	length_inv_zero_sn
length_inv_pos_dx	length_inv_succ_dx
length_inv_pos_sn	length_inv_succ_sn
	length_atom
	length_pair
genv	genv
eq_genv_dec	eq_genv_dec
rfw	rfw
rfw_shift	rfw_shift
rfw_tpair_sn	rfw_tpair_sn
rfw_tpair_dx	rfw_tpair_dx
rfw_lpair_sn	rfw_lpair_sn
rfw_lpair_dx	rfw_lpair_dx
da	da
da_inv_sort_aux	da_inv_sort_aux
da_inv_sort	da_inv_sort
da_inv_lref_aux	da_inv_lref_aux
da_inv_lref	da_inv_lref
da_inv_gref_aux	da_inv_gref_aux
da_inv_gref	da_inv_gref
da_inv_bind_aux	da_inv_bind_aux
da_inv_bind	da_inv_bind
da_inv_flat_aux	da_inv_flat_aux
da_inv_flat	da_inv_flat
lstas	lstas
lstas_inv_sort1_aux	lstas_inv_sort1_aux
lstas_inv_sort1	lstas_inv_sort1
lstas_inv_lref1_aux	lstas_inv_lref1_aux
lstas_inv_lref1	lstas_inv_lref1
lstas_inv_lref1_O	lstas_inv_lref1_O
lstas_inv_lref1_S	lstas_inv_lref1_S
lstas_inv_gref1_aux	lstas_inv_gref1_aux
lstas_inv_gref1	lstas_inv_gref1
lstas_inv_bind1_aux	lstas_inv_bind1_aux
lstas_inv_bind1	lstas_inv_bind1
lstas_inv_appl1_aux	lstas_inv_appl1_aux
lstas_inv_appl1	lstas_inv_appl1
lstas_inv_cast1_aux	lstas_inv_cast1_aux
lstas_inv_cast1	lstas_inv_cast1

lift	lift
lift_inv_O2_aux	lift_inv_O2_aux
lift_inv_O2	lift_inv_O2
lift_inv_sort1_aux	lift_inv_sort1_aux
lift_inv_sort1	lift_inv_sort1
lift_inv_lref1_aux	lift_inv_lref1_aux
lift_inv_lref1	lift_inv_lref1
lift_inv_lref1_lt	lift_inv_lref1_lt
lift_inv_lref1_ge	lift_inv_lref1_ge
lift_inv_gref1_aux	lift_inv_gref1_aux
lift_inv_gref1	lift_inv_gref1
lift_inv_bind1_aux	lift_inv_bind1_aux
lift_inv_bind1	lift_inv_bind1
lift_inv_flat1_aux	lift_inv_flat1_aux
lift_inv_flat1	lift_inv_flat1
lift_inv_sort2_aux	lift_inv_sort2_aux
lift_inv_sort2	lift_inv_sort2
lift_inv_lref2_aux	lift_inv_lref2_aux
lift_inv_lref2	lift_inv_lref2
lift_inv_lref2_lt	lift_inv_lref2_lt
lift_inv_lref2_be	lift_inv_lref2_be
lift_inv_lref2_ge	lift_inv_lref2_ge
lift_inv_gref2_aux	lift_inv_gref2_aux
lift_inv_gref2	lift_inv_gref2
lift_inv_bind2_aux	lift_inv_bind2_aux
lift_inv_bind2	lift_inv_bind2
lift_inv_flat2_aux	lift_inv_flat2_aux
lift_inv_flat2	lift_inv_flat2
lift_inv_pair_xy_x	lift_inv_pair_xy_x
lift_inv_pair_xy_y	lift_inv_pair_xy_y
lift_fwd_pair1	lift_fwd_pair1
lift_fwd_pair2	lift_fwd_pair2
lift_fwd_tw	lift_fwd_tw
lift_simple_dx	lift_simple_dx
lift_simple_sn	lift_simple_sn
lift_lref_ge_minus	lift_lref_ge_minus
lift_lref_ge_minus_eq	lift_lref_ge_minus_eq
lift_refl	lift_refl
lift_total	lift_total
lift_split	lift_split
is_lift_dec	is_lift_dec
drop	drop
d_liftable	d_liftable
d_deliftable_sn	d_deliftable_sn
dropable_sn	dropable_sn
dropable_dx	dropable_dx
drop_inv_atom1_aux	drop_inv_atom1_aux
drop_inv_atom1	drop_inv_atom1
drop_inv_O1_pair1_aux	drop_inv_O1_pair1_aux
drop_inv_O1_pair1	drop_inv_O1_pair1
drop_inv_pair1	drop_inv_pair1
drop_inv_drop1_lt	drop_inv_drop1_lt
drop_inv_drop1	drop_inv_drop1
drop_inv_skip1_aux	drop_inv_skip1_aux
drop_inv_skip1	drop_inv_skip1
drop_inv_O1_pair2	drop_inv_O1_pair2
drop_inv_skip2_aux	drop_inv_skip2_aux
drop_inv_skip2	drop_inv_skip2
drop_inv_O1_gt	drop_inv_O1_gt
drop_refl_atom_O2	drop_refl_atom_O2
drop_refl	drop_refl
drop_drop_lt	drop_drop_lt
drop_skip_lt	drop_skip_lt
drop_O1_le	drop_O1_le
drop_O1_lt	drop_O1_lt
drop_O1_pair	drop_O1_pair
drop_O1_ge	drop_O1_ge
drop_O1_eq	drop_O1_eq
drop_split	drop_split
drop_FT	drop_FT
drop_gen	drop_gen
drop_T	drop_T
d_liftable_LTC	d_liftable_LTC
d_deliftable_sn_LTC	d_deliftable_sn_LTC
dropable_sn_TC	dropable_sn_TC
dropable_dx_TC	dropable_dx_TC
d_deliftable_sn_llstar	d_deliftable_sn_llstar
drop_fwd_drop2	drop_fwd_drop2
drop_fwd_length_ge	drop_fwd_length_ge
drop_fwd_length_le_le	drop_fwd_length_le_le
drop_fwd_length_le_ge	drop_fwd_length_le_ge
drop_fwd_length	drop_fwd_length
drop_fwd_length_minus2	drop_fwd_length_minus2
drop_fwd_length_minus4	drop_fwd_length_minus4
drop_fwd_length_le2	drop_fwd_length_le2
drop_fwd_length_le4	drop_fwd_length_le4
drop_fwd_length_lt2	drop_fwd_length_lt2
drop_fwd_length_lt4	drop_fwd_length_lt4
drop_fwd_length_eq1	drop_fwd_length_eq1
drop_fwd_length_eq2	drop_fwd_length_eq2
drop_fwd_lw	drop_fwd_lw
drop_fwd_lw_lt	drop_fwd_lw_lt
drop_fwd_rfw	drop_fwd_rfw
drop_inv_O2_aux	drop_inv_O2_aux
drop_inv_O2	drop_inv_O2
drop_inv_length_eq	drop_inv_length_eq
drop_inv_refl	drop_inv_refl
drop_inv_FT_aux	drop_inv_FT_aux
drop_inv_FT	drop_inv_FT
drop_inv_gen	drop_inv_gen
drop_inv_T	drop_inv_T
lsubr	lsubr
lsubr_refl	lsubr_refl
lsubr_inv_atom1_aux	lsubr_inv_atom1_aux
lsubr_inv_atom1	lsubr_inv_atom1
lsubr_inv_abst1_aux	lsubr_inv_abst1_aux
lsubr_inv_abst1	lsubr_inv_abst1
lsubr_inv_abbr2_aux	lsubr_inv_abbr2_aux
lsubr_inv_abbr2	lsubr_inv_abbr2
lsubr_fwd_length	lsubr_fwd_length
lsubr_fwd_drop2_pair	lsubr_fwd_drop2_pair
lsubr_fwd_drop2_abbr	lsubr_fwd_drop2_abbr
cpr	cpr
lsubr_cpr_trans	lsubr_cpr_trans
tpr_cpr	tpr_cpr
cpr_refl	cpr_refl
cpr_pair_sn	cpr_pair_sn
cpr_delift	cpr_delift
lstas_cpr_aux	lstas_cpr_aux
lstas_cpr	lstas_cpr
cpr_inv_atom1_aux	cpr_inv_atom1_aux
cpr_inv_atom1	cpr_inv_atom1
cpr_inv_sort1	cpr_inv_sort1
cpr_inv_lref1	cpr_inv_lref1
cpr_inv_gref1	cpr_inv_gref1
cpr_inv_bind1_aux	cpr_inv_bind1_aux
cpr_inv_bind1	cpr_inv_bind1
cpr_inv_abbr1	cpr_inv_abbr1
cpr_inv_abst1	cpr_inv_abst1
cpr_inv_flat1_aux	cpr_inv_flat1_aux
cpr_inv_flat1	cpr_inv_flat1
cpr_inv_appl1	cpr_inv_appl1
cpr_inv_appl1_simple	cpr_inv_appl1_simple
cpr_inv_cast1	cpr_inv_cast1
cpr_fwd_bind1_minus	cpr_fwd_bind1_minus
cnr	cnr
cnr_inv_delta	cnr_inv_delta
cnr_inv_abst	cnr_inv_abst
cnr_inv_abbr	cnr_inv_abbr
cnr_inv_zeta	cnr_inv_zeta
cnr_inv_appl	cnr_inv_appl
cnr_inv_eps	cnr_inv_eps
cnr_sort	cnr_sort
cnr_lref_free	cnr_lref_free
cnr_lref_atom	cnr_lref_atom
cnr_abst	cnr_abst
cnr_appl_simple	cnr_appl_simple
cnr_dec	cnr_dec
cprs	cprs
cprs_ind	cprs_ind
cprs_ind_dx	cprs_ind_dx
cpr_cprs	cpr_cprs
cprs_refl	cprs_refl
cprs_strap1	cprs_strap1
cprs_strap2	cprs_strap2
lsubr_cprs_trans	lsubr_cprs_trans
tprs_cprs	tprs_cprs
cprs_bind_dx	cprs_bind_dx
cprs_flat_dx	cprs_flat_dx
cprs_flat_sn	cprs_flat_sn
cprs_zeta	cprs_zeta
cprs_eps	cprs_eps
cprs_beta_dx	cprs_beta_dx
cprs_theta_dx	cprs_theta_dx
cprs_inv_sort1	cprs_inv_sort1
cprs_inv_cast1	cprs_inv_cast1
cprs_inv_cnr1	cprs_inv_cnr1
scpds	scpds
sta_cprs_scpds	sta_cprs_scpds
lstas_scpds	lstas_scpds
scpds_strap1	scpds_strap1
scpds_fwd_cprs	scpds_fwd_cprs
scpes	scpes
scpds_div	scpds_div
scpes_sym	scpes_sym
lift_inj	lift_inj
lift_div_le	lift_div_le
lift_div_be	lift_div_be
lift_mono	lift_mono
lift_trans_be	lift_trans_be
lift_trans_le	lift_trans_le
lift_trans_ge	lift_trans_ge
lift_conf_O1	lift_conf_O1
lift_conf_be	lift_conf_be
drop_mono	drop_mono
drop_conf_ge	drop_conf_ge
drop_conf_be	drop_conf_be
drop_conf_le	drop_conf_le
drop_trans_ge	drop_trans_ge
drop_trans_le	drop_trans_le
d_liftable_llstar	d_liftable_llstar
drop_conf_lt	drop_conf_lt
drop_trans_lt	drop_trans_lt
drop_trans_ge_comm	drop_trans_ge_comm
drop_conf_div	drop_conf_div
drop_fwd_be	drop_fwd_be
aaa	aaa
aaa_inv_sort_aux	aaa_inv_sort_aux
aaa_inv_sort	aaa_inv_sort
aaa_inv_lref_aux	aaa_inv_lref_aux
aaa_inv_lref	aaa_inv_lref
aaa_inv_gref_aux	aaa_inv_gref_aux
aaa_inv_gref	aaa_inv_gref
aaa_inv_abbr_aux	aaa_inv_abbr_aux
aaa_inv_abbr	aaa_inv_abbr
aaa_inv_abst_aux	aaa_inv_abst_aux
aaa_inv_abst	aaa_inv_abst
aaa_inv_appl_aux	aaa_inv_appl_aux
aaa_inv_appl	aaa_inv_appl
aaa_inv_cast_aux	aaa_inv_cast_aux
aaa_inv_cast	aaa_inv_cast
aaa_lift	aaa_lift
aaa_inv_lift	aaa_inv_lift
aaa_mono	aaa_mono
lsuba	lsuba
lsuba_inv_atom1_aux	lsuba_inv_atom1_aux
lsuba_inv_atom1	lsuba_inv_atom1
lsuba_inv_pair1_aux	lsuba_inv_pair1_aux
lsuba_inv_pair1	lsuba_inv_pair1
lsuba_inv_atom2_aux	lsuba_inv_atom2_aux
lsubc_inv_atom2	lsubc_inv_atom2
lsuba_inv_pair2_aux	lsuba_inv_pair2_aux
lsuba_inv_pair2	lsuba_inv_pair2
lsuba_fwd_lsubr	lsuba_fwd_lsubr
lsuba_refl	lsuba_refl
lsuba_drop_O1_conf	lsuba_drop_O1_conf
lsuba_drop_O1_trans	lsuba_drop_O1_trans
lsuba_aaa_conf	lsuba_aaa_conf
lsuba_aaa_trans	lsuba_aaa_trans
lreq	lreq
lreq_pair_lt	lreq_pair_lt
lreq_succ_lt	lreq_succ_lt
lreq_pair_O_Y	lreq_pair_O_Y
lreq_refl	lreq_refl
lreq_O2	lreq_O2
lreq_sym	lreq_sym
lreq_inv_atom1_aux	lreq_inv_atom1_aux
lreq_inv_atom1	lreq_inv_atom1
lreq_inv_zero1_aux	lreq_inv_zero1_aux
lreq_inv_zero1	lreq_inv_zero1
lreq_inv_pair1_aux	lreq_inv_pair1_aux
lreq_inv_pair1	lreq_inv_pair1
lreq_inv_pair	lreq_inv_pair
lreq_inv_succ1_aux	lreq_inv_succ1_aux
lreq_inv_succ1	lreq_inv_succ1
lreq_inv_atom2	lreq_inv_atom2
lreq_inv_succ	lreq_inv_succ
lreq_inv_zero2	lreq_inv_zero2
lreq_inv_pair2	lreq_inv_pair2
lreq_inv_succ2	lreq_inv_succ2
lreq_fwd_length	lreq_fwd_length
lreq_inv_O_Y_aux	lreq_inv_O_Y_aux
lreq_inv_O_Y	lreq_inv_O_Y
lreq_trans	lreq_trans
lreq_canc_sn	lreq_canc_sn
lreq_canc_dx	lreq_canc_dx
lreq_join	lreq_join
dedropable_sn	dedropable_sn
lreq_drop_trans_be	lreq_drop_trans_be
lreq_drop_conf_be	lreq_drop_conf_be
drop_O1_ex	drop_O1_ex
dedropable_sn_TC	dedropable_sn_TC
drop_O1_inj	drop_O1_inj
lpx_sn	lpx_sn
lpx_sn_refl	lpx_sn_refl
lpx_sn_inv_atom1_aux	lpx_sn_inv_atom1_aux
lpx_sn_inv_atom1	lpx_sn_inv_atom1
lpx_sn_inv_pair1_aux	lpx_sn_inv_pair1_aux
lpx_sn_inv_pair1	lpx_sn_inv_pair1
lpx_sn_inv_atom2_aux	lpx_sn_inv_atom2_aux
lpx_sn_inv_atom2	lpx_sn_inv_atom2
lpx_sn_inv_pair2_aux	lpx_sn_inv_pair2_aux
lpx_sn_inv_pair2	lpx_sn_inv_pair2
lpx_sn_inv_pair	lpx_sn_inv_pair
lpx_sn_fwd_length	lpx_sn_fwd_length
lpx_sn_drop_conf	lpx_sn_drop_conf
lpx_sn_drop_trans	lpx_sn_drop_trans
lpx_sn_deliftable_dropable	lpx_sn_deliftable_dropable
lpx_sn_liftable_dedropable	lpx_sn_liftable_dedropable
lpx_sn_dropable_aux	lpx_sn_dropable_aux
lpx_sn_dropable	lpx_sn_dropable
fw	fw
fw_shift	fw_shift
fw_tpair_sn	fw_tpair_sn
fw_tpair_dx	fw_tpair_dx
fw_lpair_sn	fw_lpair_sn
fqu	fqu
fqu_drop_lt	fqu_drop_lt
fqu_lref_S_lt	fqu_lref_S_lt
fqu_fwd_fw	fqu_fwd_fw
fqu_fwd_length_lref1_aux	fqu_fwd_length_lref1_aux
fqu_fwd_length_lref1	fqu_fwd_length_lref1
fqu_inv_eq_aux	fqu_inv_eq_aux
fqu_inv_eq	fqu_inv_eq
fqu_wf_ind	fqu_wf_ind
fquq	fquq
fquq_refl	fquq_refl
fqu_fquq	fqu_fquq
fquq_fwd_fw	fquq_fwd_fw
fquq_fwd_length_lref1_aux	fquq_fwd_length_lref1_aux
fquq_fwd_length_lref1	fquq_fwd_length_lref1
fquqa	fquqa
fquqa_refl	fquqa_refl
fquqa_drop	fquqa_drop
fquq_fquqa	fquq_fquqa
fquqa_inv_fquq	fquqa_inv_fquq
fquq_inv_gen	fquq_inv_gen
fqup	fqup
fqu_fqup	fqu_fqup
fqup_strap1	fqup_strap1
fqup_strap2	fqup_strap2
fqup_drop	fqup_drop
fqup_lref	fqup_lref
fqup_pair_sn	fqup_pair_sn
fqup_bind_dx	fqup_bind_dx
fqup_flat_dx	fqup_flat_dx
fqup_flat_dx_pair_sn	fqup_flat_dx_pair_sn
fqup_bind_dx_flat_dx	fqup_bind_dx_flat_dx
fqup_flat_dx_bind_dx	fqup_flat_dx_bind_dx
fqup_ind	fqup_ind
fqup_ind_dx	fqup_ind_dx
fqup_fwd_fw	fqup_fwd_fw
fqup_wf_ind	fqup_wf_ind
fqup_wf_ind_eq	fqup_wf_ind_eq
fqus	fqus
fqus_ind	fqus_ind
fqus_ind_dx	fqus_ind_dx
fqus_refl	fqus_refl
fquq_fqus	fquq_fqus
fqus_strap1	fqus_strap1
fqus_strap2	fqus_strap2
fqus_drop	fqus_drop
fqup_fqus	fqup_fqus
fqus_fwd_fw	fqus_fwd_fw
fqup_inv_step_sn	fqup_inv_step_sn
fqus_inv_gen	fqus_inv_gen
fqus_strap1_fqu	fqus_strap1_fqu
fqus_strap2_fqu	fqus_strap2_fqu
fqus_fqup_trans	fqus_fqup_trans
fqup_fqus_trans	fqup_fqus_trans
cpx	cpx
lsubr_cpx_trans	lsubr_cpx_trans
cpx_refl	cpx_refl
cpr_cpx	cpr_cpx
cpx_pair_sn	cpx_pair_sn
cpx_delift	cpx_delift
cpx_inv_atom1_aux	cpx_inv_atom1_aux
cpx_inv_atom1	cpx_inv_atom1
cpx_inv_sort1	cpx_inv_sort1
cpx_inv_lref1	cpx_inv_lref1
cpx_inv_lref1_ge	cpx_inv_lref1_ge
cpx_inv_gref1	cpx_inv_gref1
cpx_inv_bind1_aux	cpx_inv_bind1_aux
cpx_inv_bind1	cpx_inv_bind1
cpx_inv_abbr1	cpx_inv_abbr1
cpx_inv_abst1	cpx_inv_abst1
cpx_inv_flat1_aux	cpx_inv_flat1_aux
cpx_inv_flat1	cpx_inv_flat1
cpx_inv_appl1	cpx_inv_appl1
cpx_inv_appl1_simple	cpx_inv_appl1_simple
cpx_inv_cast1	cpx_inv_cast1
cpx_fwd_bind1_minus	cpx_fwd_bind1_minus
sta_cpx_aux	sta_cpx_aux
sta_cpx	sta_cpx
cpx_lift	cpx_lift
cpx_inv_lift1	cpx_inv_lift1
fqu_cpx_trans	fqu_cpx_trans
fqu_sta_trans	fqu_sta_trans
fquq_cpx_trans	fquq_cpx_trans
fquq_sta_trans	fquq_sta_trans
fqup_cpx_trans	fqup_cpx_trans
fqus_cpx_trans	fqus_cpx_trans
fqu_cpx_trans_neq	fqu_cpx_trans_neq
fquq_cpx_trans_neq	fquq_cpx_trans_neq
fqup_cpx_trans_neq	fqup_cpx_trans_neq
fqus_cpx_trans_neq	fqus_cpx_trans_neq
lpr	lpr
lpr_inv_atom1	lpr_inv_atom1
lpr_inv_pair1	lpr_inv_pair1
lpr_inv_atom2	lpr_inv_atom2
lpr_inv_pair2	lpr_inv_pair2
lpr_refl	lpr_refl
lpr_pair	lpr_pair
lpr_fwd_length	lpr_fwd_length
lpx	lpx
lpx_inv_atom1	lpx_inv_atom1
lpx_inv_pair1	lpx_inv_pair1
lpx_inv_atom2	lpx_inv_atom2
lpx_inv_pair2	lpx_inv_pair2
lpx_inv_pair	lpx_inv_pair
lpx_refl	lpx_refl
lpx_pair	lpx_pair
lpr_lpx	lpr_lpx
lpx_fwd_length	lpx_fwd_length
lpx_drop_conf	lpx_drop_conf
drop_lpx_trans	drop_lpx_trans
lpx_drop_trans_O1	lpx_drop_trans_O1
fqu_lpx_trans	fqu_lpx_trans
fquq_lpx_trans	fquq_lpx_trans
lpx_fqu_trans	lpx_fqu_trans
lpx_fquq_trans	lpx_fquq_trans
cpx_lpx_aaa_conf	cpx_lpx_aaa_conf
cpx_aaa_conf	cpx_aaa_conf
lpx_aaa_conf	lpx_aaa_conf
cpr_aaa_conf	cpr_aaa_conf
lpr_aaa_conf	lpr_aaa_conf
cnx	cnx
cnx_inv_sort	cnx_inv_sort
cnx_inv_delta	cnx_inv_delta
cnx_inv_abst	cnx_inv_abst
cnx_inv_abbr	cnx_inv_abbr
cnx_inv_zeta	cnx_inv_zeta
cnx_inv_appl	cnx_inv_appl
cnx_inv_eps	cnx_inv_eps
cnx_fwd_cnr	cnx_fwd_cnr
cnx_sort	cnx_sort
cnx_sort_iter	cnx_sort_iter
cnx_lref_free	cnx_lref_free
cnx_lref_atom	cnx_lref_atom
cnx_abst	cnx_abst
cnx_appl_simple	cnx_appl_simple
cnx_dec	cnx_dec
cpxs	cpxs
cpxs_ind	cpxs_ind
cpxs_ind_dx	cpxs_ind_dx
cpxs_refl	cpxs_refl
cpx_cpxs	cpx_cpxs
cpxs_strap1	cpxs_strap1
cpxs_strap2	cpxs_strap2
lsubr_cpxs_trans	lsubr_cpxs_trans
cprs_cpxs	cprs_cpxs
cpxs_sort	cpxs_sort
cpxs_bind_dx	cpxs_bind_dx
cpxs_flat_dx	cpxs_flat_dx
cpxs_flat_sn	cpxs_flat_sn
cpxs_pair_sn	cpxs_pair_sn
cpxs_zeta	cpxs_zeta
cpxs_eps	cpxs_eps
cpxs_ct	cpxs_ct
cpxs_beta_dx	cpxs_beta_dx
cpxs_theta_dx	cpxs_theta_dx
cpxs_inv_sort1	cpxs_inv_sort1
cpxs_inv_cast1	cpxs_inv_cast1
cpxs_inv_cnx1	cpxs_inv_cnx1
cpxs_neq_inv_step_sn	cpxs_neq_inv_step_sn
cpxs_aaa_conf	cpxs_aaa_conf
cprs_aaa_conf	cprs_aaa_conf
lpx_sn_confluent	lpx_sn_confluent
lpx_sn_transitive	lpx_sn_transitive
lpx_sn_trans	lpx_sn_trans
lpx_sn_conf	lpx_sn_conf
cpr_lift	cpr_lift
cpr_inv_lift1	cpr_inv_lift1
lpr_drop_conf	lpr_drop_conf
drop_lpr_trans	drop_lpr_trans
lpr_drop_trans_O1	lpr_drop_trans_O1
fqu_cpr_trans_dx	fqu_cpr_trans_dx
fquq_cpr_trans_dx	fquq_cpr_trans_dx
fqu_cpr_trans_sn	fqu_cpr_trans_sn
fquq_cpr_trans_sn	fquq_cpr_trans_sn
fqu_lpr_trans	fqu_lpr_trans
fquq_lpr_trans	fquq_lpr_trans
cpr_conf_lpr_atom_atom	cpr_conf_lpr_atom_atom
cpr_conf_lpr_atom_delta	cpr_conf_lpr_atom_delta
cpr_conf_lpr_delta_delta	cpr_conf_lpr_delta_delta
cpr_conf_lpr_bind_bind	cpr_conf_lpr_bind_bind
cpr_conf_lpr_bind_zeta	cpr_conf_lpr_bind_zeta
cpr_conf_lpr_zeta_zeta	cpr_conf_lpr_zeta_zeta
cpr_conf_lpr_flat_flat	cpr_conf_lpr_flat_flat
cpr_conf_lpr_flat_eps	cpr_conf_lpr_flat_eps
cpr_conf_lpr_eps_eps	cpr_conf_lpr_eps_eps
cpr_conf_lpr_flat_beta	cpr_conf_lpr_flat_beta
cpr_conf_lpr_flat_theta	cpr_conf_lpr_flat_theta
cpr_conf_lpr_beta_beta	cpr_conf_lpr_beta_beta
cpr_conf_lpr_theta_theta	cpr_conf_lpr_theta_theta
cpr_conf_lpr	cpr_conf_lpr
cpr_conf	cpr_conf
lpr_cpr_conf_dx	lpr_cpr_conf_dx
lpr_cpr_conf_sn	lpr_cpr_conf_sn
lpr_conf	lpr_conf
cprs_delta	cprs_delta
cprs_inv_lref1	cprs_inv_lref1
cprs_lift	cprs_lift
cprs_inv_lift1	cprs_inv_lift1
cprs_trans	cprs_trans
cprs_conf	cprs_conf
cprs_bind	cprs_bind
cprs_flat	cprs_flat
cprs_beta_rc	cprs_beta_rc
cprs_beta	cprs_beta
cprs_theta_rc	cprs_theta_rc
cprs_theta	cprs_theta
cprs_inv_appl1	cprs_inv_appl1
lpr_cpr_trans	lpr_cpr_trans
cpr_bind2	cpr_bind2
lpr_cprs_trans	lpr_cprs_trans
cprs_strip	cprs_strip
cprs_lpr_conf_dx	cprs_lpr_conf_dx
cprs_lpr_conf_sn	cprs_lpr_conf_sn
cprs_bind2_dx	cprs_bind2_dx
TC_lpx_sn_pair_refl	TC_lpx_sn_pair_refl
TC_lpx_sn_pair	TC_lpx_sn_pair
lpx_sn_LTC_TC_lpx_sn	lpx_sn_LTC_TC_lpx_sn
TC_lpx_sn_inv_atom2	TC_lpx_sn_inv_atom2
TC_lpx_sn_inv_pair2	TC_lpx_sn_inv_pair2
TC_lpx_sn_ind	TC_lpx_sn_ind
TC_lpx_sn_inv_atom1	TC_lpx_sn_inv_atom1
TC_lpx_sn_inv_pair1_aux	TC_lpx_sn_inv_pair1_aux
TC_lpx_sn_inv_pair1	TC_lpx_sn_inv_pair1
TC_lpx_sn_inv_lpx_sn_LTC	TC_lpx_sn_inv_lpx_sn_LTC
TC_lpx_sn_fwd_length	TC_lpx_sn_fwd_length
lprs	lprs
lprs_ind	lprs_ind
lprs_ind_dx	lprs_ind_dx
lpr_lprs	lpr_lprs
lprs_refl	lprs_refl
lprs_strap1	lprs_strap1
lprs_strap2	lprs_strap2
lprs_pair_refl	lprs_pair_refl
lprs_inv_atom1	lprs_inv_atom1
lprs_inv_atom2	lprs_inv_atom2
lprs_fwd_length	lprs_fwd_length
lprs_pair	lprs_pair
lprs_inv_pair1	lprs_inv_pair1
lprs_inv_pair2	lprs_inv_pair2
lprs_ind_alt	lprs_ind_alt
lprs_cpr_trans	lprs_cpr_trans
lprs_cprs_trans	lprs_cprs_trans
lprs_cprs_conf_dx	lprs_cprs_conf_dx
lprs_cpr_conf_dx	lprs_cpr_conf_dx
lprs_cprs_conf_sn	lprs_cprs_conf_sn
lprs_cpr_conf_sn	lprs_cpr_conf_sn
cprs_bind2	cprs_bind2
cprs_inv_abst1	cprs_inv_abst1
cprs_inv_abst	cprs_inv_abst
cprs_inv_abbr1	cprs_inv_abbr1
lprs_pair2	lprs_pair2
cpc	cpc
cpc_refl	cpc_refl
cpc_sym	cpc_sym
cpc_fwd_cpr	cpc_fwd_cpr
cpc_conf	cpc_conf
cpcs	cpcs
cpcs_ind	cpcs_ind
cpcs_ind_dx	cpcs_ind_dx
cpcs_refl	cpcs_refl
cpcs_sym	cpcs_sym
cpc_cpcs	cpc_cpcs
cpcs_strap1	cpcs_strap1
cpcs_strap2	cpcs_strap2
cpr_cpcs_dx	cpr_cpcs_dx
cpr_cpcs_sn	cpr_cpcs_sn
cpcs_cpr_strap1	cpcs_cpr_strap1
cpcs_cpr_strap2	cpcs_cpr_strap2
cpcs_cpr_div	cpcs_cpr_div
cpr_div	cpr_div
cpcs_cpr_conf	cpcs_cpr_conf
cpcs_cprs_dx	cpcs_cprs_dx
cpcs_cprs_sn	cpcs_cprs_sn
cpcs_cprs_strap1	cpcs_cprs_strap1
cpcs_cprs_strap2	cpcs_cprs_strap2
cpcs_cprs_div	cpcs_cprs_div
cpcs_cprs_conf	cpcs_cprs_conf
cprs_div	cprs_div
cprs_cpr_div	cprs_cpr_div
cpr_cprs_div	cpr_cprs_div
cpcs_inv_cprs	cpcs_inv_cprs
cpcs_inv_sort	cpcs_inv_sort
cpcs_inv_abst1	cpcs_inv_abst1
cpcs_inv_abst2	cpcs_inv_abst2
cpcs_inv_sort_abst	cpcs_inv_sort_abst
cpcs_inv_lift	cpcs_inv_lift
lpr_cpcs_trans	lpr_cpcs_trans
lprs_cpcs_trans	lprs_cpcs_trans
cpr_cprs_conf_cpcs	cpr_cprs_conf_cpcs
cprs_cpr_conf_cpcs	cprs_cpr_conf_cpcs
cprs_conf_cpcs	cprs_conf_cpcs
lprs_cprs_conf	lprs_cprs_conf
lpr_cprs_conf	lpr_cprs_conf
lpr_cpr_conf	lpr_cpr_conf
cpcs_flat	cpcs_flat
cpcs_flat_dx_cpr_rev	cpcs_flat_dx_cpr_rev
cpcs_bind_dx	cpcs_bind_dx
cpcs_bind_sn	cpcs_bind_sn
lsubr_cpcs_trans	lsubr_cpcs_trans
cpcs_lift	cpcs_lift
cpcs_strip	cpcs_strip
cpcs_inv_abst_sn	cpcs_inv_abst_sn
cpcs_inv_abst_dx	cpcs_inv_abst_dx
cpcs_trans	cpcs_trans
cpcs_canc_sn	cpcs_canc_sn
cpcs_canc_dx	cpcs_canc_dx
cpcs_bind1	cpcs_bind1
cpcs_bind2	cpcs_bind2
lpr_cpcs_conf	lpr_cpcs_conf
cpcs_aaa_mono	cpcs_aaa_mono
da_lift	da_lift
da_inv_lift	da_inv_lift
da_mono	da_mono
lstas_lift	lstas_lift
lstas_inv_lift1	lstas_inv_lift1
lstas_split_aux	lstas_split_aux
lstas_split	lstas_split
lstas_lstas	lstas_lstas
lstas_trans	lstas_trans
lstas_mono	lstas_mono
lstas_correct	lstas_correct
lstas_conf_le	lstas_conf_le
lstas_conf	lstas_conf
da_lstas	da_lstas
lstas_da_conf	lstas_da_conf
lstas_inv_da	lstas_inv_da
lstas_inv_da_ge	lstas_inv_da_ge
lstas_inv_refl_pos	lstas_inv_refl_pos
fqus_trans	fqus_trans
cpxs_delta	cpxs_delta
lstas_cpxs	lstas_cpxs
cpxs_inv_lref1	cpxs_inv_lref1
cpxs_lift	cpxs_lift
cpxs_inv_lift1	cpxs_inv_lift1
fqu_cpxs_trans	fqu_cpxs_trans
fquq_cpxs_trans	fquq_cpxs_trans
fquq_lstas_trans	fquq_lstas_trans
fqup_cpxs_trans	fqup_cpxs_trans
fqus_cpxs_trans	fqus_cpxs_trans
fqus_lstas_trans	fqus_lstas_trans
cpxs_trans	cpxs_trans
cpxs_bind	cpxs_bind
cpxs_flat	cpxs_flat
cpxs_beta_rc	cpxs_beta_rc
cpxs_beta	cpxs_beta
cpxs_theta_rc	cpxs_theta_rc
cpxs_theta	cpxs_theta
cpxs_inv_appl1	cpxs_inv_appl1
lpx_cpx_trans	lpx_cpx_trans
cpx_bind2	cpx_bind2
lpx_cpxs_trans	lpx_cpxs_trans
cpxs_bind2_dx	cpxs_bind2_dx
fqu_cpxs_trans_neq	fqu_cpxs_trans_neq
fquq_cpxs_trans_neq	fquq_cpxs_trans_neq
fqup_cpxs_trans_neq	fqup_cpxs_trans_neq
fqus_cpxs_trans_neq	fqus_cpxs_trans_neq
scpds_strap2	scpds_strap2
scpds_cprs_trans	scpds_cprs_trans
lstas_scpds_trans	lstas_scpds_trans
scpds_inv_abst1	scpds_inv_abst1
scpds_inv_abbr_abst	scpds_inv_abbr_abst
scpds_inv_lstas_eq	scpds_inv_lstas_eq
scpds_fwd_cpxs	scpds_fwd_cpxs
scpds_conf_eq	scpds_conf_eq
scpes_inv_lstas_eq	scpes_inv_lstas_eq
cpcs_scpes	cpcs_scpes
scpes_inv_abst2	scpes_inv_abst2
scpes_refl	scpes_refl
lstas_scpes_trans	lstas_scpes_trans
cprs_scpds_div	cprs_scpds_div
scpes_trans	scpes_trans
scpes_canc_sn	scpes_canc_sn
scpes_canc_dx	scpes_canc_dx
aaa_lstas	aaa_lstas
lstas_aaa_conf	lstas_aaa_conf
scpds_aaa_conf	scpds_aaa_conf
scpes_aaa_mono	scpes_aaa_mono
lsubr_inv_pair1_aux	lsubr_inv_pair1_aux
lsubr_inv_pair1	lsubr_inv_pair1
lsubr_trans	lsubr_trans
applv	applv
applv_simple	applv_simple
at	at
at_inv_nil_aux	at_inv_nil_aux
at_inv_nil	at_inv_nil
at_inv_cons_aux	at_inv_cons_aux
at_inv_cons	at_inv_cons
at_inv_cons_lt	at_inv_cons_lt
at_inv_cons_ge	at_inv_cons_ge
minuss	minuss
minuss_inv_nil1_aux	minuss_inv_nil1_aux
minuss_inv_nil1	minuss_inv_nil1
minuss_inv_cons1_aux	minuss_inv_cons1_aux
minuss_inv_cons1	minuss_inv_cons1
minuss_inv_cons1_ge	minuss_inv_cons1_ge
minuss_inv_cons1_lt	minuss_inv_cons1_lt
liftv	liftv
liftv_inv_nil1_aux	liftv_inv_nil1_aux
liftv_inv_nil1	liftv_inv_nil1
liftv_inv_cons1_aux	liftv_inv_cons1_aux
liftv_inv_cons1	liftv_inv_cons1
liftv_total	liftv_total
pluss	pluss
pluss_inv_nil2	pluss_inv_nil2
pluss_inv_cons2	pluss_inv_cons2
lifts	lifts
lifts_inv_nil_aux	lifts_inv_nil_aux
lifts_inv_nil	lifts_inv_nil
lifts_inv_cons_aux	lifts_inv_cons_aux
lifts_inv_cons	lifts_inv_cons
lifts_inv_sort1	lifts_inv_sort1
lifts_inv_lref1	lifts_inv_lref1
lifts_inv_gref1	lifts_inv_gref1
lifts_inv_bind1	lifts_inv_bind1
lifts_inv_flat1	lifts_inv_flat1
lifts_simple_dx	lifts_simple_dx
lifts_simple_sn	lifts_simple_sn
lifts_bind	lifts_bind
lifts_flat	lifts_flat
lifts_total	lifts_total
liftsv	liftsv
lifts_inv_applv1	lifts_inv_applv1
lifts_applv	lifts_applv
drops	drops
d_liftable1	d_liftable1
d_liftables1	d_liftables1
d_liftables1_all	d_liftables1_all
drops_inv_nil_aux	drops_inv_nil_aux
drops_inv_nil	drops_inv_nil
drops_inv_cons_aux	drops_inv_cons_aux
drops_inv_cons	drops_inv_cons
drops_inv_skip2	drops_inv_skip2
drops_skip	drops_skip
d1_liftable_liftables	d1_liftable_liftables
d1_liftables_liftables_all	d1_liftables_liftables_all
aaa_lifts	aaa_lifts
aaa_fqu_conf	aaa_fqu_conf
aaa_fquq_conf	aaa_fquq_conf
aaa_fqup_conf	aaa_fqup_conf
aaa_fqus_conf	aaa_fqus_conf
lsubd	lsubd
lsubd_fwd_lsubr	lsubd_fwd_lsubr
lsubd_inv_atom1_aux	lsubd_inv_atom1_aux
lsubd_inv_atom1	lsubd_inv_atom1
lsubd_inv_pair1_aux	lsubd_inv_pair1_aux
lsubd_inv_pair1	lsubd_inv_pair1
lsubd_inv_atom2_aux	lsubd_inv_atom2_aux
lsubd_inv_atom2	lsubd_inv_atom2
lsubd_inv_pair2_aux	lsubd_inv_pair2_aux
lsubd_inv_pair2	lsubd_inv_pair2
lsubd_refl	lsubd_refl
lsubd_drop_O1_conf	lsubd_drop_O1_conf
lsubd_drop_O1_trans	lsubd_drop_O1_trans
lsubd_da_trans	lsubd_da_trans
lsubd_da_conf	lsubd_da_conf
lsubd_trans	lsubd_trans
aaa_da	aaa_da
llpx_sn	llpx_sn
llpx_sn_inv_bind_aux	llpx_sn_inv_bind_aux
llpx_sn_inv_bind	llpx_sn_inv_bind
llpx_sn_inv_flat_aux	llpx_sn_inv_flat_aux
llpx_sn_inv_flat	llpx_sn_inv_flat
llpx_sn_fwd_length	llpx_sn_fwd_length
llpx_sn_fwd_drop_sn	llpx_sn_fwd_drop_sn
llpx_sn_fwd_drop_dx	llpx_sn_fwd_drop_dx
llpx_sn_fwd_lref_aux	llpx_sn_fwd_lref_aux
llpx_sn_fwd_lref	llpx_sn_fwd_lref
llpx_sn_fwd_bind_sn	llpx_sn_fwd_bind_sn
llpx_sn_fwd_bind_dx	llpx_sn_fwd_bind_dx
llpx_sn_fwd_flat_sn	llpx_sn_fwd_flat_sn
llpx_sn_fwd_flat_dx	llpx_sn_fwd_flat_dx
llpx_sn_fwd_pair_sn	llpx_sn_fwd_pair_sn
llpx_sn_refl	llpx_sn_refl
llpx_sn_Y	llpx_sn_Y
llpx_sn_ge_up	llpx_sn_ge_up
llpx_sn_ge	llpx_sn_ge
llpx_sn_bind_O	llpx_sn_bind_O
llpx_sn_co	llpx_sn_co
lreq_llpx_sn_trans	lreq_llpx_sn_trans
llpx_sn_lreq_trans	llpx_sn_lreq_trans
llpx_sn_lreq_repl	llpx_sn_lreq_repl
llpx_sn_bind_repl_SO	llpx_sn_bind_repl_SO
llpx_sn_fwd_lref_dx	llpx_sn_fwd_lref_dx
llpx_sn_fwd_lref_sn	llpx_sn_fwd_lref_sn
llpx_sn_inv_lref_ge_dx	llpx_sn_inv_lref_ge_dx
llpx_sn_inv_lref_ge_sn	llpx_sn_inv_lref_ge_sn
llpx_sn_inv_lref_ge_bi	llpx_sn_inv_lref_ge_bi
llpx_sn_inv_S_aux	llpx_sn_inv_S_aux
llpx_sn_inv_S	llpx_sn_inv_S
llpx_sn_inv_bind_O	llpx_sn_inv_bind_O
llpx_sn_fwd_bind_O_dx	llpx_sn_fwd_bind_O_dx
llpx_sn_bind_repl_O	llpx_sn_bind_repl_O
llpx_sn_dec	llpx_sn_dec
llpx_sn_lift_le	llpx_sn_lift_le
llpx_sn_lift_ge	llpx_sn_lift_ge
llpx_sn_inv_lift_le	llpx_sn_inv_lift_le
llpx_sn_inv_lift_be	llpx_sn_inv_lift_be
llpx_sn_inv_lift_ge	llpx_sn_inv_lift_ge
llpx_sn_inv_lift_O	llpx_sn_inv_lift_O
llpx_sn_drop_conf_O	llpx_sn_drop_conf_O
llpx_sn_drop_trans_O	llpx_sn_drop_trans_O
nllpx_sn_inv_bind	nllpx_sn_inv_bind
nllpx_sn_inv_flat	nllpx_sn_inv_flat
nllpx_sn_inv_bind_O	nllpx_sn_inv_bind_O
ceq	ceq
lleq	lleq
lleq_transitive	lleq_transitive
lleq_ind	lleq_ind
lleq_inv_bind	lleq_inv_bind
lleq_inv_flat	lleq_inv_flat
lleq_fwd_length	lleq_fwd_length
lleq_fwd_lref	lleq_fwd_lref
lleq_fwd_drop_sn	lleq_fwd_drop_sn
lleq_fwd_drop_dx	lleq_fwd_drop_dx
lleq_fwd_bind_sn	lleq_fwd_bind_sn
lleq_fwd_bind_dx	lleq_fwd_bind_dx
lleq_fwd_flat_sn	lleq_fwd_flat_sn
lleq_fwd_flat_dx	lleq_fwd_flat_dx
lleq_sort	lleq_sort
lleq_skip	lleq_skip
lleq_lref	lleq_lref
lleq_free	lleq_free
lleq_gref	lleq_gref
lleq_bind	lleq_bind
lleq_flat	lleq_flat
lleq_refl	lleq_refl
lleq_Y	lleq_Y
lleq_sym	lleq_sym
lleq_ge_up	lleq_ge_up
lleq_ge	lleq_ge
lleq_bind_O	lleq_bind_O
llpx_sn_lrefl	llpx_sn_lrefl
lleq_bind_repl_O	lleq_bind_repl_O
lleq_dec	lleq_dec
lleq_llpx_sn_trans	lleq_llpx_sn_trans
lleq_llpx_sn_conf	lleq_llpx_sn_conf
lleq_inv_lref_ge_dx	lleq_inv_lref_ge_dx
lleq_inv_lref_ge_sn	lleq_inv_lref_ge_sn
lleq_inv_lref_ge_bi	lleq_inv_lref_ge_bi
lleq_inv_lref_ge	lleq_inv_lref_ge
lleq_inv_S	lleq_inv_S
lleq_inv_bind_O	lleq_inv_bind_O
lleq_fwd_lref_dx	lleq_fwd_lref_dx
lleq_fwd_lref_sn	lleq_fwd_lref_sn
lleq_fwd_bind_O_dx	lleq_fwd_bind_O_dx
lleq_lift_le	lleq_lift_le
lleq_lift_ge	lleq_lift_ge
lleq_inv_lift_le	lleq_inv_lift_le
lleq_inv_lift_be	lleq_inv_lift_be
lleq_inv_lift_ge	lleq_inv_lift_ge
nlleq_inv_bind	nlleq_inv_bind
nlleq_inv_flat	nlleq_inv_flat
nlleq_inv_bind_O	nlleq_inv_bind_O
lleq_aaa_trans	lleq_aaa_trans
aaa_lleq_conf	aaa_lleq_conf
lsuba_trans	lsuba_trans
ri2	ri2
ib2	ib2
crr	crr
crr_inv_sort_aux	crr_inv_sort_aux
crr_inv_sort	crr_inv_sort
crr_inv_lref_aux	crr_inv_lref_aux
crr_inv_lref	crr_inv_lref
crr_inv_gref_aux	crr_inv_gref_aux
crr_inv_gref	crr_inv_gref
trr_inv_atom	trr_inv_atom
crr_inv_ib2_aux	crr_inv_ib2_aux
crr_inv_ib2	crr_inv_ib2
crr_inv_appl_aux	crr_inv_appl_aux
crr_inv_appl	crr_inv_appl
cir	cir
cir_inv_delta	cir_inv_delta
cir_inv_ri2	cir_inv_ri2
cir_inv_ib2	cir_inv_ib2
cir_inv_bind	cir_inv_bind
cir_inv_appl	cir_inv_appl
cir_inv_flat	cir_inv_flat
cir_sort	cir_sort
cir_gref	cir_gref
tir_atom	tir_atom
cir_ib2	cir_ib2
cir_appl	cir_appl
crx	crx
crr_crx	crr_crx
crx_inv_sort_aux	crx_inv_sort_aux
crx_inv_sort	crx_inv_sort
crx_inv_lref_aux	crx_inv_lref_aux
crx_inv_lref	crx_inv_lref
crx_inv_gref_aux	crx_inv_gref_aux
crx_inv_gref	crx_inv_gref
trx_inv_atom	trx_inv_atom
crx_inv_ib2_aux	crx_inv_ib2_aux
crx_inv_ib2	crx_inv_ib2
crx_inv_appl_aux	crx_inv_appl_aux
crx_inv_appl	crx_inv_appl
cix	cix
cix_inv_sort	cix_inv_sort
cix_inv_delta	cix_inv_delta
cix_inv_ri2	cix_inv_ri2
cix_inv_ib2	cix_inv_ib2
cix_inv_bind	cix_inv_bind
cix_inv_appl	cix_inv_appl
cix_inv_flat	cix_inv_flat
cix_inv_cir	cix_inv_cir
cix_sort	cix_sort
tix_lref	tix_lref
cix_gref	cix_gref
cix_ib2	cix_ib2
cix_appl	cix_appl
cpx_fwd_cix	cpx_fwd_cix
nlift_lref_be_SO	nlift_lref_be_SO
nlift_bind_sn	nlift_bind_sn
nlift_bind_dx	nlift_bind_dx
nlift_flat_sn	nlift_flat_sn
nlift_flat_dx	nlift_flat_dx
nlift_inv_lref_be_SO	nlift_inv_lref_be_SO
nlift_inv_bind	nlift_inv_bind
nlift_inv_flat	nlift_inv_flat
frees	frees
frees_trans	frees_trans
frees_inv	frees_inv
frees_inv_sort	frees_inv_sort
frees_inv_gref	frees_inv_gref
frees_inv_lref	frees_inv_lref
frees_inv_lref_free	frees_inv_lref_free
frees_inv_lref_skip	frees_inv_lref_skip
frees_inv_lref_ge	frees_inv_lref_ge
frees_inv_lref_lt	frees_inv_lref_lt
frees_inv_bind	frees_inv_bind
frees_inv_flat	frees_inv_flat
frees_lref_eq	frees_lref_eq
frees_lref_be	frees_lref_be
frees_bind_sn	frees_bind_sn
frees_bind_dx	frees_bind_dx
frees_flat_sn	frees_flat_sn
frees_flat_dx	frees_flat_dx
frees_weak	frees_weak
frees_inv_bind_O	frees_inv_bind_O
frees_dec	frees_dec
frees_S	frees_S
frees_bind_dx_O	frees_bind_dx_O
frees_lift_ge	frees_lift_ge
frees_inv_lift_be	frees_inv_lift_be
frees_inv_lift_ge	frees_inv_lift_ge
append	append
d_appendable_sn	d_appendable_sn
append_atom_sn	append_atom_sn
append_assoc	append_assoc
append_length	append_length
ltail_length	ltail_length
lpair_ltail	lpair_ltail
append_inj_sn	append_inj_sn
append_inj_dx	append_inj_dx
append_inv_refl_dx	append_inv_refl_dx
append_inv_pair_dx	append_inv_pair_dx
length_inv_pos_dx_ltail	length_inv_pos_dx_ltail
length_inv_pos_sn_ltail	length_inv_pos_sn_ltail
lenv_ind_alt	lenv_ind_alt
drop_O1_append_sn_le_aux	drop_O1_append_sn_le_aux
drop_O1_append_sn_le	drop_O1_append_sn_le
drop_O1_inv_append1_ge	drop_O1_inv_append1_ge
drop_O1_inv_append1_le	drop_O1_inv_append1_le
frees_append	frees_append
frees_inv_append_aux	frees_inv_append_aux
frees_inv_append	frees_inv_append
llor	llor
llor_atom	llor_atom
llor_tail_frees	llor_tail_frees
llor_tail_cofrees	llor_tail_cofrees
llor_skip	llor_skip
llor_total	llor_total
lpx_sn_alt	lpx_sn_alt
lpx_sn_alt_fwd_length	lpx_sn_alt_fwd_length
lpx_sn_alt_inv_atom1	lpx_sn_alt_inv_atom1
lpx_sn_alt_inv_pair1	lpx_sn_alt_inv_pair1
lpx_sn_alt_inv_atom2	lpx_sn_alt_inv_atom2
lpx_sn_alt_inv_pair2	lpx_sn_alt_inv_pair2
lpx_sn_alt_atom	lpx_sn_alt_atom
lpx_sn_alt_pair	lpx_sn_alt_pair
lpx_sn_lpx_sn_alt	lpx_sn_lpx_sn_alt
lpx_sn_alt_inv_lpx_sn	lpx_sn_alt_inv_lpx_sn
lpx_sn_intro_alt	lpx_sn_intro_alt
lpx_sn_inv_alt	lpx_sn_inv_alt
llpx_sn_alt_r	llpx_sn_alt_r
llpx_sn_alt_r_intro_alt	llpx_sn_alt_r_intro_alt
llpx_sn_alt_r_ind_alt	llpx_sn_alt_r_ind_alt
llpx_sn_alt_r_inv_alt	llpx_sn_alt_r_inv_alt
llpx_sn_alt_r_inv_flat	llpx_sn_alt_r_inv_flat
llpx_sn_alt_r_inv_bind	llpx_sn_alt_r_inv_bind
llpx_sn_alt_r_fwd_length	llpx_sn_alt_r_fwd_length
llpx_sn_alt_r_fwd_lref	llpx_sn_alt_r_fwd_lref
llpx_sn_alt_r_sort	llpx_sn_alt_r_sort
llpx_sn_alt_r_gref	llpx_sn_alt_r_gref
llpx_sn_alt_r_skip	llpx_sn_alt_r_skip
llpx_sn_alt_r_free	llpx_sn_alt_r_free
llpx_sn_alt_r_lref	llpx_sn_alt_r_lref
llpx_sn_alt_r_flat	llpx_sn_alt_r_flat
llpx_sn_alt_r_bind	llpx_sn_alt_r_bind
llpx_sn_lpx_sn_alt_r	llpx_sn_lpx_sn_alt_r
llpx_sn_alt_r_inv_lpx_sn	llpx_sn_alt_r_inv_lpx_sn
llpx_sn_intro_alt_r	llpx_sn_intro_alt_r
llpx_sn_ind_alt_r	llpx_sn_ind_alt_r
llpx_sn_inv_alt_r	llpx_sn_inv_alt_r
llpx_sn_alt	llpx_sn_alt
llpx_sn_llpx_sn_alt	llpx_sn_llpx_sn_alt
llpx_sn_alt_inv_llpx_sn	llpx_sn_alt_inv_llpx_sn
lleq_intro_alt	lleq_intro_alt
lleq_inv_alt	lleq_inv_alt
llpx_sn_llor_fwd_sn	llpx_sn_llor_fwd_sn
lpx_sn_llpx_sn	lpx_sn_llpx_sn
lreq_lleq_trans	lreq_lleq_trans
lleq_lreq_trans	lleq_lreq_trans
lleq_lreq_repl	lleq_lreq_repl
lleq_bind_repl_SO	lleq_bind_repl_SO
llpx_sn_frees_trans_aux	llpx_sn_frees_trans_aux
llpx_sn_frees_trans	llpx_sn_frees_trans
llpx_sn_llor_dx	llpx_sn_llor_dx
llpx_sn_llor_dx_sym	llpx_sn_llor_dx_sym
lreq_cpx_trans	lreq_cpx_trans
cpx_llpx_sn_conf	cpx_llpx_sn_conf
lleq_cpx_trans	lleq_cpx_trans
cpx_lleq_conf	cpx_lleq_conf
cpx_lleq_conf_sn	cpx_lleq_conf_sn
cpx_lleq_conf_dx	cpx_lleq_conf_dx
lreq_frees_trans	lreq_frees_trans
frees_lreq_conf	frees_lreq_conf
lpx_cpx_frees_trans	lpx_cpx_frees_trans
cpx_frees_trans	cpx_frees_trans
lpx_frees_trans	lpx_frees_trans
lleq_lpx_trans	lleq_lpx_trans
lpx_lleq_fqu_trans	lpx_lleq_fqu_trans
lpx_lleq_fquq_trans	lpx_lleq_fquq_trans
lpx_lleq_fqup_trans	lpx_lleq_fqup_trans
lpx_lleq_fqus_trans	lpx_lleq_fqus_trans
lreq_lpx_trans_lleq_aux	lreq_lpx_trans_lleq_aux
lreq_lpx_trans_lleq	lreq_lpx_trans_lleq
cnx_inv_crx	cnx_inv_crx
fleq	fleq
fleq_refl	fleq_refl
fleq_sym	fleq_sym
fleq_inv_gen	fleq_inv_gen
lleq_fqu_trans	lleq_fqu_trans
lleq_fquq_trans	lleq_fquq_trans
lleq_fqup_trans	lleq_fqup_trans
lleq_fqus_trans	lleq_fqus_trans
lleq_trans	lleq_trans
lleq_canc_sn	lleq_canc_sn
lleq_canc_dx	lleq_canc_dx
lleq_nlleq_trans	lleq_nlleq_trans
nlleq_lleq_div	nlleq_lleq_div
fpb	fpb
cpr_fpb	cpr_fpb
lpr_fpb	lpr_fpb
lleq_fpb_trans	lleq_fpb_trans
fleq_fpb_trans	fleq_fpb_trans
fpb_inv_fleq	fpb_inv_fleq
fpbq	fpbq
fpbq_refl	fpbq_refl
cpr_fpbq	cpr_fpbq
lpr_fpbq	lpr_fpbq
fpbqa	fpbqa
fleq_fpbq	fleq_fpbq
fpb_fpbq	fpb_fpbq
fpbq_fpbqa	fpbq_fpbqa
fpbqa_inv_fpbq	fpbqa_inv_fpbq
fpbq_ind_alt	fpbq_ind_alt
fpb_fpbq_alt	fpb_fpbq_alt
fpbq_inv_fpb_alt	fpbq_inv_fpb_alt
fpbq_aaa_conf	fpbq_aaa_conf
cpr_fwd_cir	cpr_fwd_cir
sta_fpb	sta_fpb
crr_lift	crr_lift
crr_inv_lift	crr_inv_lift
cir_lift	cir_lift
cir_inv_lift	cir_inv_lift
cpr_llpx_sn_conf	cpr_llpx_sn_conf
crx_lift	crx_lift
crx_inv_lift	crx_inv_lift
cnx_lift	cnx_lift
cnx_inv_lift	cnx_inv_lift
cnr_inv_crr	cnr_inv_crr
cnr_lref_abst	cnr_lref_abst
cnr_lift	cnr_lift
cnr_inv_lift	cnr_inv_lift
cir_cnr	cir_cnr
cnr_inv_cir	cnr_inv_cir
cix_lref	cix_lref
cix_lift	cix_lift
cix_inv_lift	cix_inv_lift
sta_fpbq	sta_fpbq
cix_cnx	cix_cnx
cnx_inv_cix	cnx_inv_cix
lstas_llpx_sn_conf	lstas_llpx_sn_conf
unfold	unfold
lsuby	lsuby
lsuby_pair_lt	lsuby_pair_lt
lsuby_succ_lt	lsuby_succ_lt
lsuby_pair_O_Y	lsuby_pair_O_Y
lsuby_refl	lsuby_refl
lsuby_O2	lsuby_O2
lsuby_sym	lsuby_sym
lsuby_inv_atom1_aux	lsuby_inv_atom1_aux
lsuby_inv_atom1	lsuby_inv_atom1
lsuby_inv_zero1_aux	lsuby_inv_zero1_aux
lsuby_inv_zero1	lsuby_inv_zero1
lsuby_inv_pair1_aux	lsuby_inv_pair1_aux
lsuby_inv_pair1	lsuby_inv_pair1
lsuby_inv_succ1_aux	lsuby_inv_succ1_aux
lsuby_inv_succ1	lsuby_inv_succ1
lsuby_inv_zero2_aux	lsuby_inv_zero2_aux
lsuby_inv_zero2	lsuby_inv_zero2
lsuby_inv_pair2_aux	lsuby_inv_pair2_aux
lsuby_inv_pair2	lsuby_inv_pair2
lsuby_inv_succ2_aux	lsuby_inv_succ2_aux
lsuby_inv_succ2	lsuby_inv_succ2
lsuby_fwd_length	lsuby_fwd_length
lsuby_drop_trans_be	lsuby_drop_trans_be
cpy	cpy
lsuby_cpy_trans	lsuby_cpy_trans
cpy_refl	cpy_refl
cpy_full	cpy_full
cpy_weak	cpy_weak
cpy_weak_top	cpy_weak_top
cpy_weak_full	cpy_weak_full
cpy_split_up	cpy_split_up
cpy_split_down	cpy_split_down
cpy_fwd_up	cpy_fwd_up
cpy_fwd_tw	cpy_fwd_tw
cpy_inv_atom1_aux	cpy_inv_atom1_aux
cpy_inv_atom1	cpy_inv_atom1
cpy_inv_sort1	cpy_inv_sort1
cpy_inv_lref1	cpy_inv_lref1
cpy_inv_gref1	cpy_inv_gref1
cpy_inv_bind1_aux	cpy_inv_bind1_aux
cpy_inv_bind1	cpy_inv_bind1
cpy_inv_flat1_aux	cpy_inv_flat1_aux
cpy_inv_flat1	cpy_inv_flat1
cpy_inv_refl_O2_aux	cpy_inv_refl_O2_aux
cpy_inv_refl_O2	cpy_inv_refl_O2
cpy_inv_lift1_eq	cpy_inv_lift1_eq
cpy_lift_le	cpy_lift_le
cpy_lift_be	cpy_lift_be
cpy_lift_ge	cpy_lift_ge
cpy_inv_lift1_le	cpy_inv_lift1_le
cpy_inv_lift1_be	cpy_inv_lift1_be
cpy_inv_lift1_ge	cpy_inv_lift1_ge
cpy_inv_lift1_ge_up	cpy_inv_lift1_ge_up
cpy_inv_lift1_be_up	cpy_inv_lift1_be_up
cpy_inv_lift1_le_up	cpy_inv_lift1_le_up
cpy_conf_eq	cpy_conf_eq
cpy_conf_neq	cpy_conf_neq
cpy_trans_ge	cpy_trans_ge
cpy_trans_down	cpy_trans_down
cpy_fwd_nlift2_ge	cpy_fwd_nlift2_ge
gget	gget
gget_inv_gt	gget_inv_gt
gget_inv_eq	gget_inv_eq
gget_inv_lt_aux	gget_inv_lt_aux
gget_inv_lt	gget_inv_lt
gget_total	gget_total
gget_mono	gget_mono
gget_dec	gget_dec
lsuby_trans	lsuby_trans
liftv_mono	liftv_mono
csx	csx
csx_ind	csx_ind
csx_intro	csx_intro
csx_cpx_trans	csx_cpx_trans
cnx_csx	cnx_csx
csx_sort	csx_sort
csx_cast	csx_cast
csx_fwd_pair_sn_aux	csx_fwd_pair_sn_aux
csx_fwd_pair_sn	csx_fwd_pair_sn
csx_fwd_bind_dx_aux	csx_fwd_bind_dx_aux
csx_fwd_bind_dx	csx_fwd_bind_dx
csx_fwd_flat_dx_aux	csx_fwd_flat_dx_aux
csx_fwd_flat_dx	csx_fwd_flat_dx
csx_fwd_bind	csx_fwd_bind
csx_fwd_flat	csx_fwd_flat
cpre	cpre
csx_cpre	csx_cpre
cpre_mono	cpre_mono
lpxs	lpxs
lpxs_ind	lpxs_ind
lpxs_ind_dx	lpxs_ind_dx
lprs_lpxs	lprs_lpxs
lpx_lpxs	lpx_lpxs
lpxs_refl	lpxs_refl
lpxs_strap1	lpxs_strap1
lpxs_strap2	lpxs_strap2
lpxs_pair_refl	lpxs_pair_refl
lpxs_inv_atom1	lpxs_inv_atom1
lpxs_inv_atom2	lpxs_inv_atom2
lpxs_fwd_length	lpxs_fwd_length
fpbs	fpbs
fpbs_ind	fpbs_ind
fpbs_ind_dx	fpbs_ind_dx
fpbs_refl	fpbs_refl
fpbq_fpbs	fpbq_fpbs
fpbs_strap1	fpbs_strap1
fpbs_strap2	fpbs_strap2
fqup_fpbs	fqup_fpbs
fqus_fpbs	fqus_fpbs
cpxs_fpbs	cpxs_fpbs
lpxs_fpbs	lpxs_fpbs
lleq_fpbs	lleq_fpbs
cprs_fpbs	cprs_fpbs
lprs_fpbs	lprs_fpbs
fpbs_fqus_trans	fpbs_fqus_trans
fpbs_fqup_trans	fpbs_fqup_trans
fpbs_cpxs_trans	fpbs_cpxs_trans
fpbs_lpxs_trans	fpbs_lpxs_trans
fpbs_lleq_trans	fpbs_lleq_trans
fqus_fpbs_trans	fqus_fpbs_trans
cpxs_fpbs_trans	cpxs_fpbs_trans
lpxs_fpbs_trans	lpxs_fpbs_trans
lleq_fpbs_trans	lleq_fpbs_trans
cpxs_fqus_fpbs	cpxs_fqus_fpbs
cpxs_fqup_fpbs	cpxs_fqup_fpbs
fqus_lpxs_fpbs	fqus_lpxs_fpbs
cpxs_fqus_lpxs_fpbs	cpxs_fqus_lpxs_fpbs
lpxs_lleq_fpbs	lpxs_lleq_fpbs
cpr_lpr_fpbs	cpr_lpr_fpbs
fpbg	fpbg
fpb_fpbg	fpb_fpbg
fpbg_fpbq_trans	fpbg_fpbq_trans
sta_fpbg	sta_fpbg
csx_lleq_conf	csx_lleq_conf
csx_lleq_trans	csx_lleq_trans
fpbs_trans	fpbs_trans
lreq_cpxs_trans	lreq_cpxs_trans
lpxs_drop_conf	lpxs_drop_conf
drop_lpxs_trans	drop_lpxs_trans
lpxs_drop_trans_O1	lpxs_drop_trans_O1
lpxs_pair	lpxs_pair
lpxs_inv_pair1	lpxs_inv_pair1
lpxs_inv_pair2	lpxs_inv_pair2
lpxs_ind_alt	lpxs_ind_alt
lpxs_cpx_trans	lpxs_cpx_trans
lpxs_cpxs_trans	lpxs_cpxs_trans
cpxs_bind2	cpxs_bind2
cpxs_inv_abst1	cpxs_inv_abst1
cpxs_inv_abbr1	cpxs_inv_abbr1
lpxs_pair2	lpxs_pair2
lpx_fqup_trans	lpx_fqup_trans
lpx_fqus_trans	lpx_fqus_trans
lpxs_fquq_trans	lpxs_fquq_trans
lpxs_fqup_trans	lpxs_fqup_trans
lpxs_fqus_trans	lpxs_fqus_trans
lleq_lpxs_trans	lleq_lpxs_trans
lpxs_nlleq_inv_step_sn	lpxs_nlleq_inv_step_sn
lpxs_lleq_fqu_trans	lpxs_lleq_fqu_trans
lpxs_lleq_fquq_trans	lpxs_lleq_fquq_trans
lpxs_lleq_fqup_trans	lpxs_lleq_fqup_trans
lpxs_lleq_fqus_trans	lpxs_lleq_fqus_trans
lreq_lpxs_trans_lleq_aux	lreq_lpxs_trans_lleq_aux
lreq_lpxs_trans_lleq	lreq_lpxs_trans_lleq
lstas_fpbs	lstas_fpbs
sta_fpbs	sta_fpbs
cpr_lpr_sta_fpbs	cpr_lpr_sta_fpbs
fleq_trans	fleq_trans
fleq_canc_sn	fleq_canc_sn
fleq_canc_dx	fleq_canc_dx
fpbg_fleq_trans	fpbg_fleq_trans
fleq_fpbg_trans	fleq_fpbg_trans
fleq_fpbs	fleq_fpbs
fpbg_fwd_fpbs	fpbg_fwd_fpbs
fpbs_fpbg	fpbs_fpbg
fpbs_fpb_trans	fpbs_fpb_trans
fpb_fpbg_trans	fpb_fpbg_trans
fpbq_fpbg_trans	fpbq_fpbg_trans
fpbs_fpbg_trans	fpbs_fpbg_trans
fpbg_fpbs_trans	fpbg_fpbs_trans
fqup_fpbg	fqup_fpbg
cpxs_fpbg	cpxs_fpbg
lstas_fpbg	lstas_fpbg
lpxs_fpbg	lpxs_fpbg
fsb	fsb
fsb_ind_alt	fsb_ind_alt
fsb_inv_csx	fsb_inv_csx
fsba	fsba
fsba_ind_alt	fsba_ind_alt
fsba_fpbs_trans	fsba_fpbs_trans
fsb_fsba	fsb_fsba
fsba_inv_fsb	fsba_inv_fsb
fsb_fpbs_trans	fsb_fpbs_trans
fsb_ind_fpbg	fsb_ind_fpbg
lpxs_trans	lpxs_trans
lsx	lsx
lsx_ind	lsx_ind
lsx_intro	lsx_intro
lsx_atom	lsx_atom
lsx_sort	lsx_sort
lsx_gref	lsx_gref
lsx_ge_up	lsx_ge_up
lsx_ge	lsx_ge
lsx_fwd_bind_sn	lsx_fwd_bind_sn
lsx_fwd_flat_sn	lsx_fwd_flat_sn
lsx_fwd_flat_dx	lsx_fwd_flat_dx
lsx_fwd_pair_sn	lsx_fwd_pair_sn
lsx_inv_flat	lsx_inv_flat
lsxa	lsxa
lsxa_ind	lsxa_ind
lsxa_intro	lsxa_intro
lsxa_intro_aux	lsxa_intro_aux
lsxa_lleq_trans	lsxa_lleq_trans
lsxa_lpxs_trans	lsxa_lpxs_trans
lsxa_intro_lpx	lsxa_intro_lpx
lsx_lsxa	lsx_lsxa
lsxa_inv_lsx	lsxa_inv_lsx
lsx_intro_alt	lsx_intro_alt
lsx_lpxs_trans	lsx_lpxs_trans
lsx_ind_alt	lsx_ind_alt
lsx_bind_lpxs_aux	lsx_bind_lpxs_aux
lsx_bind	lsx_bind
lsx_flat_lpxs	lsx_flat_lpxs
lsx_flat	lsx_flat
tsts	tsts
tsts_inv_atom1_aux	tsts_inv_atom1_aux
tsts_inv_atom1	tsts_inv_atom1
tsts_inv_pair1_aux	tsts_inv_pair1_aux
tsts_inv_pair1	tsts_inv_pair1
tsts_inv_atom2_aux	tsts_inv_atom2_aux
tsts_inv_atom2	tsts_inv_atom2
tsts_inv_pair2_aux	tsts_inv_pair2_aux
tsts_inv_pair2	tsts_inv_pair2
tsts_refl	tsts_refl
tsts_sym	tsts_sym
tsts_dec	tsts_dec
simple_tsts_repl_dx	simple_tsts_repl_dx
simple_tsts_repl_sn	simple_tsts_repl_sn
tsts_trans	tsts_trans
tsts_canc_sn	tsts_canc_sn
tsts_canc_dx	tsts_canc_dx
csxa	csxa
csxa_ind	csxa_ind
csx_intro_cpxs	csx_intro_cpxs
csxa_intro	csxa_intro
csxa_intro_aux	csxa_intro_aux
csxa_cpxs_trans	csxa_cpxs_trans
csxa_intro_cpx	csxa_intro_cpx
csx_csxa	csx_csxa
csxa_csx	csxa_csx
csx_cpxs_trans	csx_cpxs_trans
csx_ind_alt	csx_ind_alt
nf	nf
candidate	candidate
CP0	CP0
CP1	CP1
CP2	CP2
CP3	CP3
gcp	gcp
gcp0_lifts	gcp0_lifts
gcp2_lifts	gcp2_lifts
gcp2_lifts_all	gcp2_lifts_all
csx_lift	csx_lift
csx_inv_lift	csx_inv_lift
csx_inv_lref_bind	csx_inv_lref_bind
csx_lref_bind	csx_lref_bind
csx_appl_simple	csx_appl_simple
csx_fqu_conf	csx_fqu_conf
csx_fquq_conf	csx_fquq_conf
csx_fqup_conf	csx_fqup_conf
csx_fqus_conf	csx_fqus_conf
csx_gcp	csx_gcp
csx_lpx_conf	csx_lpx_conf
csx_abst	csx_abst
csx_abbr	csx_abbr
csx_appl_beta_aux	csx_appl_beta_aux
csx_appl_beta	csx_appl_beta
csx_appl_theta_aux	csx_appl_theta_aux
csx_appl_theta	csx_appl_theta
csx_appl_simple_tsts	csx_appl_simple_tsts
csx_lpxs_conf	csx_lpxs_conf
lsx_lref_free	lsx_lref_free
lsx_lref_skip	lsx_lref_skip
lsx_fwd_lref_be	lsx_fwd_lref_be
lsx_lift_le	lsx_lift_le
lsx_lift_ge	lsx_lift_ge
lsx_inv_lift_le	lsx_inv_lift_le
lsx_inv_lift_be	lsx_inv_lift_be
lsx_inv_lift_ge	lsx_inv_lift_ge
lsx_lleq_trans	lsx_lleq_trans
lsx_lpx_trans	lsx_lpx_trans
lsx_lreq_conf	lsx_lreq_conf
lsx_fwd_bind_dx	lsx_fwd_bind_dx
lsx_inv_bind	lsx_inv_bind
lcosx	lcosx
lcosx_O	lcosx_O
lcosx_drop_trans_lt	lcosx_drop_trans_lt
lcosx_inv_succ_aux	lcosx_inv_succ_aux
lcosx_inv_succ	lcosx_inv_succ
lcosx_inv_pair	lcosx_inv_pair
lsx_cpx_trans_lcosx	lsx_cpx_trans_lcosx
lsx_cpx_trans_O	lsx_cpx_trans_O
lsx_lref_be_lpxs	lsx_lref_be_lpxs
lsx_lref_be	lsx_lref_be
csx_lsx	csx_lsx
fpbs_aaa_conf	fpbs_aaa_conf
at_mono	at_mono
lifts_lift_trans_le	lifts_lift_trans_le
lifts_lift_trans	lifts_lift_trans
liftsv_liftv_trans_le	liftsv_liftv_trans_le
drops_drop_trans	drops_drop_trans
S1	S1
S2	S2
S3	S3
S4	S4
S5	S5
S6	S6
S7	S7
gcr	gcr
cfun	cfun
acr	acr
gcr_lift	gcr_lift
gcr_lifts	gcr_lifts
acr_gcr	acr_gcr
acr_abst	acr_abst
cpxs_fwd_cnx	cpxs_fwd_cnx
cpxs_fwd_sort	cpxs_fwd_sort
cpxs_fwd_beta	cpxs_fwd_beta
cpxs_fwd_delta	cpxs_fwd_delta
cpxs_fwd_theta	cpxs_fwd_theta
cpxs_fwd_cast	cpxs_fwd_cast
lleq_cpxs_trans	lleq_cpxs_trans
cpxs_lleq_conf	cpxs_lleq_conf
cpxs_lleq_conf_dx	cpxs_lleq_conf_dx
cpxs_lleq_conf_sn	cpxs_lleq_conf_sn
lprs_drop_conf	lprs_drop_conf
drop_lprs_trans	drop_lprs_trans
lprs_drop_trans_O1	lprs_drop_trans_O1
fpbg_trans	fpbg_trans
scpds_lift	scpds_lift
scpds_inv_lift1	scpds_inv_lift1
lifts_trans	lifts_trans
drops_trans	drops_trans
lsubc	lsubc
lsubc_inv_atom1_aux	lsubc_inv_atom1_aux
lsubc_inv_atom1	lsubc_inv_atom1
lsubc_inv_pair1_aux	lsubc_inv_pair1_aux
lsubc_inv_pair1	lsubc_inv_pair1
lsubc_inv_atom2_aux	lsubc_inv_atom2_aux
lsubc_inv_atom2	lsubc_inv_atom2
lsubc_inv_pair2_aux	lsubc_inv_pair2_aux
lsubc_inv_pair2	lsubc_inv_pair2
lsubc_fwd_lsubr	lsubc_fwd_lsubr
lsubc_refl	lsubc_refl
lsubc_drop_O1_trans	lsubc_drop_O1_trans
drop_lsubc_trans	drop_lsubc_trans
drops_lsubc_trans	drops_lsubc_trans
acr_aaa_csubc_lifts	acr_aaa_csubc_lifts
acr_aaa	acr_aaa
gcr_aaa	gcr_aaa
tsts_inv_bind_applv_simple	tsts_inv_bind_applv_simple
cpxs_fwd_cnx_vector	cpxs_fwd_cnx_vector
cpxs_fwd_sort_vector	cpxs_fwd_sort_vector
cpxs_fwd_beta_vector	cpxs_fwd_beta_vector
cpxs_fwd_delta_vector	cpxs_fwd_delta_vector
cpxs_fwd_theta_vector	cpxs_fwd_theta_vector
cpxs_fwd_cast_vector	cpxs_fwd_cast_vector
csxv	csxv
csxv_inv_cons	csxv_inv_cons
csx_fwd_applv	csx_fwd_applv
csx_applv_cnx	csx_applv_cnx
csx_applv_sort	csx_applv_sort
csx_applv_beta	csx_applv_beta
csx_applv_delta	csx_applv_delta
csx_applv_theta	csx_applv_theta
csx_applv_cast	csx_applv_cast
csx_gcr	csx_gcr
aaa_csx	aaa_csx
aaa_ind_csx_aux	aaa_ind_csx_aux
aaa_ind_csx	aaa_ind_csx
aaa_ind_csx_alt_aux	aaa_ind_csx_alt_aux
aaa_ind_csx_alt	aaa_ind_csx_alt
lprs_strip	lprs_strip
lprs_conf	lprs_conf
lprs_trans	lprs_trans
fpbsa	fpbsa
fpb_fpbsa_trans	fpb_fpbsa_trans
fpbs_fpbsa	fpbs_fpbsa
fpbsa_inv_fpbs	fpbsa_inv_fpbs
fpbs_intro_alt	fpbs_intro_alt
fpbs_inv_alt	fpbs_inv_alt
fpbs_cpx_trans_neq	fpbs_cpx_trans_neq
fpb_fpbs	fpb_fpbs
csx_fpb_conf	csx_fpb_conf
csx_fpbs_conf	csx_fpbs_conf
csx_fsb_fpbs	csx_fsb_fpbs
csx_fsb	csx_fsb
csx_ind_fpb	csx_ind_fpb
csx_ind_fpbg	csx_ind_fpbg
aaa_fsb	aaa_fsb
aaa_fsba	aaa_fsba
aaa_ind_fpb_aux	aaa_ind_fpb_aux
aaa_ind_fpb	aaa_ind_fpb
aaa_ind_fpbg_aux	aaa_ind_fpbg_aux
aaa_ind_fpbg	aaa_ind_fpbg
cpxe	cpxe
csx_cpxe	csx_cpxe
lpxs_aaa_conf	lpxs_aaa_conf
lprs_aaa_conf	lprs_aaa_conf
lsuba_lsubc	lsuba_lsubc
ApplDelta	ApplDelta
ApplOmega1	ApplOmega1
ApplOmega2	ApplOmega2
ApplOmega3	ApplOmega3
ApplDelta_lift	ApplDelta_lift
cpr_ApplOmega_12	cpr_ApplOmega_12
cpr_ApplOmega_23	cpr_ApplOmega_23
cpxs_ApplOmega_13	cpxs_ApplOmega_13
fqup_ApplOmega_13	fqup_ApplOmega_13
fpbg_refl	fpbg_refl
Delta	Delta
Omega1	Omega1
Omega2	Omega2
Delta_lift	Delta_lift
cpr_Omega_12	cpr_Omega_12
cpr_Omega_21	cpr_Omega_21
sta_ldec	sta_ldec
snv	snv
snv_inv_lref_aux	snv_inv_lref_aux
snv_inv_lref	snv_inv_lref
snv_inv_gref_aux	snv_inv_gref_aux
snv_inv_gref	snv_inv_gref
snv_inv_bind_aux	snv_inv_bind_aux
snv_inv_bind	snv_inv_bind
snv_inv_appl_aux	snv_inv_appl_aux
snv_inv_appl	snv_inv_appl
snv_inv_cast_aux	snv_inv_cast_aux
snv_inv_cast	snv_inv_cast
snv_extended	snv_extended
snv_restricted	snv_restricted
snv_fwd_aaa	snv_fwd_aaa
snv_fwd_da	snv_fwd_da
snv_fwd_lstas	snv_fwd_lstas
snv_fwd_fsb	snv_fwd_fsb
snv_lift	snv_lift
snv_inv_lift	snv_inv_lift
snv_fqu_conf	snv_fqu_conf
snv_fquq_conf	snv_fquq_conf
snv_fqup_conf	snv_fqup_conf
snv_fqus_conf	snv_fqus_conf
IH_snv_cpr_lpr	IH_snv_cpr_lpr
IH_da_cpr_lpr	IH_da_cpr_lpr
IH_lstas_cpr_lpr	IH_lstas_cpr_lpr
IH_snv_lstas	IH_snv_lstas
snv_cprs_lpr_aux	snv_cprs_lpr_aux
da_cprs_lpr_aux	da_cprs_lpr_aux
da_scpds_lpr_aux	da_scpds_lpr_aux
da_scpes_aux	da_scpes_aux
lstas_cprs_lpr_aux	lstas_cprs_lpr_aux
scpds_cpr_lpr_aux	scpds_cpr_lpr_aux
scpes_cpr_lpr_aux	scpes_cpr_lpr_aux
lstas_scpds_aux	lstas_scpds_aux
scpes_le_aux	scpes_le_aux
snv_cast_scpes	snv_cast_scpes
shnv	shnv
shnv_inv_cast_aux	shnv_inv_cast_aux
shnv_inv_cast	shnv_inv_cast
shnv_inv_snv	shnv_inv_snv
snv_shnv_cast	snv_shnv_cast
lsubsv	lsubsv
lsubsv_inv_atom1_aux	lsubsv_inv_atom1_aux
lsubsv_inv_atom1	lsubsv_inv_atom1
lsubsv_inv_pair1_aux	lsubsv_inv_pair1_aux
lsubsv_inv_pair1	lsubsv_inv_pair1
lsubsv_inv_atom2_aux	lsubsv_inv_atom2_aux
lsubsv_inv_atom2	lsubsv_inv_atom2
lsubsv_inv_pair2_aux	lsubsv_inv_pair2_aux
lsubsv_inv_pair2	lsubsv_inv_pair2
lsubsv_fwd_lsubr	lsubsv_fwd_lsubr
lsubsv_refl	lsubsv_refl
lsubsv_cprs_trans	lsubsv_cprs_trans
lsubsv_drop_O1_conf	lsubsv_drop_O1_conf
lsubsv_drop_O1_trans	lsubsv_drop_O1_trans
lsubsv_fwd_lsubd	lsubsv_fwd_lsubd
lsubsv_lstas_trans	lsubsv_lstas_trans
lsubsv_sta_trans	lsubsv_sta_trans
lsubsv_scpds_trans	lsubsv_scpds_trans
lsubsv_snv_trans	lsubsv_snv_trans
snv_cpr_lpr_aux	snv_cpr_lpr_aux
lstas_cpr_lpr_aux	lstas_cpr_lpr_aux
snv_lstas_aux	snv_lstas_aux
lsubsv_fwd_lsuba	lsubsv_fwd_lsuba
da_cpr_lpr_aux	da_cpr_lpr_aux
lsubsv_cpcs_trans	lsubsv_cpcs_trans
snv_preserve	snv_preserve
da_cpr_lpr	da_cpr_lpr
snv_cpr_lpr	snv_cpr_lpr
snv_lstas	snv_lstas
lstas_cpr_lpr	lstas_cpr_lpr
snv_cprs_lpr	snv_cprs_lpr
da_cprs_lpr	da_cprs_lpr
lstas_cprs_lpr	lstas_cprs_lpr
lstas_cpcs_lpr	lstas_cpcs_lpr
cpys	cpys
cpys_ind	cpys_ind
cpys_ind_dx	cpys_ind_dx
cpy_cpys	cpy_cpys
cpys_strap1	cpys_strap1
cpys_strap2	cpys_strap2
lsuby_cpys_trans	lsuby_cpys_trans
cpys_refl	cpys_refl
cpys_bind	cpys_bind
cpys_flat	cpys_flat
cpys_weak	cpys_weak
cpys_weak_top	cpys_weak_top
cpys_weak_full	cpys_weak_full
cpys_fwd_up	cpys_fwd_up
cpys_fwd_tw	cpys_fwd_tw
cpys_inv_sort1	cpys_inv_sort1
cpys_inv_gref1	cpys_inv_gref1
cpys_inv_bind1	cpys_inv_bind1
cpys_inv_flat1	cpys_inv_flat1
cpys_inv_refl_O2	cpys_inv_refl_O2
cpys_inv_lift1_eq	cpys_inv_lift1_eq
cpys_subst	cpys_subst
cpys_subst_Y2	cpys_subst_Y2
cpys_inv_atom1	cpys_inv_atom1
cpys_inv_lref1	cpys_inv_lref1
cpys_inv_lref1_Y2	cpys_inv_lref1_Y2
cpys_inv_lref1_drop	cpys_inv_lref1_drop
cpys_lift_le	cpys_lift_le
cpys_lift_be	cpys_lift_be
cpys_lift_ge	cpys_lift_ge
cpys_inv_lift1_le	cpys_inv_lift1_le
cpys_inv_lift1_be	cpys_inv_lift1_be
cpys_inv_lift1_ge	cpys_inv_lift1_ge
cpys_inv_lift1_ge_up	cpys_inv_lift1_ge_up
cpys_inv_lift1_be_up	cpys_inv_lift1_be_up
cpys_inv_lift1_le_up	cpys_inv_lift1_le_up
cpys_inv_lift1_subst	cpys_inv_lift1_subst
cpysa	cpysa
lsuby_cpysa_trans	lsuby_cpysa_trans
cpysa_refl	cpysa_refl
cpysa_cpy_trans	cpysa_cpy_trans
cpys_cpysa	cpys_cpysa
cpysa_inv_cpys	cpysa_inv_cpys
cpys_ind_alt	cpys_ind_alt
cpys_inv_SO2	cpys_inv_SO2
cpys_strip_eq	cpys_strip_eq
cpys_strip_neq	cpys_strip_neq
cpys_strap1_down	cpys_strap1_down
cpys_strap2_down	cpys_strap2_down
cpys_split_up	cpys_split_up
cpys_inv_lift1_up	cpys_inv_lift1_up
cpys_conf_eq	cpys_conf_eq
cpys_conf_neq	cpys_conf_neq
cpys_trans_eq	cpys_trans_eq
cpys_trans_down	cpys_trans_down
cpys_antisym_eq	cpys_antisym_eq
llpx_sn_TC_pair_dx	llpx_sn_TC_pair_dx
fqup_trans	fqup_trans
lleq_intro_alt_r	lleq_intro_alt_r
lleq_ind_alt_r	lleq_ind_alt_r
lleq_inv_alt_r	lleq_inv_alt_r

$\lambda\delta rainbow rule$

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

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/matita/lambdadelta/basic_2/ (core Î»Î´ version 2)

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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 $\lambda\delta butterfly$ +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

Version 2A1	Version 2A2
aarity	aarity
destruct_apair_apair_aux	destruct_apair_apair_aux
discr_apair_xy_x	discr_apair_xy_x
discr_tpair_xy_y	discr_apair_xy_y
eq_aarity_dec	eq_aarity_dec
item0	item0
bind2	bind2
flat2	flat2
item2	item2
destruct_sort_sort_aux	destruct_sort_sort_aux
eq_item0_dec	eq_item0_dec
eq_bind2_dec	eq_bind2_dec
eq_flat2_dec	eq_flat2_dec
eq_item2_dec	eq_item2_dec
sh	sh
sh_N	sh_N
nexts_le	nexts_le
nexts_lt	nexts_lt
nexts_dec	nexts_dec
nexts_inj	nexts_inj
sd	sd
deg_O	deg_O
sd_O	sd_O
deg_SO	deg_SO
deg_SO_inv_pos_aux	deg_SO_inv_succ_aux
deg_SO_inv_pos	deg_SO_inv_succ
deg_SO_refl	deg_SO_refl
deg_SO_gt	deg_SO_gt
sd_SO	sd_SO
sd_d	sd_d
deg_inv_pred	deg_inv_pred
deg_inv_prec	deg_inv_prec
deg_iter	deg_iter
deg_next_SO	deg_next_SO
sd_d_SS	sd_d_SS
sd_d_correct	sd_d_correct
term	term
eq_term_dec	eq_term_dec
destruct_tatom_tatom_aux	destruct_tatom_tatom_aux
destruct_tpair_tpair_aux	destruct_tpair_tpair_aux
discr_tpair_xy_x	discr_tpair_xy_x
discr_tpair_xy_y	discr_tpair_xy_y
eq_false_inv_tpair_sn	eq_false_inv_tpair_sn
eq_false_inv_tpair_dx	eq_false_inv_tpair_dx
tw	tw
tw_pos	tw_pos
simple	simple
simple_inv_bind_aux	simple_inv_bind_aux
simple_inv_bind	simple_inv_bind
simple_inv_pair	simple_inv_pair
lenv	lenv
eq_lenv_dec	eq_lenv_dec
destruct_lpair_lpair_aux	destruct_lpair_lpair_aux
discr_lpair_x_xy	discr_lpair_x_xy
+	discr_lpair_xy_x
+	ceq
+	cfull
lw	lw
lw_pair	lw_pair
length	length
length_inv_zero_dx	length_inv_zero_dx
length_inv_zero_sn	length_inv_zero_sn
length_inv_pos_dx	length_inv_succ_dx
length_inv_pos_sn	length_inv_succ_sn
+	length_atom
+	length_pair
genv	genv
eq_genv_dec	eq_genv_dec
rfw	rfw
rfw_shift	rfw_shift
rfw_tpair_sn	rfw_tpair_sn
rfw_tpair_dx	rfw_tpair_dx
rfw_lpair_sn	rfw_lpair_sn
rfw_lpair_dx	rfw_lpair_dx
da	da
da_inv_sort_aux	da_inv_sort_aux
da_inv_sort	da_inv_sort
da_inv_lref_aux	da_inv_lref_aux
da_inv_lref	da_inv_lref
da_inv_gref_aux	da_inv_gref_aux
da_inv_gref	da_inv_gref
da_inv_bind_aux	da_inv_bind_aux
da_inv_bind	da_inv_bind
da_inv_flat_aux	da_inv_flat_aux
da_inv_flat	da_inv_flat
lstas	lstas
lstas_inv_sort1_aux	lstas_inv_sort1_aux
lstas_inv_sort1	lstas_inv_sort1
lstas_inv_lref1_aux	lstas_inv_lref1_aux
lstas_inv_lref1	lstas_inv_lref1
lstas_inv_lref1_O	lstas_inv_lref1_O
lstas_inv_lref1_S	lstas_inv_lref1_S
lstas_inv_gref1_aux	lstas_inv_gref1_aux
lstas_inv_gref1	lstas_inv_gref1
lstas_inv_bind1_aux	lstas_inv_bind1_aux
lstas_inv_bind1	lstas_inv_bind1
lstas_inv_appl1_aux	lstas_inv_appl1_aux
lstas_inv_appl1	lstas_inv_appl1
lstas_inv_cast1_aux	lstas_inv_cast1_aux
lstas_inv_cast1	lstas_inv_cast1
+	+
lift	lift
lift_inv_O2_aux	lift_inv_O2_aux
lift_inv_O2	lift_inv_O2
lift_inv_sort1_aux	lift_inv_sort1_aux
lift_inv_sort1	lift_inv_sort1
lift_inv_lref1_aux	lift_inv_lref1_aux
lift_inv_lref1	lift_inv_lref1
lift_inv_lref1_lt	lift_inv_lref1_lt
lift_inv_lref1_ge	lift_inv_lref1_ge
lift_inv_gref1_aux	lift_inv_gref1_aux
lift_inv_gref1	lift_inv_gref1
lift_inv_bind1_aux	lift_inv_bind1_aux
lift_inv_bind1	lift_inv_bind1
lift_inv_flat1_aux	lift_inv_flat1_aux
lift_inv_flat1	lift_inv_flat1
lift_inv_sort2_aux	lift_inv_sort2_aux
lift_inv_sort2	lift_inv_sort2
lift_inv_lref2_aux	lift_inv_lref2_aux
lift_inv_lref2	lift_inv_lref2
lift_inv_lref2_lt	lift_inv_lref2_lt
lift_inv_lref2_be	lift_inv_lref2_be
lift_inv_lref2_ge	lift_inv_lref2_ge
lift_inv_gref2_aux	lift_inv_gref2_aux
lift_inv_gref2	lift_inv_gref2
lift_inv_bind2_aux	lift_inv_bind2_aux
lift_inv_bind2	lift_inv_bind2
lift_inv_flat2_aux	lift_inv_flat2_aux
lift_inv_flat2	lift_inv_flat2
lift_inv_pair_xy_x	lift_inv_pair_xy_x
lift_inv_pair_xy_y	lift_inv_pair_xy_y
lift_fwd_pair1	lift_fwd_pair1
lift_fwd_pair2	lift_fwd_pair2
lift_fwd_tw	lift_fwd_tw
lift_simple_dx	lift_simple_dx
lift_simple_sn	lift_simple_sn
lift_lref_ge_minus	lift_lref_ge_minus
lift_lref_ge_minus_eq	lift_lref_ge_minus_eq
lift_refl	lift_refl
lift_total	lift_total
lift_split	lift_split
is_lift_dec	is_lift_dec
drop	drop
d_liftable	d_liftable
d_deliftable_sn	d_deliftable_sn
dropable_sn	dropable_sn
dropable_dx	dropable_dx
drop_inv_atom1_aux	drop_inv_atom1_aux
drop_inv_atom1	drop_inv_atom1
drop_inv_O1_pair1_aux	drop_inv_O1_pair1_aux
drop_inv_O1_pair1	drop_inv_O1_pair1
drop_inv_pair1	drop_inv_pair1
drop_inv_drop1_lt	drop_inv_drop1_lt
drop_inv_drop1	drop_inv_drop1
drop_inv_skip1_aux	drop_inv_skip1_aux
drop_inv_skip1	drop_inv_skip1
drop_inv_O1_pair2	drop_inv_O1_pair2
drop_inv_skip2_aux	drop_inv_skip2_aux
drop_inv_skip2	drop_inv_skip2
drop_inv_O1_gt	drop_inv_O1_gt
drop_refl_atom_O2	drop_refl_atom_O2
drop_refl	drop_refl
drop_drop_lt	drop_drop_lt
drop_skip_lt	drop_skip_lt
drop_O1_le	drop_O1_le
drop_O1_lt	drop_O1_lt
drop_O1_pair	drop_O1_pair
drop_O1_ge	drop_O1_ge
drop_O1_eq	drop_O1_eq
drop_split	drop_split
drop_FT	drop_FT
drop_gen	drop_gen
drop_T	drop_T
d_liftable_LTC	d_liftable_LTC
d_deliftable_sn_LTC	d_deliftable_sn_LTC
dropable_sn_TC	dropable_sn_TC
dropable_dx_TC	dropable_dx_TC
d_deliftable_sn_llstar	d_deliftable_sn_llstar
drop_fwd_drop2	drop_fwd_drop2
drop_fwd_length_ge	drop_fwd_length_ge
drop_fwd_length_le_le	drop_fwd_length_le_le
drop_fwd_length_le_ge	drop_fwd_length_le_ge
drop_fwd_length	drop_fwd_length
drop_fwd_length_minus2	drop_fwd_length_minus2
drop_fwd_length_minus4	drop_fwd_length_minus4
drop_fwd_length_le2	drop_fwd_length_le2
drop_fwd_length_le4	drop_fwd_length_le4
drop_fwd_length_lt2	drop_fwd_length_lt2
drop_fwd_length_lt4	drop_fwd_length_lt4
drop_fwd_length_eq1	drop_fwd_length_eq1
drop_fwd_length_eq2	drop_fwd_length_eq2
drop_fwd_lw	drop_fwd_lw
drop_fwd_lw_lt	drop_fwd_lw_lt
drop_fwd_rfw	drop_fwd_rfw
drop_inv_O2_aux	drop_inv_O2_aux
drop_inv_O2	drop_inv_O2
drop_inv_length_eq	drop_inv_length_eq
drop_inv_refl	drop_inv_refl
drop_inv_FT_aux	drop_inv_FT_aux
drop_inv_FT	drop_inv_FT
drop_inv_gen	drop_inv_gen
drop_inv_T	drop_inv_T
lsubr	lsubr
lsubr_refl	lsubr_refl
lsubr_inv_atom1_aux	lsubr_inv_atom1_aux
lsubr_inv_atom1	lsubr_inv_atom1
lsubr_inv_abst1_aux	lsubr_inv_abst1_aux
lsubr_inv_abst1	lsubr_inv_abst1
lsubr_inv_abbr2_aux	lsubr_inv_abbr2_aux
lsubr_inv_abbr2	lsubr_inv_abbr2
lsubr_fwd_length	lsubr_fwd_length
lsubr_fwd_drop2_pair	lsubr_fwd_drop2_pair
lsubr_fwd_drop2_abbr	lsubr_fwd_drop2_abbr
cpr	cpr
lsubr_cpr_trans	lsubr_cpr_trans
tpr_cpr	tpr_cpr
cpr_refl	cpr_refl
cpr_pair_sn	cpr_pair_sn
cpr_delift	cpr_delift
lstas_cpr_aux	lstas_cpr_aux
lstas_cpr	lstas_cpr
cpr_inv_atom1_aux	cpr_inv_atom1_aux
cpr_inv_atom1	cpr_inv_atom1
cpr_inv_sort1	cpr_inv_sort1
cpr_inv_lref1	cpr_inv_lref1
cpr_inv_gref1	cpr_inv_gref1
cpr_inv_bind1_aux	cpr_inv_bind1_aux
cpr_inv_bind1	cpr_inv_bind1
cpr_inv_abbr1	cpr_inv_abbr1
cpr_inv_abst1	cpr_inv_abst1
cpr_inv_flat1_aux	cpr_inv_flat1_aux
cpr_inv_flat1	cpr_inv_flat1
cpr_inv_appl1	cpr_inv_appl1
cpr_inv_appl1_simple	cpr_inv_appl1_simple
cpr_inv_cast1	cpr_inv_cast1
cpr_fwd_bind1_minus	cpr_fwd_bind1_minus
cnr	cnr
cnr_inv_delta	cnr_inv_delta
cnr_inv_abst	cnr_inv_abst
cnr_inv_abbr	cnr_inv_abbr
cnr_inv_zeta	cnr_inv_zeta
cnr_inv_appl	cnr_inv_appl
cnr_inv_eps	cnr_inv_eps
cnr_sort	cnr_sort
cnr_lref_free	cnr_lref_free
cnr_lref_atom	cnr_lref_atom
cnr_abst	cnr_abst
cnr_appl_simple	cnr_appl_simple
cnr_dec	cnr_dec
cprs	cprs
cprs_ind	cprs_ind
cprs_ind_dx	cprs_ind_dx
cpr_cprs	cpr_cprs
cprs_refl	cprs_refl
cprs_strap1	cprs_strap1
cprs_strap2	cprs_strap2
lsubr_cprs_trans	lsubr_cprs_trans
tprs_cprs	tprs_cprs
cprs_bind_dx	cprs_bind_dx
cprs_flat_dx	cprs_flat_dx
cprs_flat_sn	cprs_flat_sn
cprs_zeta	cprs_zeta
cprs_eps	cprs_eps
cprs_beta_dx	cprs_beta_dx
cprs_theta_dx	cprs_theta_dx
cprs_inv_sort1	cprs_inv_sort1
cprs_inv_cast1	cprs_inv_cast1
cprs_inv_cnr1	cprs_inv_cnr1
scpds	scpds
sta_cprs_scpds	sta_cprs_scpds
lstas_scpds	lstas_scpds
scpds_strap1	scpds_strap1
scpds_fwd_cprs	scpds_fwd_cprs
scpes	scpes
scpds_div	scpds_div
scpes_sym	scpes_sym
lift_inj	lift_inj
lift_div_le	lift_div_le
lift_div_be	lift_div_be
lift_mono	lift_mono
lift_trans_be	lift_trans_be
lift_trans_le	lift_trans_le
lift_trans_ge	lift_trans_ge
lift_conf_O1	lift_conf_O1
lift_conf_be	lift_conf_be
drop_mono	drop_mono
drop_conf_ge	drop_conf_ge
drop_conf_be	drop_conf_be
drop_conf_le	drop_conf_le
drop_trans_ge	drop_trans_ge
drop_trans_le	drop_trans_le
d_liftable_llstar	d_liftable_llstar
drop_conf_lt	drop_conf_lt
drop_trans_lt	drop_trans_lt
drop_trans_ge_comm	drop_trans_ge_comm
drop_conf_div	drop_conf_div
drop_fwd_be	drop_fwd_be
aaa	aaa
aaa_inv_sort_aux	aaa_inv_sort_aux
aaa_inv_sort	aaa_inv_sort
aaa_inv_lref_aux	aaa_inv_lref_aux
aaa_inv_lref	aaa_inv_lref
aaa_inv_gref_aux	aaa_inv_gref_aux
aaa_inv_gref	aaa_inv_gref
aaa_inv_abbr_aux	aaa_inv_abbr_aux
aaa_inv_abbr	aaa_inv_abbr
aaa_inv_abst_aux	aaa_inv_abst_aux
aaa_inv_abst	aaa_inv_abst
aaa_inv_appl_aux	aaa_inv_appl_aux
aaa_inv_appl	aaa_inv_appl
aaa_inv_cast_aux	aaa_inv_cast_aux
aaa_inv_cast	aaa_inv_cast
aaa_lift	aaa_lift
aaa_inv_lift	aaa_inv_lift
aaa_mono	aaa_mono
lsuba	lsuba
lsuba_inv_atom1_aux	lsuba_inv_atom1_aux
lsuba_inv_atom1	lsuba_inv_atom1
lsuba_inv_pair1_aux	lsuba_inv_pair1_aux
lsuba_inv_pair1	lsuba_inv_pair1
lsuba_inv_atom2_aux	lsuba_inv_atom2_aux
lsubc_inv_atom2	lsubc_inv_atom2
lsuba_inv_pair2_aux	lsuba_inv_pair2_aux
lsuba_inv_pair2	lsuba_inv_pair2
lsuba_fwd_lsubr	lsuba_fwd_lsubr
lsuba_refl	lsuba_refl
lsuba_drop_O1_conf	lsuba_drop_O1_conf
lsuba_drop_O1_trans	lsuba_drop_O1_trans
lsuba_aaa_conf	lsuba_aaa_conf
lsuba_aaa_trans	lsuba_aaa_trans
lreq	lreq
lreq_pair_lt	lreq_pair_lt
lreq_succ_lt	lreq_succ_lt
lreq_pair_O_Y	lreq_pair_O_Y
lreq_refl	lreq_refl
lreq_O2	lreq_O2
lreq_sym	lreq_sym
lreq_inv_atom1_aux	lreq_inv_atom1_aux
lreq_inv_atom1	lreq_inv_atom1
lreq_inv_zero1_aux	lreq_inv_zero1_aux
lreq_inv_zero1	lreq_inv_zero1
lreq_inv_pair1_aux	lreq_inv_pair1_aux
lreq_inv_pair1	lreq_inv_pair1
lreq_inv_pair	lreq_inv_pair
lreq_inv_succ1_aux	lreq_inv_succ1_aux
lreq_inv_succ1	lreq_inv_succ1
lreq_inv_atom2	lreq_inv_atom2
lreq_inv_succ	lreq_inv_succ
lreq_inv_zero2	lreq_inv_zero2
lreq_inv_pair2	lreq_inv_pair2
lreq_inv_succ2	lreq_inv_succ2
lreq_fwd_length	lreq_fwd_length
lreq_inv_O_Y_aux	lreq_inv_O_Y_aux
lreq_inv_O_Y	lreq_inv_O_Y
lreq_trans	lreq_trans
lreq_canc_sn	lreq_canc_sn
lreq_canc_dx	lreq_canc_dx
lreq_join	lreq_join
dedropable_sn	dedropable_sn
lreq_drop_trans_be	lreq_drop_trans_be
lreq_drop_conf_be	lreq_drop_conf_be
drop_O1_ex	drop_O1_ex
dedropable_sn_TC	dedropable_sn_TC
drop_O1_inj	drop_O1_inj
lpx_sn	lpx_sn
lpx_sn_refl	lpx_sn_refl
lpx_sn_inv_atom1_aux	lpx_sn_inv_atom1_aux
lpx_sn_inv_atom1	lpx_sn_inv_atom1
lpx_sn_inv_pair1_aux	lpx_sn_inv_pair1_aux
lpx_sn_inv_pair1	lpx_sn_inv_pair1
lpx_sn_inv_atom2_aux	lpx_sn_inv_atom2_aux
lpx_sn_inv_atom2	lpx_sn_inv_atom2
lpx_sn_inv_pair2_aux	lpx_sn_inv_pair2_aux
lpx_sn_inv_pair2	lpx_sn_inv_pair2
lpx_sn_inv_pair	lpx_sn_inv_pair
lpx_sn_fwd_length	lpx_sn_fwd_length
lpx_sn_drop_conf	lpx_sn_drop_conf
lpx_sn_drop_trans	lpx_sn_drop_trans
lpx_sn_deliftable_dropable	lpx_sn_deliftable_dropable
lpx_sn_liftable_dedropable	lpx_sn_liftable_dedropable
lpx_sn_dropable_aux	lpx_sn_dropable_aux
lpx_sn_dropable	lpx_sn_dropable
fw	fw
fw_shift	fw_shift
fw_tpair_sn	fw_tpair_sn
fw_tpair_dx	fw_tpair_dx
fw_lpair_sn	fw_lpair_sn
fqu	fqu
fqu_drop_lt	fqu_drop_lt
fqu_lref_S_lt	fqu_lref_S_lt
fqu_fwd_fw	fqu_fwd_fw
fqu_fwd_length_lref1_aux	fqu_fwd_length_lref1_aux
fqu_fwd_length_lref1	fqu_fwd_length_lref1
fqu_inv_eq_aux	fqu_inv_eq_aux
fqu_inv_eq	fqu_inv_eq
fqu_wf_ind	fqu_wf_ind
fquq	fquq
fquq_refl	fquq_refl
fqu_fquq	fqu_fquq
fquq_fwd_fw	fquq_fwd_fw
fquq_fwd_length_lref1_aux	fquq_fwd_length_lref1_aux
fquq_fwd_length_lref1	fquq_fwd_length_lref1
fquqa	fquqa
fquqa_refl	fquqa_refl
fquqa_drop	fquqa_drop
fquq_fquqa	fquq_fquqa
fquqa_inv_fquq	fquqa_inv_fquq
fquq_inv_gen	fquq_inv_gen
fqup	fqup
fqu_fqup	fqu_fqup
fqup_strap1	fqup_strap1
fqup_strap2	fqup_strap2
fqup_drop	fqup_drop
fqup_lref	fqup_lref
fqup_pair_sn	fqup_pair_sn
fqup_bind_dx	fqup_bind_dx
fqup_flat_dx	fqup_flat_dx
fqup_flat_dx_pair_sn	fqup_flat_dx_pair_sn
fqup_bind_dx_flat_dx	fqup_bind_dx_flat_dx
fqup_flat_dx_bind_dx	fqup_flat_dx_bind_dx
fqup_ind	fqup_ind
fqup_ind_dx	fqup_ind_dx
fqup_fwd_fw	fqup_fwd_fw
fqup_wf_ind	fqup_wf_ind
fqup_wf_ind_eq	fqup_wf_ind_eq
fqus	fqus
fqus_ind	fqus_ind
fqus_ind_dx	fqus_ind_dx
fqus_refl	fqus_refl
fquq_fqus	fquq_fqus
fqus_strap1	fqus_strap1
fqus_strap2	fqus_strap2
fqus_drop	fqus_drop
fqup_fqus	fqup_fqus
fqus_fwd_fw	fqus_fwd_fw
fqup_inv_step_sn	fqup_inv_step_sn
fqus_inv_gen	fqus_inv_gen
fqus_strap1_fqu	fqus_strap1_fqu
fqus_strap2_fqu	fqus_strap2_fqu
fqus_fqup_trans	fqus_fqup_trans
fqup_fqus_trans	fqup_fqus_trans
cpx	cpx
lsubr_cpx_trans	lsubr_cpx_trans
cpx_refl	cpx_refl
cpr_cpx	cpr_cpx
cpx_pair_sn	cpx_pair_sn
cpx_delift	cpx_delift
cpx_inv_atom1_aux	cpx_inv_atom1_aux
cpx_inv_atom1	cpx_inv_atom1
cpx_inv_sort1	cpx_inv_sort1
cpx_inv_lref1	cpx_inv_lref1
cpx_inv_lref1_ge	cpx_inv_lref1_ge
cpx_inv_gref1	cpx_inv_gref1
cpx_inv_bind1_aux	cpx_inv_bind1_aux
cpx_inv_bind1	cpx_inv_bind1
cpx_inv_abbr1	cpx_inv_abbr1
cpx_inv_abst1	cpx_inv_abst1
cpx_inv_flat1_aux	cpx_inv_flat1_aux
cpx_inv_flat1	cpx_inv_flat1
cpx_inv_appl1	cpx_inv_appl1
cpx_inv_appl1_simple	cpx_inv_appl1_simple
cpx_inv_cast1	cpx_inv_cast1
cpx_fwd_bind1_minus	cpx_fwd_bind1_minus
sta_cpx_aux	sta_cpx_aux
sta_cpx	sta_cpx
cpx_lift	cpx_lift
cpx_inv_lift1	cpx_inv_lift1
fqu_cpx_trans	fqu_cpx_trans
fqu_sta_trans	fqu_sta_trans
fquq_cpx_trans	fquq_cpx_trans
fquq_sta_trans	fquq_sta_trans
fqup_cpx_trans	fqup_cpx_trans
fqus_cpx_trans	fqus_cpx_trans
fqu_cpx_trans_neq	fqu_cpx_trans_neq
fquq_cpx_trans_neq	fquq_cpx_trans_neq
fqup_cpx_trans_neq	fqup_cpx_trans_neq
fqus_cpx_trans_neq	fqus_cpx_trans_neq
lpr	lpr
lpr_inv_atom1	lpr_inv_atom1
lpr_inv_pair1	lpr_inv_pair1
lpr_inv_atom2	lpr_inv_atom2
lpr_inv_pair2	lpr_inv_pair2
lpr_refl	lpr_refl
lpr_pair	lpr_pair
lpr_fwd_length	lpr_fwd_length
lpx	lpx
lpx_inv_atom1	lpx_inv_atom1
lpx_inv_pair1	lpx_inv_pair1
lpx_inv_atom2	lpx_inv_atom2
lpx_inv_pair2	lpx_inv_pair2
lpx_inv_pair	lpx_inv_pair
lpx_refl	lpx_refl
lpx_pair	lpx_pair
lpr_lpx	lpr_lpx
lpx_fwd_length	lpx_fwd_length
lpx_drop_conf	lpx_drop_conf
drop_lpx_trans	drop_lpx_trans
lpx_drop_trans_O1	lpx_drop_trans_O1
fqu_lpx_trans	fqu_lpx_trans
fquq_lpx_trans	fquq_lpx_trans
lpx_fqu_trans	lpx_fqu_trans
lpx_fquq_trans	lpx_fquq_trans
cpx_lpx_aaa_conf	cpx_lpx_aaa_conf
cpx_aaa_conf	cpx_aaa_conf
lpx_aaa_conf	lpx_aaa_conf
cpr_aaa_conf	cpr_aaa_conf
lpr_aaa_conf	lpr_aaa_conf
cnx	cnx
cnx_inv_sort	cnx_inv_sort
cnx_inv_delta	cnx_inv_delta
cnx_inv_abst	cnx_inv_abst
cnx_inv_abbr	cnx_inv_abbr
cnx_inv_zeta	cnx_inv_zeta
cnx_inv_appl	cnx_inv_appl
cnx_inv_eps	cnx_inv_eps
cnx_fwd_cnr	cnx_fwd_cnr
cnx_sort	cnx_sort
cnx_sort_iter	cnx_sort_iter
cnx_lref_free	cnx_lref_free
cnx_lref_atom	cnx_lref_atom
cnx_abst	cnx_abst
cnx_appl_simple	cnx_appl_simple
cnx_dec	cnx_dec
cpxs	cpxs
cpxs_ind	cpxs_ind
cpxs_ind_dx	cpxs_ind_dx
cpxs_refl	cpxs_refl
cpx_cpxs	cpx_cpxs
cpxs_strap1	cpxs_strap1
cpxs_strap2	cpxs_strap2
lsubr_cpxs_trans	lsubr_cpxs_trans
cprs_cpxs	cprs_cpxs
cpxs_sort	cpxs_sort
cpxs_bind_dx	cpxs_bind_dx
cpxs_flat_dx	cpxs_flat_dx
cpxs_flat_sn	cpxs_flat_sn
cpxs_pair_sn	cpxs_pair_sn
cpxs_zeta	cpxs_zeta
cpxs_eps	cpxs_eps
cpxs_ct	cpxs_ct
cpxs_beta_dx	cpxs_beta_dx
cpxs_theta_dx	cpxs_theta_dx
cpxs_inv_sort1	cpxs_inv_sort1
cpxs_inv_cast1	cpxs_inv_cast1
cpxs_inv_cnx1	cpxs_inv_cnx1
cpxs_neq_inv_step_sn	cpxs_neq_inv_step_sn
cpxs_aaa_conf	cpxs_aaa_conf
cprs_aaa_conf	cprs_aaa_conf
lpx_sn_confluent	lpx_sn_confluent
lpx_sn_transitive	lpx_sn_transitive
lpx_sn_trans	lpx_sn_trans
lpx_sn_conf	lpx_sn_conf
cpr_lift	cpr_lift
cpr_inv_lift1	cpr_inv_lift1
lpr_drop_conf	lpr_drop_conf
drop_lpr_trans	drop_lpr_trans
lpr_drop_trans_O1	lpr_drop_trans_O1
fqu_cpr_trans_dx	fqu_cpr_trans_dx
fquq_cpr_trans_dx	fquq_cpr_trans_dx
fqu_cpr_trans_sn	fqu_cpr_trans_sn
fquq_cpr_trans_sn	fquq_cpr_trans_sn
fqu_lpr_trans	fqu_lpr_trans
fquq_lpr_trans	fquq_lpr_trans
cpr_conf_lpr_atom_atom	cpr_conf_lpr_atom_atom
cpr_conf_lpr_atom_delta	cpr_conf_lpr_atom_delta
cpr_conf_lpr_delta_delta	cpr_conf_lpr_delta_delta
cpr_conf_lpr_bind_bind	cpr_conf_lpr_bind_bind
cpr_conf_lpr_bind_zeta	cpr_conf_lpr_bind_zeta
cpr_conf_lpr_zeta_zeta	cpr_conf_lpr_zeta_zeta
cpr_conf_lpr_flat_flat	cpr_conf_lpr_flat_flat
cpr_conf_lpr_flat_eps	cpr_conf_lpr_flat_eps
cpr_conf_lpr_eps_eps	cpr_conf_lpr_eps_eps
cpr_conf_lpr_flat_beta	cpr_conf_lpr_flat_beta
cpr_conf_lpr_flat_theta	cpr_conf_lpr_flat_theta
cpr_conf_lpr_beta_beta	cpr_conf_lpr_beta_beta
cpr_conf_lpr_theta_theta	cpr_conf_lpr_theta_theta
cpr_conf_lpr	cpr_conf_lpr
cpr_conf	cpr_conf
lpr_cpr_conf_dx	lpr_cpr_conf_dx
lpr_cpr_conf_sn	lpr_cpr_conf_sn
lpr_conf	lpr_conf
cprs_delta	cprs_delta
cprs_inv_lref1	cprs_inv_lref1
cprs_lift	cprs_lift
cprs_inv_lift1	cprs_inv_lift1
cprs_trans	cprs_trans
cprs_conf	cprs_conf
cprs_bind	cprs_bind
cprs_flat	cprs_flat
cprs_beta_rc	cprs_beta_rc
cprs_beta	cprs_beta
cprs_theta_rc	cprs_theta_rc
cprs_theta	cprs_theta
cprs_inv_appl1	cprs_inv_appl1
lpr_cpr_trans	lpr_cpr_trans
cpr_bind2	cpr_bind2
lpr_cprs_trans	lpr_cprs_trans
cprs_strip	cprs_strip
cprs_lpr_conf_dx	cprs_lpr_conf_dx
cprs_lpr_conf_sn	cprs_lpr_conf_sn
cprs_bind2_dx	cprs_bind2_dx
TC_lpx_sn_pair_refl	TC_lpx_sn_pair_refl
TC_lpx_sn_pair	TC_lpx_sn_pair
lpx_sn_LTC_TC_lpx_sn	lpx_sn_LTC_TC_lpx_sn
TC_lpx_sn_inv_atom2	TC_lpx_sn_inv_atom2
TC_lpx_sn_inv_pair2	TC_lpx_sn_inv_pair2
TC_lpx_sn_ind	TC_lpx_sn_ind
TC_lpx_sn_inv_atom1	TC_lpx_sn_inv_atom1
TC_lpx_sn_inv_pair1_aux	TC_lpx_sn_inv_pair1_aux
TC_lpx_sn_inv_pair1	TC_lpx_sn_inv_pair1
TC_lpx_sn_inv_lpx_sn_LTC	TC_lpx_sn_inv_lpx_sn_LTC
TC_lpx_sn_fwd_length	TC_lpx_sn_fwd_length
lprs	lprs
lprs_ind	lprs_ind
lprs_ind_dx	lprs_ind_dx
lpr_lprs	lpr_lprs
lprs_refl	lprs_refl
lprs_strap1	lprs_strap1
lprs_strap2	lprs_strap2
lprs_pair_refl	lprs_pair_refl
lprs_inv_atom1	lprs_inv_atom1
lprs_inv_atom2	lprs_inv_atom2
lprs_fwd_length	lprs_fwd_length
lprs_pair	lprs_pair
lprs_inv_pair1	lprs_inv_pair1
lprs_inv_pair2	lprs_inv_pair2
lprs_ind_alt	lprs_ind_alt
lprs_cpr_trans	lprs_cpr_trans
lprs_cprs_trans	lprs_cprs_trans
lprs_cprs_conf_dx	lprs_cprs_conf_dx
lprs_cpr_conf_dx	lprs_cpr_conf_dx
lprs_cprs_conf_sn	lprs_cprs_conf_sn
lprs_cpr_conf_sn	lprs_cpr_conf_sn
cprs_bind2	cprs_bind2
cprs_inv_abst1	cprs_inv_abst1
cprs_inv_abst	cprs_inv_abst
cprs_inv_abbr1	cprs_inv_abbr1
lprs_pair2	lprs_pair2
cpc	cpc
cpc_refl	cpc_refl
cpc_sym	cpc_sym
cpc_fwd_cpr	cpc_fwd_cpr
cpc_conf	cpc_conf
cpcs	cpcs
cpcs_ind	cpcs_ind
cpcs_ind_dx	cpcs_ind_dx
cpcs_refl	cpcs_refl
cpcs_sym	cpcs_sym
cpc_cpcs	cpc_cpcs
cpcs_strap1	cpcs_strap1
cpcs_strap2	cpcs_strap2
cpr_cpcs_dx	cpr_cpcs_dx
cpr_cpcs_sn	cpr_cpcs_sn
cpcs_cpr_strap1	cpcs_cpr_strap1
cpcs_cpr_strap2	cpcs_cpr_strap2
cpcs_cpr_div	cpcs_cpr_div
cpr_div	cpr_div
cpcs_cpr_conf	cpcs_cpr_conf
cpcs_cprs_dx	cpcs_cprs_dx
cpcs_cprs_sn	cpcs_cprs_sn
cpcs_cprs_strap1	cpcs_cprs_strap1
cpcs_cprs_strap2	cpcs_cprs_strap2
cpcs_cprs_div	cpcs_cprs_div
cpcs_cprs_conf	cpcs_cprs_conf
cprs_div	cprs_div
cprs_cpr_div	cprs_cpr_div
cpr_cprs_div	cpr_cprs_div
cpcs_inv_cprs	cpcs_inv_cprs
cpcs_inv_sort	cpcs_inv_sort
cpcs_inv_abst1	cpcs_inv_abst1
cpcs_inv_abst2	cpcs_inv_abst2
cpcs_inv_sort_abst	cpcs_inv_sort_abst
cpcs_inv_lift	cpcs_inv_lift
lpr_cpcs_trans	lpr_cpcs_trans
lprs_cpcs_trans	lprs_cpcs_trans
cpr_cprs_conf_cpcs	cpr_cprs_conf_cpcs
cprs_cpr_conf_cpcs	cprs_cpr_conf_cpcs
cprs_conf_cpcs	cprs_conf_cpcs
lprs_cprs_conf	lprs_cprs_conf
lpr_cprs_conf	lpr_cprs_conf
lpr_cpr_conf	lpr_cpr_conf
cpcs_flat	cpcs_flat
cpcs_flat_dx_cpr_rev	cpcs_flat_dx_cpr_rev
cpcs_bind_dx	cpcs_bind_dx
cpcs_bind_sn	cpcs_bind_sn
lsubr_cpcs_trans	lsubr_cpcs_trans
cpcs_lift	cpcs_lift
cpcs_strip	cpcs_strip
cpcs_inv_abst_sn	cpcs_inv_abst_sn
cpcs_inv_abst_dx	cpcs_inv_abst_dx
cpcs_trans	cpcs_trans
cpcs_canc_sn	cpcs_canc_sn
cpcs_canc_dx	cpcs_canc_dx
cpcs_bind1	cpcs_bind1
cpcs_bind2	cpcs_bind2
lpr_cpcs_conf	lpr_cpcs_conf
cpcs_aaa_mono	cpcs_aaa_mono
da_lift	da_lift
da_inv_lift	da_inv_lift
da_mono	da_mono
lstas_lift	lstas_lift
lstas_inv_lift1	lstas_inv_lift1
lstas_split_aux	lstas_split_aux
lstas_split	lstas_split
lstas_lstas	lstas_lstas
lstas_trans	lstas_trans
lstas_mono	lstas_mono
lstas_correct	lstas_correct
lstas_conf_le	lstas_conf_le
lstas_conf	lstas_conf
da_lstas	da_lstas
lstas_da_conf	lstas_da_conf
lstas_inv_da	lstas_inv_da
lstas_inv_da_ge	lstas_inv_da_ge
lstas_inv_refl_pos	lstas_inv_refl_pos
fqus_trans	fqus_trans
cpxs_delta	cpxs_delta
lstas_cpxs	lstas_cpxs
cpxs_inv_lref1	cpxs_inv_lref1
cpxs_lift	cpxs_lift
cpxs_inv_lift1	cpxs_inv_lift1
fqu_cpxs_trans	fqu_cpxs_trans
fquq_cpxs_trans	fquq_cpxs_trans
fquq_lstas_trans	fquq_lstas_trans
fqup_cpxs_trans	fqup_cpxs_trans
fqus_cpxs_trans	fqus_cpxs_trans
fqus_lstas_trans	fqus_lstas_trans
cpxs_trans	cpxs_trans
cpxs_bind	cpxs_bind
cpxs_flat	cpxs_flat
cpxs_beta_rc	cpxs_beta_rc
cpxs_beta	cpxs_beta
cpxs_theta_rc	cpxs_theta_rc
cpxs_theta	cpxs_theta
cpxs_inv_appl1	cpxs_inv_appl1
lpx_cpx_trans	lpx_cpx_trans
cpx_bind2	cpx_bind2
lpx_cpxs_trans	lpx_cpxs_trans
cpxs_bind2_dx	cpxs_bind2_dx
fqu_cpxs_trans_neq	fqu_cpxs_trans_neq
fquq_cpxs_trans_neq	fquq_cpxs_trans_neq
fqup_cpxs_trans_neq	fqup_cpxs_trans_neq
fqus_cpxs_trans_neq	fqus_cpxs_trans_neq
scpds_strap2	scpds_strap2
scpds_cprs_trans	scpds_cprs_trans
lstas_scpds_trans	lstas_scpds_trans
scpds_inv_abst1	scpds_inv_abst1
scpds_inv_abbr_abst	scpds_inv_abbr_abst
scpds_inv_lstas_eq	scpds_inv_lstas_eq
scpds_fwd_cpxs	scpds_fwd_cpxs
scpds_conf_eq	scpds_conf_eq
scpes_inv_lstas_eq	scpes_inv_lstas_eq
cpcs_scpes	cpcs_scpes
scpes_inv_abst2	scpes_inv_abst2
scpes_refl	scpes_refl
lstas_scpes_trans	lstas_scpes_trans
cprs_scpds_div	cprs_scpds_div
scpes_trans	scpes_trans
scpes_canc_sn	scpes_canc_sn
scpes_canc_dx	scpes_canc_dx
aaa_lstas	aaa_lstas
lstas_aaa_conf	lstas_aaa_conf
scpds_aaa_conf	scpds_aaa_conf
scpes_aaa_mono	scpes_aaa_mono
lsubr_inv_pair1_aux	lsubr_inv_pair1_aux
lsubr_inv_pair1	lsubr_inv_pair1
lsubr_trans	lsubr_trans
applv	applv
applv_simple	applv_simple
at	at
at_inv_nil_aux	at_inv_nil_aux
at_inv_nil	at_inv_nil
at_inv_cons_aux	at_inv_cons_aux
at_inv_cons	at_inv_cons
at_inv_cons_lt	at_inv_cons_lt
at_inv_cons_ge	at_inv_cons_ge
minuss	minuss
minuss_inv_nil1_aux	minuss_inv_nil1_aux
minuss_inv_nil1	minuss_inv_nil1
minuss_inv_cons1_aux	minuss_inv_cons1_aux
minuss_inv_cons1	minuss_inv_cons1
minuss_inv_cons1_ge	minuss_inv_cons1_ge
minuss_inv_cons1_lt	minuss_inv_cons1_lt
liftv	liftv
liftv_inv_nil1_aux	liftv_inv_nil1_aux
liftv_inv_nil1	liftv_inv_nil1
liftv_inv_cons1_aux	liftv_inv_cons1_aux
liftv_inv_cons1	liftv_inv_cons1
liftv_total	liftv_total
pluss	pluss
pluss_inv_nil2	pluss_inv_nil2
pluss_inv_cons2	pluss_inv_cons2
lifts	lifts
lifts_inv_nil_aux	lifts_inv_nil_aux
lifts_inv_nil	lifts_inv_nil
lifts_inv_cons_aux	lifts_inv_cons_aux
lifts_inv_cons	lifts_inv_cons
lifts_inv_sort1	lifts_inv_sort1
lifts_inv_lref1	lifts_inv_lref1
lifts_inv_gref1	lifts_inv_gref1
lifts_inv_bind1	lifts_inv_bind1
lifts_inv_flat1	lifts_inv_flat1
lifts_simple_dx	lifts_simple_dx
lifts_simple_sn	lifts_simple_sn
lifts_bind	lifts_bind
lifts_flat	lifts_flat
lifts_total	lifts_total
liftsv	liftsv
lifts_inv_applv1	lifts_inv_applv1
lifts_applv	lifts_applv
drops	drops
d_liftable1	d_liftable1
d_liftables1	d_liftables1
d_liftables1_all	d_liftables1_all
drops_inv_nil_aux	drops_inv_nil_aux
drops_inv_nil	drops_inv_nil
drops_inv_cons_aux	drops_inv_cons_aux
drops_inv_cons	drops_inv_cons
drops_inv_skip2	drops_inv_skip2
drops_skip	drops_skip
d1_liftable_liftables	d1_liftable_liftables
d1_liftables_liftables_all	d1_liftables_liftables_all
aaa_lifts	aaa_lifts
aaa_fqu_conf	aaa_fqu_conf
aaa_fquq_conf	aaa_fquq_conf
aaa_fqup_conf	aaa_fqup_conf
aaa_fqus_conf	aaa_fqus_conf
lsubd	lsubd
lsubd_fwd_lsubr	lsubd_fwd_lsubr
lsubd_inv_atom1_aux	lsubd_inv_atom1_aux
lsubd_inv_atom1	lsubd_inv_atom1
lsubd_inv_pair1_aux	lsubd_inv_pair1_aux
lsubd_inv_pair1	lsubd_inv_pair1
lsubd_inv_atom2_aux	lsubd_inv_atom2_aux
lsubd_inv_atom2	lsubd_inv_atom2
lsubd_inv_pair2_aux	lsubd_inv_pair2_aux
lsubd_inv_pair2	lsubd_inv_pair2
lsubd_refl	lsubd_refl
lsubd_drop_O1_conf	lsubd_drop_O1_conf
lsubd_drop_O1_trans	lsubd_drop_O1_trans
lsubd_da_trans	lsubd_da_trans
lsubd_da_conf	lsubd_da_conf
lsubd_trans	lsubd_trans
aaa_da	aaa_da
llpx_sn	llpx_sn
llpx_sn_inv_bind_aux	llpx_sn_inv_bind_aux
llpx_sn_inv_bind	llpx_sn_inv_bind
llpx_sn_inv_flat_aux	llpx_sn_inv_flat_aux
llpx_sn_inv_flat	llpx_sn_inv_flat
llpx_sn_fwd_length	llpx_sn_fwd_length
llpx_sn_fwd_drop_sn	llpx_sn_fwd_drop_sn
llpx_sn_fwd_drop_dx	llpx_sn_fwd_drop_dx
llpx_sn_fwd_lref_aux	llpx_sn_fwd_lref_aux
llpx_sn_fwd_lref	llpx_sn_fwd_lref
llpx_sn_fwd_bind_sn	llpx_sn_fwd_bind_sn
llpx_sn_fwd_bind_dx	llpx_sn_fwd_bind_dx
llpx_sn_fwd_flat_sn	llpx_sn_fwd_flat_sn
llpx_sn_fwd_flat_dx	llpx_sn_fwd_flat_dx
llpx_sn_fwd_pair_sn	llpx_sn_fwd_pair_sn
llpx_sn_refl	llpx_sn_refl
llpx_sn_Y	llpx_sn_Y
llpx_sn_ge_up	llpx_sn_ge_up
llpx_sn_ge	llpx_sn_ge
llpx_sn_bind_O	llpx_sn_bind_O
llpx_sn_co	llpx_sn_co
lreq_llpx_sn_trans	lreq_llpx_sn_trans
llpx_sn_lreq_trans	llpx_sn_lreq_trans
llpx_sn_lreq_repl	llpx_sn_lreq_repl
llpx_sn_bind_repl_SO	llpx_sn_bind_repl_SO
llpx_sn_fwd_lref_dx	llpx_sn_fwd_lref_dx
llpx_sn_fwd_lref_sn	llpx_sn_fwd_lref_sn
llpx_sn_inv_lref_ge_dx	llpx_sn_inv_lref_ge_dx
llpx_sn_inv_lref_ge_sn	llpx_sn_inv_lref_ge_sn
llpx_sn_inv_lref_ge_bi	llpx_sn_inv_lref_ge_bi
llpx_sn_inv_S_aux	llpx_sn_inv_S_aux
llpx_sn_inv_S	llpx_sn_inv_S
llpx_sn_inv_bind_O	llpx_sn_inv_bind_O
llpx_sn_fwd_bind_O_dx	llpx_sn_fwd_bind_O_dx
llpx_sn_bind_repl_O	llpx_sn_bind_repl_O
llpx_sn_dec	llpx_sn_dec
llpx_sn_lift_le	llpx_sn_lift_le
llpx_sn_lift_ge	llpx_sn_lift_ge
llpx_sn_inv_lift_le	llpx_sn_inv_lift_le
llpx_sn_inv_lift_be	llpx_sn_inv_lift_be
llpx_sn_inv_lift_ge	llpx_sn_inv_lift_ge
llpx_sn_inv_lift_O	llpx_sn_inv_lift_O
llpx_sn_drop_conf_O	llpx_sn_drop_conf_O
llpx_sn_drop_trans_O	llpx_sn_drop_trans_O
nllpx_sn_inv_bind	nllpx_sn_inv_bind
nllpx_sn_inv_flat	nllpx_sn_inv_flat
nllpx_sn_inv_bind_O	nllpx_sn_inv_bind_O
ceq	ceq
lleq	lleq
lleq_transitive	lleq_transitive
lleq_ind	lleq_ind
lleq_inv_bind	lleq_inv_bind
lleq_inv_flat	lleq_inv_flat
lleq_fwd_length	lleq_fwd_length
lleq_fwd_lref	lleq_fwd_lref
lleq_fwd_drop_sn	lleq_fwd_drop_sn
lleq_fwd_drop_dx	lleq_fwd_drop_dx
lleq_fwd_bind_sn	lleq_fwd_bind_sn
lleq_fwd_bind_dx	lleq_fwd_bind_dx
lleq_fwd_flat_sn	lleq_fwd_flat_sn
lleq_fwd_flat_dx	lleq_fwd_flat_dx
lleq_sort	lleq_sort
lleq_skip	lleq_skip
lleq_lref	lleq_lref
lleq_free	lleq_free
lleq_gref	lleq_gref
lleq_bind	lleq_bind
lleq_flat	lleq_flat
lleq_refl	lleq_refl
lleq_Y	lleq_Y
lleq_sym	lleq_sym
lleq_ge_up	lleq_ge_up
lleq_ge	lleq_ge
lleq_bind_O	lleq_bind_O
llpx_sn_lrefl	llpx_sn_lrefl
lleq_bind_repl_O	lleq_bind_repl_O
lleq_dec	lleq_dec
lleq_llpx_sn_trans	lleq_llpx_sn_trans
lleq_llpx_sn_conf	lleq_llpx_sn_conf
lleq_inv_lref_ge_dx	lleq_inv_lref_ge_dx
lleq_inv_lref_ge_sn	lleq_inv_lref_ge_sn
lleq_inv_lref_ge_bi	lleq_inv_lref_ge_bi
lleq_inv_lref_ge	lleq_inv_lref_ge
lleq_inv_S	lleq_inv_S
lleq_inv_bind_O	lleq_inv_bind_O
lleq_fwd_lref_dx	lleq_fwd_lref_dx
lleq_fwd_lref_sn	lleq_fwd_lref_sn
lleq_fwd_bind_O_dx	lleq_fwd_bind_O_dx
lleq_lift_le	lleq_lift_le
lleq_lift_ge	lleq_lift_ge
lleq_inv_lift_le	lleq_inv_lift_le
lleq_inv_lift_be	lleq_inv_lift_be
lleq_inv_lift_ge	lleq_inv_lift_ge
nlleq_inv_bind	nlleq_inv_bind
nlleq_inv_flat	nlleq_inv_flat
nlleq_inv_bind_O	nlleq_inv_bind_O
lleq_aaa_trans	lleq_aaa_trans
aaa_lleq_conf	aaa_lleq_conf
lsuba_trans	lsuba_trans
ri2	ri2
ib2	ib2
crr	crr
crr_inv_sort_aux	crr_inv_sort_aux
crr_inv_sort	crr_inv_sort
crr_inv_lref_aux	crr_inv_lref_aux
crr_inv_lref	crr_inv_lref
crr_inv_gref_aux	crr_inv_gref_aux
crr_inv_gref	crr_inv_gref
trr_inv_atom	trr_inv_atom
crr_inv_ib2_aux	crr_inv_ib2_aux
crr_inv_ib2	crr_inv_ib2
crr_inv_appl_aux	crr_inv_appl_aux
crr_inv_appl	crr_inv_appl
cir	cir
cir_inv_delta	cir_inv_delta
cir_inv_ri2	cir_inv_ri2
cir_inv_ib2	cir_inv_ib2
cir_inv_bind	cir_inv_bind
cir_inv_appl	cir_inv_appl
cir_inv_flat	cir_inv_flat
cir_sort	cir_sort
cir_gref	cir_gref
tir_atom	tir_atom
cir_ib2	cir_ib2
cir_appl	cir_appl
crx	crx
crr_crx	crr_crx
crx_inv_sort_aux	crx_inv_sort_aux
crx_inv_sort	crx_inv_sort
crx_inv_lref_aux	crx_inv_lref_aux
crx_inv_lref	crx_inv_lref
crx_inv_gref_aux	crx_inv_gref_aux
crx_inv_gref	crx_inv_gref
trx_inv_atom	trx_inv_atom
crx_inv_ib2_aux	crx_inv_ib2_aux
crx_inv_ib2	crx_inv_ib2
crx_inv_appl_aux	crx_inv_appl_aux
crx_inv_appl	crx_inv_appl
cix	cix
cix_inv_sort	cix_inv_sort
cix_inv_delta	cix_inv_delta
cix_inv_ri2	cix_inv_ri2
cix_inv_ib2	cix_inv_ib2
cix_inv_bind	cix_inv_bind
cix_inv_appl	cix_inv_appl
cix_inv_flat	cix_inv_flat
cix_inv_cir	cix_inv_cir
cix_sort	cix_sort
tix_lref	tix_lref
cix_gref	cix_gref
cix_ib2	cix_ib2
cix_appl	cix_appl
cpx_fwd_cix	cpx_fwd_cix
nlift_lref_be_SO	nlift_lref_be_SO
nlift_bind_sn	nlift_bind_sn
nlift_bind_dx	nlift_bind_dx
nlift_flat_sn	nlift_flat_sn
nlift_flat_dx	nlift_flat_dx
nlift_inv_lref_be_SO	nlift_inv_lref_be_SO
nlift_inv_bind	nlift_inv_bind
nlift_inv_flat	nlift_inv_flat
frees	frees
frees_trans	frees_trans
frees_inv	frees_inv
frees_inv_sort	frees_inv_sort
frees_inv_gref	frees_inv_gref
frees_inv_lref	frees_inv_lref
frees_inv_lref_free	frees_inv_lref_free
frees_inv_lref_skip	frees_inv_lref_skip
frees_inv_lref_ge	frees_inv_lref_ge
frees_inv_lref_lt	frees_inv_lref_lt
frees_inv_bind	frees_inv_bind
frees_inv_flat	frees_inv_flat
frees_lref_eq	frees_lref_eq
frees_lref_be	frees_lref_be
frees_bind_sn	frees_bind_sn
frees_bind_dx	frees_bind_dx
frees_flat_sn	frees_flat_sn
frees_flat_dx	frees_flat_dx
frees_weak	frees_weak
frees_inv_bind_O	frees_inv_bind_O
frees_dec	frees_dec
frees_S	frees_S
frees_bind_dx_O	frees_bind_dx_O
frees_lift_ge	frees_lift_ge
frees_inv_lift_be	frees_inv_lift_be
frees_inv_lift_ge	frees_inv_lift_ge
append	append
d_appendable_sn	d_appendable_sn
append_atom_sn	append_atom_sn
append_assoc	append_assoc
append_length	append_length
ltail_length	ltail_length
lpair_ltail	lpair_ltail
append_inj_sn	append_inj_sn
append_inj_dx	append_inj_dx
append_inv_refl_dx	append_inv_refl_dx
append_inv_pair_dx	append_inv_pair_dx
length_inv_pos_dx_ltail	length_inv_pos_dx_ltail
length_inv_pos_sn_ltail	length_inv_pos_sn_ltail
lenv_ind_alt	lenv_ind_alt
drop_O1_append_sn_le_aux	drop_O1_append_sn_le_aux
drop_O1_append_sn_le	drop_O1_append_sn_le
drop_O1_inv_append1_ge	drop_O1_inv_append1_ge
drop_O1_inv_append1_le	drop_O1_inv_append1_le
frees_append	frees_append
frees_inv_append_aux	frees_inv_append_aux
frees_inv_append	frees_inv_append
llor	llor
llor_atom	llor_atom
llor_tail_frees	llor_tail_frees
llor_tail_cofrees	llor_tail_cofrees
llor_skip	llor_skip
llor_total	llor_total
lpx_sn_alt	lpx_sn_alt
lpx_sn_alt_fwd_length	lpx_sn_alt_fwd_length
lpx_sn_alt_inv_atom1	lpx_sn_alt_inv_atom1
lpx_sn_alt_inv_pair1	lpx_sn_alt_inv_pair1
lpx_sn_alt_inv_atom2	lpx_sn_alt_inv_atom2
lpx_sn_alt_inv_pair2	lpx_sn_alt_inv_pair2
lpx_sn_alt_atom	lpx_sn_alt_atom
lpx_sn_alt_pair	lpx_sn_alt_pair
lpx_sn_lpx_sn_alt	lpx_sn_lpx_sn_alt
lpx_sn_alt_inv_lpx_sn	lpx_sn_alt_inv_lpx_sn
lpx_sn_intro_alt	lpx_sn_intro_alt
lpx_sn_inv_alt	lpx_sn_inv_alt
llpx_sn_alt_r	llpx_sn_alt_r
llpx_sn_alt_r_intro_alt	llpx_sn_alt_r_intro_alt
llpx_sn_alt_r_ind_alt	llpx_sn_alt_r_ind_alt
llpx_sn_alt_r_inv_alt	llpx_sn_alt_r_inv_alt
llpx_sn_alt_r_inv_flat	llpx_sn_alt_r_inv_flat
llpx_sn_alt_r_inv_bind	llpx_sn_alt_r_inv_bind
llpx_sn_alt_r_fwd_length	llpx_sn_alt_r_fwd_length
llpx_sn_alt_r_fwd_lref	llpx_sn_alt_r_fwd_lref
llpx_sn_alt_r_sort	llpx_sn_alt_r_sort
llpx_sn_alt_r_gref	llpx_sn_alt_r_gref
llpx_sn_alt_r_skip	llpx_sn_alt_r_skip
llpx_sn_alt_r_free	llpx_sn_alt_r_free
llpx_sn_alt_r_lref	llpx_sn_alt_r_lref
llpx_sn_alt_r_flat	llpx_sn_alt_r_flat
llpx_sn_alt_r_bind	llpx_sn_alt_r_bind
llpx_sn_lpx_sn_alt_r	llpx_sn_lpx_sn_alt_r
llpx_sn_alt_r_inv_lpx_sn	llpx_sn_alt_r_inv_lpx_sn
llpx_sn_intro_alt_r	llpx_sn_intro_alt_r
llpx_sn_ind_alt_r	llpx_sn_ind_alt_r
llpx_sn_inv_alt_r	llpx_sn_inv_alt_r
llpx_sn_alt	llpx_sn_alt
llpx_sn_llpx_sn_alt	llpx_sn_llpx_sn_alt
llpx_sn_alt_inv_llpx_sn	llpx_sn_alt_inv_llpx_sn
lleq_intro_alt	lleq_intro_alt
lleq_inv_alt	lleq_inv_alt
llpx_sn_llor_fwd_sn	llpx_sn_llor_fwd_sn
lpx_sn_llpx_sn	lpx_sn_llpx_sn
lreq_lleq_trans	lreq_lleq_trans
lleq_lreq_trans	lleq_lreq_trans
lleq_lreq_repl	lleq_lreq_repl
lleq_bind_repl_SO	lleq_bind_repl_SO
llpx_sn_frees_trans_aux	llpx_sn_frees_trans_aux
llpx_sn_frees_trans	llpx_sn_frees_trans
llpx_sn_llor_dx	llpx_sn_llor_dx
llpx_sn_llor_dx_sym	llpx_sn_llor_dx_sym
lreq_cpx_trans	lreq_cpx_trans
cpx_llpx_sn_conf	cpx_llpx_sn_conf
lleq_cpx_trans	lleq_cpx_trans
cpx_lleq_conf	cpx_lleq_conf
cpx_lleq_conf_sn	cpx_lleq_conf_sn
cpx_lleq_conf_dx	cpx_lleq_conf_dx
lreq_frees_trans	lreq_frees_trans
frees_lreq_conf	frees_lreq_conf
lpx_cpx_frees_trans	lpx_cpx_frees_trans
cpx_frees_trans	cpx_frees_trans
lpx_frees_trans	lpx_frees_trans
lleq_lpx_trans	lleq_lpx_trans
lpx_lleq_fqu_trans	lpx_lleq_fqu_trans
lpx_lleq_fquq_trans	lpx_lleq_fquq_trans
lpx_lleq_fqup_trans	lpx_lleq_fqup_trans
lpx_lleq_fqus_trans	lpx_lleq_fqus_trans
lreq_lpx_trans_lleq_aux	lreq_lpx_trans_lleq_aux
lreq_lpx_trans_lleq	lreq_lpx_trans_lleq
cnx_inv_crx	cnx_inv_crx
fleq	fleq
fleq_refl	fleq_refl
fleq_sym	fleq_sym
fleq_inv_gen	fleq_inv_gen
lleq_fqu_trans	lleq_fqu_trans
lleq_fquq_trans	lleq_fquq_trans
lleq_fqup_trans	lleq_fqup_trans
lleq_fqus_trans	lleq_fqus_trans
lleq_trans	lleq_trans
lleq_canc_sn	lleq_canc_sn
lleq_canc_dx	lleq_canc_dx
lleq_nlleq_trans	lleq_nlleq_trans
nlleq_lleq_div	nlleq_lleq_div
fpb	fpb
cpr_fpb	cpr_fpb
lpr_fpb	lpr_fpb
lleq_fpb_trans	lleq_fpb_trans
fleq_fpb_trans	fleq_fpb_trans
fpb_inv_fleq	fpb_inv_fleq
fpbq	fpbq
fpbq_refl	fpbq_refl
cpr_fpbq	cpr_fpbq
lpr_fpbq	lpr_fpbq
fpbqa	fpbqa
fleq_fpbq	fleq_fpbq
fpb_fpbq	fpb_fpbq
fpbq_fpbqa	fpbq_fpbqa
fpbqa_inv_fpbq	fpbqa_inv_fpbq
fpbq_ind_alt	fpbq_ind_alt
fpb_fpbq_alt	fpb_fpbq_alt
fpbq_inv_fpb_alt	fpbq_inv_fpb_alt
fpbq_aaa_conf	fpbq_aaa_conf
cpr_fwd_cir	cpr_fwd_cir
sta_fpb	sta_fpb
crr_lift	crr_lift
crr_inv_lift	crr_inv_lift
cir_lift	cir_lift
cir_inv_lift	cir_inv_lift
cpr_llpx_sn_conf	cpr_llpx_sn_conf
crx_lift	crx_lift
crx_inv_lift	crx_inv_lift
cnx_lift	cnx_lift
cnx_inv_lift	cnx_inv_lift
cnr_inv_crr	cnr_inv_crr
cnr_lref_abst	cnr_lref_abst
cnr_lift	cnr_lift
cnr_inv_lift	cnr_inv_lift
cir_cnr	cir_cnr
cnr_inv_cir	cnr_inv_cir
cix_lref	cix_lref
cix_lift	cix_lift
cix_inv_lift	cix_inv_lift
sta_fpbq	sta_fpbq
cix_cnx	cix_cnx
cnx_inv_cix	cnx_inv_cix
lstas_llpx_sn_conf	lstas_llpx_sn_conf
unfold	unfold
lsuby	lsuby
lsuby_pair_lt	lsuby_pair_lt
lsuby_succ_lt	lsuby_succ_lt
lsuby_pair_O_Y	lsuby_pair_O_Y
lsuby_refl	lsuby_refl
lsuby_O2	lsuby_O2
lsuby_sym	lsuby_sym
lsuby_inv_atom1_aux	lsuby_inv_atom1_aux
lsuby_inv_atom1	lsuby_inv_atom1
lsuby_inv_zero1_aux	lsuby_inv_zero1_aux
lsuby_inv_zero1	lsuby_inv_zero1
lsuby_inv_pair1_aux	lsuby_inv_pair1_aux
lsuby_inv_pair1	lsuby_inv_pair1
lsuby_inv_succ1_aux	lsuby_inv_succ1_aux
lsuby_inv_succ1	lsuby_inv_succ1
lsuby_inv_zero2_aux	lsuby_inv_zero2_aux
lsuby_inv_zero2	lsuby_inv_zero2
lsuby_inv_pair2_aux	lsuby_inv_pair2_aux
lsuby_inv_pair2	lsuby_inv_pair2
lsuby_inv_succ2_aux	lsuby_inv_succ2_aux
lsuby_inv_succ2	lsuby_inv_succ2
lsuby_fwd_length	lsuby_fwd_length
lsuby_drop_trans_be	lsuby_drop_trans_be
cpy	cpy
lsuby_cpy_trans	lsuby_cpy_trans
cpy_refl	cpy_refl
cpy_full	cpy_full
cpy_weak	cpy_weak
cpy_weak_top	cpy_weak_top
cpy_weak_full	cpy_weak_full
cpy_split_up	cpy_split_up
cpy_split_down	cpy_split_down
cpy_fwd_up	cpy_fwd_up
cpy_fwd_tw	cpy_fwd_tw
cpy_inv_atom1_aux	cpy_inv_atom1_aux
cpy_inv_atom1	cpy_inv_atom1
cpy_inv_sort1	cpy_inv_sort1
cpy_inv_lref1	cpy_inv_lref1
cpy_inv_gref1	cpy_inv_gref1
cpy_inv_bind1_aux	cpy_inv_bind1_aux
cpy_inv_bind1	cpy_inv_bind1
cpy_inv_flat1_aux	cpy_inv_flat1_aux
cpy_inv_flat1	cpy_inv_flat1
cpy_inv_refl_O2_aux	cpy_inv_refl_O2_aux
cpy_inv_refl_O2	cpy_inv_refl_O2
cpy_inv_lift1_eq	cpy_inv_lift1_eq
cpy_lift_le	cpy_lift_le
cpy_lift_be	cpy_lift_be
cpy_lift_ge	cpy_lift_ge
cpy_inv_lift1_le	cpy_inv_lift1_le
cpy_inv_lift1_be	cpy_inv_lift1_be
cpy_inv_lift1_ge	cpy_inv_lift1_ge
cpy_inv_lift1_ge_up	cpy_inv_lift1_ge_up
cpy_inv_lift1_be_up	cpy_inv_lift1_be_up
cpy_inv_lift1_le_up	cpy_inv_lift1_le_up
cpy_conf_eq	cpy_conf_eq
cpy_conf_neq	cpy_conf_neq
cpy_trans_ge	cpy_trans_ge
cpy_trans_down	cpy_trans_down
cpy_fwd_nlift2_ge	cpy_fwd_nlift2_ge
gget	gget
gget_inv_gt	gget_inv_gt
gget_inv_eq	gget_inv_eq
gget_inv_lt_aux	gget_inv_lt_aux
gget_inv_lt	gget_inv_lt
gget_total	gget_total
gget_mono	gget_mono
gget_dec	gget_dec
lsuby_trans	lsuby_trans
liftv_mono	liftv_mono
csx	csx
csx_ind	csx_ind
csx_intro	csx_intro
csx_cpx_trans	csx_cpx_trans
cnx_csx	cnx_csx
csx_sort	csx_sort
csx_cast	csx_cast
csx_fwd_pair_sn_aux	csx_fwd_pair_sn_aux
csx_fwd_pair_sn	csx_fwd_pair_sn
csx_fwd_bind_dx_aux	csx_fwd_bind_dx_aux
csx_fwd_bind_dx	csx_fwd_bind_dx
csx_fwd_flat_dx_aux	csx_fwd_flat_dx_aux
csx_fwd_flat_dx	csx_fwd_flat_dx
csx_fwd_bind	csx_fwd_bind
csx_fwd_flat	csx_fwd_flat
cpre	cpre
csx_cpre	csx_cpre
cpre_mono	cpre_mono
lpxs	lpxs
lpxs_ind	lpxs_ind
lpxs_ind_dx	lpxs_ind_dx
lprs_lpxs	lprs_lpxs
lpx_lpxs	lpx_lpxs
lpxs_refl	lpxs_refl
lpxs_strap1	lpxs_strap1
lpxs_strap2	lpxs_strap2
lpxs_pair_refl	lpxs_pair_refl
lpxs_inv_atom1	lpxs_inv_atom1
lpxs_inv_atom2	lpxs_inv_atom2
lpxs_fwd_length	lpxs_fwd_length
fpbs	fpbs
fpbs_ind	fpbs_ind
fpbs_ind_dx	fpbs_ind_dx
fpbs_refl	fpbs_refl
fpbq_fpbs	fpbq_fpbs
fpbs_strap1	fpbs_strap1
fpbs_strap2	fpbs_strap2
fqup_fpbs	fqup_fpbs
fqus_fpbs	fqus_fpbs
cpxs_fpbs	cpxs_fpbs
lpxs_fpbs	lpxs_fpbs
lleq_fpbs	lleq_fpbs
cprs_fpbs	cprs_fpbs
lprs_fpbs	lprs_fpbs
fpbs_fqus_trans	fpbs_fqus_trans
fpbs_fqup_trans	fpbs_fqup_trans
fpbs_cpxs_trans	fpbs_cpxs_trans
fpbs_lpxs_trans	fpbs_lpxs_trans
fpbs_lleq_trans	fpbs_lleq_trans
fqus_fpbs_trans	fqus_fpbs_trans
cpxs_fpbs_trans	cpxs_fpbs_trans
lpxs_fpbs_trans	lpxs_fpbs_trans
lleq_fpbs_trans	lleq_fpbs_trans
cpxs_fqus_fpbs	cpxs_fqus_fpbs
cpxs_fqup_fpbs	cpxs_fqup_fpbs
fqus_lpxs_fpbs	fqus_lpxs_fpbs
cpxs_fqus_lpxs_fpbs	cpxs_fqus_lpxs_fpbs
lpxs_lleq_fpbs	lpxs_lleq_fpbs
cpr_lpr_fpbs	cpr_lpr_fpbs
fpbg	fpbg
fpb_fpbg	fpb_fpbg
fpbg_fpbq_trans	fpbg_fpbq_trans
sta_fpbg	sta_fpbg
csx_lleq_conf	csx_lleq_conf
csx_lleq_trans	csx_lleq_trans
fpbs_trans	fpbs_trans
lreq_cpxs_trans	lreq_cpxs_trans
lpxs_drop_conf	lpxs_drop_conf
drop_lpxs_trans	drop_lpxs_trans
lpxs_drop_trans_O1	lpxs_drop_trans_O1
lpxs_pair	lpxs_pair
lpxs_inv_pair1	lpxs_inv_pair1
lpxs_inv_pair2	lpxs_inv_pair2
lpxs_ind_alt	lpxs_ind_alt
lpxs_cpx_trans	lpxs_cpx_trans
lpxs_cpxs_trans	lpxs_cpxs_trans
cpxs_bind2	cpxs_bind2
cpxs_inv_abst1	cpxs_inv_abst1
cpxs_inv_abbr1	cpxs_inv_abbr1
lpxs_pair2	lpxs_pair2
lpx_fqup_trans	lpx_fqup_trans
lpx_fqus_trans	lpx_fqus_trans
lpxs_fquq_trans	lpxs_fquq_trans
lpxs_fqup_trans	lpxs_fqup_trans
lpxs_fqus_trans	lpxs_fqus_trans
lleq_lpxs_trans	lleq_lpxs_trans
lpxs_nlleq_inv_step_sn	lpxs_nlleq_inv_step_sn
lpxs_lleq_fqu_trans	lpxs_lleq_fqu_trans
lpxs_lleq_fquq_trans	lpxs_lleq_fquq_trans
lpxs_lleq_fqup_trans	lpxs_lleq_fqup_trans
lpxs_lleq_fqus_trans	lpxs_lleq_fqus_trans
lreq_lpxs_trans_lleq_aux	lreq_lpxs_trans_lleq_aux
lreq_lpxs_trans_lleq	lreq_lpxs_trans_lleq
lstas_fpbs	lstas_fpbs
sta_fpbs	sta_fpbs
cpr_lpr_sta_fpbs	cpr_lpr_sta_fpbs
fleq_trans	fleq_trans
fleq_canc_sn	fleq_canc_sn
fleq_canc_dx	fleq_canc_dx
fpbg_fleq_trans	fpbg_fleq_trans
fleq_fpbg_trans	fleq_fpbg_trans
fleq_fpbs	fleq_fpbs
fpbg_fwd_fpbs	fpbg_fwd_fpbs
fpbs_fpbg	fpbs_fpbg
fpbs_fpb_trans	fpbs_fpb_trans
fpb_fpbg_trans	fpb_fpbg_trans
fpbq_fpbg_trans	fpbq_fpbg_trans
fpbs_fpbg_trans	fpbs_fpbg_trans
fpbg_fpbs_trans	fpbg_fpbs_trans
fqup_fpbg	fqup_fpbg
cpxs_fpbg	cpxs_fpbg
lstas_fpbg	lstas_fpbg
lpxs_fpbg	lpxs_fpbg
fsb	fsb
fsb_ind_alt	fsb_ind_alt
fsb_inv_csx	fsb_inv_csx
fsba	fsba
fsba_ind_alt	fsba_ind_alt
fsba_fpbs_trans	fsba_fpbs_trans
fsb_fsba	fsb_fsba
fsba_inv_fsb	fsba_inv_fsb
fsb_fpbs_trans	fsb_fpbs_trans
fsb_ind_fpbg	fsb_ind_fpbg
lpxs_trans	lpxs_trans
lsx	lsx
lsx_ind	lsx_ind
lsx_intro	lsx_intro
lsx_atom	lsx_atom
lsx_sort	lsx_sort
lsx_gref	lsx_gref
lsx_ge_up	lsx_ge_up
lsx_ge	lsx_ge
lsx_fwd_bind_sn	lsx_fwd_bind_sn
lsx_fwd_flat_sn	lsx_fwd_flat_sn
lsx_fwd_flat_dx	lsx_fwd_flat_dx
lsx_fwd_pair_sn	lsx_fwd_pair_sn
lsx_inv_flat	lsx_inv_flat
lsxa	lsxa
lsxa_ind	lsxa_ind
lsxa_intro	lsxa_intro
lsxa_intro_aux	lsxa_intro_aux
lsxa_lleq_trans	lsxa_lleq_trans
lsxa_lpxs_trans	lsxa_lpxs_trans
lsxa_intro_lpx	lsxa_intro_lpx
lsx_lsxa	lsx_lsxa
lsxa_inv_lsx	lsxa_inv_lsx
lsx_intro_alt	lsx_intro_alt
lsx_lpxs_trans	lsx_lpxs_trans
lsx_ind_alt	lsx_ind_alt
lsx_bind_lpxs_aux	lsx_bind_lpxs_aux
lsx_bind	lsx_bind
lsx_flat_lpxs	lsx_flat_lpxs
lsx_flat	lsx_flat
tsts	tsts
tsts_inv_atom1_aux	tsts_inv_atom1_aux
tsts_inv_atom1	tsts_inv_atom1
tsts_inv_pair1_aux	tsts_inv_pair1_aux
tsts_inv_pair1	tsts_inv_pair1
tsts_inv_atom2_aux	tsts_inv_atom2_aux
tsts_inv_atom2	tsts_inv_atom2
tsts_inv_pair2_aux	tsts_inv_pair2_aux
tsts_inv_pair2	tsts_inv_pair2
tsts_refl	tsts_refl
tsts_sym	tsts_sym
tsts_dec	tsts_dec
simple_tsts_repl_dx	simple_tsts_repl_dx
simple_tsts_repl_sn	simple_tsts_repl_sn
tsts_trans	tsts_trans
tsts_canc_sn	tsts_canc_sn
tsts_canc_dx	tsts_canc_dx
csxa	csxa
csxa_ind	csxa_ind
csx_intro_cpxs	csx_intro_cpxs
csxa_intro	csxa_intro
csxa_intro_aux	csxa_intro_aux
csxa_cpxs_trans	csxa_cpxs_trans
csxa_intro_cpx	csxa_intro_cpx
csx_csxa	csx_csxa
csxa_csx	csxa_csx
csx_cpxs_trans	csx_cpxs_trans
csx_ind_alt	csx_ind_alt
nf	nf
candidate	candidate
CP0	CP0
CP1	CP1
CP2	CP2
CP3	CP3
gcp	gcp
gcp0_lifts	gcp0_lifts
gcp2_lifts	gcp2_lifts
gcp2_lifts_all	gcp2_lifts_all
csx_lift	csx_lift
csx_inv_lift	csx_inv_lift
csx_inv_lref_bind	csx_inv_lref_bind
csx_lref_bind	csx_lref_bind
csx_appl_simple	csx_appl_simple
csx_fqu_conf	csx_fqu_conf
csx_fquq_conf	csx_fquq_conf
csx_fqup_conf	csx_fqup_conf
csx_fqus_conf	csx_fqus_conf
csx_gcp	csx_gcp
csx_lpx_conf	csx_lpx_conf
csx_abst	csx_abst
csx_abbr	csx_abbr
csx_appl_beta_aux	csx_appl_beta_aux
csx_appl_beta	csx_appl_beta
csx_appl_theta_aux	csx_appl_theta_aux
csx_appl_theta	csx_appl_theta
csx_appl_simple_tsts	csx_appl_simple_tsts
csx_lpxs_conf	csx_lpxs_conf
lsx_lref_free	lsx_lref_free
lsx_lref_skip	lsx_lref_skip
lsx_fwd_lref_be	lsx_fwd_lref_be
lsx_lift_le	lsx_lift_le
lsx_lift_ge	lsx_lift_ge
lsx_inv_lift_le	lsx_inv_lift_le
lsx_inv_lift_be	lsx_inv_lift_be
lsx_inv_lift_ge	lsx_inv_lift_ge
lsx_lleq_trans	lsx_lleq_trans
lsx_lpx_trans	lsx_lpx_trans
lsx_lreq_conf	lsx_lreq_conf
lsx_fwd_bind_dx	lsx_fwd_bind_dx
lsx_inv_bind	lsx_inv_bind
lcosx	lcosx
lcosx_O	lcosx_O
lcosx_drop_trans_lt	lcosx_drop_trans_lt
lcosx_inv_succ_aux	lcosx_inv_succ_aux
lcosx_inv_succ	lcosx_inv_succ
lcosx_inv_pair	lcosx_inv_pair
lsx_cpx_trans_lcosx	lsx_cpx_trans_lcosx
lsx_cpx_trans_O	lsx_cpx_trans_O
lsx_lref_be_lpxs	lsx_lref_be_lpxs
lsx_lref_be	lsx_lref_be
csx_lsx	csx_lsx
fpbs_aaa_conf	fpbs_aaa_conf
at_mono	at_mono
lifts_lift_trans_le	lifts_lift_trans_le
lifts_lift_trans	lifts_lift_trans
liftsv_liftv_trans_le	liftsv_liftv_trans_le
drops_drop_trans	drops_drop_trans
S1	S1
S2	S2
S3	S3
S4	S4
S5	S5
S6	S6
S7	S7
gcr	gcr
cfun	cfun
acr	acr
gcr_lift	gcr_lift
gcr_lifts	gcr_lifts
acr_gcr	acr_gcr
acr_abst	acr_abst
cpxs_fwd_cnx	cpxs_fwd_cnx
cpxs_fwd_sort	cpxs_fwd_sort
cpxs_fwd_beta	cpxs_fwd_beta
cpxs_fwd_delta	cpxs_fwd_delta
cpxs_fwd_theta	cpxs_fwd_theta
cpxs_fwd_cast	cpxs_fwd_cast
lleq_cpxs_trans	lleq_cpxs_trans
cpxs_lleq_conf	cpxs_lleq_conf
cpxs_lleq_conf_dx	cpxs_lleq_conf_dx
cpxs_lleq_conf_sn	cpxs_lleq_conf_sn
lprs_drop_conf	lprs_drop_conf
drop_lprs_trans	drop_lprs_trans
lprs_drop_trans_O1	lprs_drop_trans_O1
fpbg_trans	fpbg_trans
scpds_lift	scpds_lift
scpds_inv_lift1	scpds_inv_lift1
lifts_trans	lifts_trans
drops_trans	drops_trans
lsubc	lsubc
lsubc_inv_atom1_aux	lsubc_inv_atom1_aux
lsubc_inv_atom1	lsubc_inv_atom1
lsubc_inv_pair1_aux	lsubc_inv_pair1_aux
lsubc_inv_pair1	lsubc_inv_pair1
lsubc_inv_atom2_aux	lsubc_inv_atom2_aux
lsubc_inv_atom2	lsubc_inv_atom2
lsubc_inv_pair2_aux	lsubc_inv_pair2_aux
lsubc_inv_pair2	lsubc_inv_pair2
lsubc_fwd_lsubr	lsubc_fwd_lsubr
lsubc_refl	lsubc_refl
lsubc_drop_O1_trans	lsubc_drop_O1_trans
drop_lsubc_trans	drop_lsubc_trans
drops_lsubc_trans	drops_lsubc_trans
acr_aaa_csubc_lifts	acr_aaa_csubc_lifts
acr_aaa	acr_aaa
gcr_aaa	gcr_aaa
tsts_inv_bind_applv_simple	tsts_inv_bind_applv_simple
cpxs_fwd_cnx_vector	cpxs_fwd_cnx_vector
cpxs_fwd_sort_vector	cpxs_fwd_sort_vector
cpxs_fwd_beta_vector	cpxs_fwd_beta_vector
cpxs_fwd_delta_vector	cpxs_fwd_delta_vector
cpxs_fwd_theta_vector	cpxs_fwd_theta_vector
cpxs_fwd_cast_vector	cpxs_fwd_cast_vector
csxv	csxv
csxv_inv_cons	csxv_inv_cons
csx_fwd_applv	csx_fwd_applv
csx_applv_cnx	csx_applv_cnx
csx_applv_sort	csx_applv_sort
csx_applv_beta	csx_applv_beta
csx_applv_delta	csx_applv_delta
csx_applv_theta	csx_applv_theta
csx_applv_cast	csx_applv_cast
csx_gcr	csx_gcr
aaa_csx	aaa_csx
aaa_ind_csx_aux	aaa_ind_csx_aux
aaa_ind_csx	aaa_ind_csx
aaa_ind_csx_alt_aux	aaa_ind_csx_alt_aux
aaa_ind_csx_alt	aaa_ind_csx_alt
lprs_strip	lprs_strip
lprs_conf	lprs_conf
lprs_trans	lprs_trans
fpbsa	fpbsa
fpb_fpbsa_trans	fpb_fpbsa_trans
fpbs_fpbsa	fpbs_fpbsa
fpbsa_inv_fpbs	fpbsa_inv_fpbs
fpbs_intro_alt	fpbs_intro_alt
fpbs_inv_alt	fpbs_inv_alt
fpbs_cpx_trans_neq	fpbs_cpx_trans_neq
fpb_fpbs	fpb_fpbs
csx_fpb_conf	csx_fpb_conf
csx_fpbs_conf	csx_fpbs_conf
csx_fsb_fpbs	csx_fsb_fpbs
csx_fsb	csx_fsb
csx_ind_fpb	csx_ind_fpb
csx_ind_fpbg	csx_ind_fpbg
aaa_fsb	aaa_fsb
aaa_fsba	aaa_fsba
aaa_ind_fpb_aux	aaa_ind_fpb_aux
aaa_ind_fpb	aaa_ind_fpb
aaa_ind_fpbg_aux	aaa_ind_fpbg_aux
aaa_ind_fpbg	aaa_ind_fpbg
cpxe	cpxe
csx_cpxe	csx_cpxe
lpxs_aaa_conf	lpxs_aaa_conf
lprs_aaa_conf	lprs_aaa_conf
lsuba_lsubc	lsuba_lsubc
ApplDelta	ApplDelta
ApplOmega1	ApplOmega1
ApplOmega2	ApplOmega2
ApplOmega3	ApplOmega3
ApplDelta_lift	ApplDelta_lift
cpr_ApplOmega_12	cpr_ApplOmega_12
cpr_ApplOmega_23	cpr_ApplOmega_23
cpxs_ApplOmega_13	cpxs_ApplOmega_13
fqup_ApplOmega_13	fqup_ApplOmega_13
fpbg_refl	fpbg_refl
Delta	Delta
Omega1	Omega1
Omega2	Omega2
Delta_lift	Delta_lift
cpr_Omega_12	cpr_Omega_12
cpr_Omega_21	cpr_Omega_21
sta_ldec	sta_ldec
snv	snv
snv_inv_lref_aux	snv_inv_lref_aux
snv_inv_lref	snv_inv_lref
snv_inv_gref_aux	snv_inv_gref_aux
snv_inv_gref	snv_inv_gref
snv_inv_bind_aux	snv_inv_bind_aux
snv_inv_bind	snv_inv_bind
snv_inv_appl_aux	snv_inv_appl_aux
snv_inv_appl	snv_inv_appl
snv_inv_cast_aux	snv_inv_cast_aux
snv_inv_cast	snv_inv_cast
snv_extended	snv_extended
snv_restricted	snv_restricted
snv_fwd_aaa	snv_fwd_aaa
snv_fwd_da	snv_fwd_da
snv_fwd_lstas	snv_fwd_lstas
snv_fwd_fsb	snv_fwd_fsb
snv_lift	snv_lift
snv_inv_lift	snv_inv_lift
snv_fqu_conf	snv_fqu_conf
snv_fquq_conf	snv_fquq_conf
snv_fqup_conf	snv_fqup_conf
snv_fqus_conf	snv_fqus_conf
IH_snv_cpr_lpr	IH_snv_cpr_lpr
IH_da_cpr_lpr	IH_da_cpr_lpr
IH_lstas_cpr_lpr	IH_lstas_cpr_lpr
IH_snv_lstas	IH_snv_lstas
snv_cprs_lpr_aux	snv_cprs_lpr_aux
da_cprs_lpr_aux	da_cprs_lpr_aux
da_scpds_lpr_aux	da_scpds_lpr_aux
da_scpes_aux	da_scpes_aux
lstas_cprs_lpr_aux	lstas_cprs_lpr_aux
scpds_cpr_lpr_aux	scpds_cpr_lpr_aux
scpes_cpr_lpr_aux	scpes_cpr_lpr_aux
lstas_scpds_aux	lstas_scpds_aux
scpes_le_aux	scpes_le_aux
snv_cast_scpes	snv_cast_scpes
shnv	shnv
shnv_inv_cast_aux	shnv_inv_cast_aux
shnv_inv_cast	shnv_inv_cast
shnv_inv_snv	shnv_inv_snv
snv_shnv_cast	snv_shnv_cast
lsubsv	lsubsv
lsubsv_inv_atom1_aux	lsubsv_inv_atom1_aux
lsubsv_inv_atom1	lsubsv_inv_atom1
lsubsv_inv_pair1_aux	lsubsv_inv_pair1_aux
lsubsv_inv_pair1	lsubsv_inv_pair1
lsubsv_inv_atom2_aux	lsubsv_inv_atom2_aux
lsubsv_inv_atom2	lsubsv_inv_atom2
lsubsv_inv_pair2_aux	lsubsv_inv_pair2_aux
lsubsv_inv_pair2	lsubsv_inv_pair2
lsubsv_fwd_lsubr	lsubsv_fwd_lsubr
lsubsv_refl	lsubsv_refl
lsubsv_cprs_trans	lsubsv_cprs_trans
lsubsv_drop_O1_conf	lsubsv_drop_O1_conf
lsubsv_drop_O1_trans	lsubsv_drop_O1_trans
lsubsv_fwd_lsubd	lsubsv_fwd_lsubd
lsubsv_lstas_trans	lsubsv_lstas_trans
lsubsv_sta_trans	lsubsv_sta_trans
lsubsv_scpds_trans	lsubsv_scpds_trans
lsubsv_snv_trans	lsubsv_snv_trans
snv_cpr_lpr_aux	snv_cpr_lpr_aux
lstas_cpr_lpr_aux	lstas_cpr_lpr_aux
snv_lstas_aux	snv_lstas_aux
lsubsv_fwd_lsuba	lsubsv_fwd_lsuba
da_cpr_lpr_aux	da_cpr_lpr_aux
lsubsv_cpcs_trans	lsubsv_cpcs_trans
snv_preserve	snv_preserve
da_cpr_lpr	da_cpr_lpr
snv_cpr_lpr	snv_cpr_lpr
snv_lstas	snv_lstas
lstas_cpr_lpr	lstas_cpr_lpr
snv_cprs_lpr	snv_cprs_lpr
da_cprs_lpr	da_cprs_lpr
lstas_cprs_lpr	lstas_cprs_lpr
lstas_cpcs_lpr	lstas_cpcs_lpr
cpys	cpys
cpys_ind	cpys_ind
cpys_ind_dx	cpys_ind_dx
cpy_cpys	cpy_cpys
cpys_strap1	cpys_strap1
cpys_strap2	cpys_strap2
lsuby_cpys_trans	lsuby_cpys_trans
cpys_refl	cpys_refl
cpys_bind	cpys_bind
cpys_flat	cpys_flat
cpys_weak	cpys_weak
cpys_weak_top	cpys_weak_top
cpys_weak_full	cpys_weak_full
cpys_fwd_up	cpys_fwd_up
cpys_fwd_tw	cpys_fwd_tw
cpys_inv_sort1	cpys_inv_sort1
cpys_inv_gref1	cpys_inv_gref1
cpys_inv_bind1	cpys_inv_bind1
cpys_inv_flat1	cpys_inv_flat1
cpys_inv_refl_O2	cpys_inv_refl_O2
cpys_inv_lift1_eq	cpys_inv_lift1_eq
cpys_subst	cpys_subst
cpys_subst_Y2	cpys_subst_Y2
cpys_inv_atom1	cpys_inv_atom1
cpys_inv_lref1	cpys_inv_lref1
cpys_inv_lref1_Y2	cpys_inv_lref1_Y2
cpys_inv_lref1_drop	cpys_inv_lref1_drop
cpys_lift_le	cpys_lift_le
cpys_lift_be	cpys_lift_be
cpys_lift_ge	cpys_lift_ge
cpys_inv_lift1_le	cpys_inv_lift1_le
cpys_inv_lift1_be	cpys_inv_lift1_be
cpys_inv_lift1_ge	cpys_inv_lift1_ge
cpys_inv_lift1_ge_up	cpys_inv_lift1_ge_up
cpys_inv_lift1_be_up	cpys_inv_lift1_be_up
cpys_inv_lift1_le_up	cpys_inv_lift1_le_up
cpys_inv_lift1_subst	cpys_inv_lift1_subst
cpysa	cpysa
lsuby_cpysa_trans	lsuby_cpysa_trans
cpysa_refl	cpysa_refl
cpysa_cpy_trans	cpysa_cpy_trans
cpys_cpysa	cpys_cpysa
cpysa_inv_cpys	cpysa_inv_cpys
cpys_ind_alt	cpys_ind_alt
cpys_inv_SO2	cpys_inv_SO2
cpys_strip_eq	cpys_strip_eq
cpys_strip_neq	cpys_strip_neq
cpys_strap1_down	cpys_strap1_down
cpys_strap2_down	cpys_strap2_down
cpys_split_up	cpys_split_up
cpys_inv_lift1_up	cpys_inv_lift1_up
cpys_conf_eq	cpys_conf_eq
cpys_conf_neq	cpys_conf_neq
cpys_trans_eq	cpys_trans_eq
cpys_trans_down	cpys_trans_down
cpys_antisym_eq	cpys_antisym_eq
llpx_sn_TC_pair_dx	llpx_sn_TC_pair_dx
fqup_trans	fqup_trans
lleq_intro_alt_r	lleq_intro_alt_r
lleq_ind_alt_r	lleq_ind_alt_r
lleq_inv_alt_r	lleq_inv_alt_r

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 346916416..9a7d91b3a 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,15 +1,406 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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)

Documentation $\lambda\delta butterfly$

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Documentation $\lambda\delta butterfly$ +

BibTeX database of Î»Î´ documentation: - downloadlambdadelta.bib, - viewlambdadelta.txt + download + lambdadelta.bib, + view + lambdadelta.txt (revised 2015-09). -

$\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

The main source of information is J3a. -

J3a.	F. Guidi: Verified Representations of Landau's "Grundlagen" in the Î»Î´ Family and in the Calculus of Constructions (2015-12). In JFR 8(1), Univerity of Bologna, pp. 93-116. BibTeX entry.

$\lambda\delta butterfly$ Î»Î´ version 2 (active)

+ + + + + + + + + + +

+ J3a. +	F. Guidi: Verified Representations of Landau's "Grundlagen" in the Î»Î´ Family and in the Calculus of Constructions (2015-12). In JFR 8(1), Univerity of Bologna, pp. 93-116. BibTeX entry.
+	+ +

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

The main source of information is R2c. -

R2c.	F. Guidi: Extending the Applicability Condition in the Formal System Î»Î´ (2015-03). University of Bologna, technical report AMS Acta 4411. BibTeX entry.

R2b.	F. Guidi: An Efficient Validation Procedure for the Formal System Î»Î´ (2010-07). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.

R2a.	F. Guidi: Landau's "Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of Bologna, technical report UBLCS-2009-16. BibTeX entry.

P2d.	F. Guidi: Considerations on Automath in Light of the Grundlagen (revised 2016-06). Presentation at University of Bologna (slides).

P2c.	F. Guidi: The Formal System Î»Î´ and the "Three Problems" (2014-06). Presentation at University of Bologna, for the 10th anniversary of Î»Î´ (slides).

P2b.	F. Guidi: An Efficient Validation Procedure for the Formal System Î»Î´ (2010-07). Presentation at CiE 2010 (slides).

P2a.	F. Guidi: A Validator for the Formal System Î»Î´ (revised 2010-02). Presentation at University of Bologna (slides).

V2a.	F. Guidi: lambdadelta_2A1 (revised 2014-10). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry.

$\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ R2c. +	F. Guidi: Extending the Applicability Condition in the Formal System Î»Î´ (2015-03). University of Bologna, technical report AMS Acta 4411. BibTeX entry.
+	+ +
+ R2b. +	F. Guidi: An Efficient Validation Procedure for the Formal System Î»Î´ (2010-07). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
+	+ +
+ R2a. +	F. Guidi: Landau's "Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of Bologna, technical report UBLCS-2009-16. BibTeX entry.
+	+ +
+ P2d. +	F. Guidi: Considerations on Automath in Light of the Grundlagen (revised 2016-06). Presentation at University of Bologna (slides).
+	+ +
+ P2c. +	F. Guidi: The Formal System Î»Î´ and the "Three Problems" (2014-06). Presentation at University of Bologna, for the 10th anniversary of Î»Î´ (slides).
+	+ +
+ P2b. +	F. Guidi: An Efficient Validation Procedure for the Formal System Î»Î´ (2010-07). Presentation at CiE 2010 (slides).
+	+ +
+ P2a. +	F. Guidi: A Validator for the Formal System Î»Î´ (revised 2010-02). Presentation at University of Bologna (slides).
+	+ +
+ V2a. +	F. Guidi: lambdadelta_2A1 (revised 2014-10). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry.
+	+ +

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

The main source of information is J1a. A summary is available in P1e. -

J1a.	F. Guidi: The Formal System Î»Î´ (2009-11). In ACM ToCL 11(1), pp. 5:1-5:37 online app. pp. 1-11 (accepted2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.

R1c.	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). BibTeX entry.

R1b.	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.

R1a.	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification (2006-01). University of Bologna, technical report UBLCS-2006-01. BibTeX entry.

P1e.	F. Guidi: The Formal System Î»Î´ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).

P1d.	F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).

P1c.	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).

P1b.	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).

P1a.	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).

V1a.	F. Guidi: lambdadelta_1 (revised 2015-01). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry.

$\lambda\delta rainbow rule$

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ J1a. +	F. Guidi: The Formal System Î»Î´ (2009-11). In ACM ToCL 11(1), pp. 5:1-5:37 online app. pp. 1-11 (accepted + 2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
+	+ +
+ R1c. +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). BibTeX entry.
+	+ +
+ R1b. +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.
+	+ +
+ R1a. +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification (2006-01). University of Bologna, technical report UBLCS-2006-01. BibTeX entry.
+	+ +
+ P1e. +	F. Guidi: The Formal System Î»Î´ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).
+	+ +
+ P1d. +	F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).
+	+ +
+ P1c. +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).
+	+ +
+ P1b. +	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).
+	+ +
+ P1a. +	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).
+	+ +
+ V1a. +	F. Guidi: lambdadelta_1 (revised 2015-01). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry.
+	+ +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 61e02fdb8..768502a4d 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -1,12 +1,296 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/BOLOGNA/lambdadelta/ground_1/ (background for Î»Î´ version 1)

$\lambda\delta rainbow rule$

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 $\lambda\delta butterfly$

Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/BOLOGNA/lambdadelta/ground_1/ (background for Î»Î´ version 1)

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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 $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	10	characters	15063	nodes	14881
propositions	theorems	0	lemmas	50	total	50
concepts	declared	24	defined	4	total	28

January 2015. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	10	characters	15063	nodes	14881
propositions	theorems	0	lemmas	50	total	50
concepts	declared	24	defined	4	total	28

+ January 2015. Update with backports from the abandoned specification of Î»Î´ version 2. -

May 2008. +

+ May 2008. Specification is concluded. -

May 2004. +

+ May 2004. Specification starts. -

Logical Structure of the Specification $\lambda\delta butterfly$

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

component	plane	files
multiple relocation		bg_plist
extensions to the library		bg_hints	bg_blt
generated logical decomposables		bg_types	bg_props
preamble		bg_require	bg_rewrite	bg_tactics	bg_subst

$\lambda\delta rainbow rule$

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

+ + +

Logical Structure of the Specification $\lambda\delta butterfly$ +

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

component	plane	files	+ +	+ +	+ +
multiple relocation	+	+ bg_plist +	+ +	+ +	+ +
extensions to the library	+	+ bg_hints +	+ bg_blt +	+ +	+ +
generated logical decomposables	+	+ bg_types +	+ bg_props +	+ +	+ +
preamble	+	+ bg_require +	+ bg_rewrite +	+ bg_tactics +	+ bg_subst +

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:41 +0100

+ + diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index d0349b2ad..36c3513b0 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -1,18 +1,824 @@ -\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/ground_2/ (background for Î»Î´ version 2)

$\lambda\delta rainbow rule$

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 $\lambda\delta butterfly$

Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

cic:/matita/lambdadelta/ground_2/ (background for Î»Î´ version 2)

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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 $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. -

category	objects
sizes	files	93	characters	135543	nodes	314125
propositions	theorems	38	lemmas	647	total	685
concepts	declared	63	defined	67	total	130

2016 April 18. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	95	characters	135595	nodes	314345
propositions	theorems	38	lemmas	647	total	685
concepts	declared	63	defined	67	total	130

+ 2016 April 18. Generic rt-transition counter (rtc). -

2016 March 4. +

+ 2016 March 4. Platform-independent multiple relocation (rtmap). -

2016 January 20. +

+ 2016 January 20. Multiple relocation with streams of naturals. -

2015 October 11. +

+ 2015 October 11. Multiple relocation with lists of booleans. -

2013 November 27. +

+ 2013 November 27. Natural numbers with infinity (ynat). -

2011 August 10. +

+ 2011 August 10. Specification starts. -

Logical Structure of the Specification $\lambda\delta butterfly$

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

component

plane

files

generic rt-transition counter

rtc ( â©?,?,?,?âª ) ( ðð ) ( ðð ) ( ðð )

rtc_isrc ( ððâ¦?, ?â¦ )

rtc_shift ( â? )

rtc_max ( ? â¨ ? )

rtc_plus ( ? + ? )

multiple relocation

rtmap

rtmap_eq ( ? â ? )

rtmap_pushs ( â*[?]? )

rtmap_tl ( â«±? )

rtmap_tls ( â«±*[?]? )

rtmap_isid ( ðâ¦?â¦ )

rtmap_id

rtmap_fcla ( ðâ¦?â¦ â¡ ? )

rtmap_isfin ( ðâ¦?â¦ )

rtmap_isuni ( ðâ¦?â¦ )

rtmap_uni ( ðâ´?âµ )

rtmap_sle ( ? â ? )

rtmap_sand ( ? â ? â¡ ? )

rtmap_sor ( ? â ? â¡ ? )

rtmap_at ( @â¦?,?â¦ â¡ ? )

rtmap_istot ( ðâ¦?â¦ )

rtmap_after ( ? â ? â¡ ? )

rtmap_coafter ( ? ~â ? â¡ ? )

nstream ( â? ) ( â«¯? )

nstream_eq

nstream_isid

nstream_id ( ðð )

nstream_sand

nstream_istot ( ?@â´?âµ )

nstream_after ( ? â ? )

nstream_coafter ( ? ~â ? )

mr2

mr2_at ( @â¦?,?â¦ â¡ ? )

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

natural numbers with infinity

ynat ( â )

ynat_pred ( â«°? )

ynat_succ ( â«¯? )

ynat_le ( ? â¤ ? )

ynat_lt ( ? < ? )

ynat_plus ( ? + ? )

extensions to the library

stream ( ? @ ? )

stream_eq ( ? â ? )

stream_hdtl ( â? )

stream_tls ( â*[?]? )

list ( â ) ( ? @ ? ) ( |?| )

list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

bool ( â» ) ( â )

arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? )

star

lstar

generated logical decomposables

xoa ( ââ ) ( â¨â¨ ) ( â§â§ )

xoa_props ( â¥ ) ( â¤ )

$\lambda\delta rainbow rule$

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

+ + +

Logical Structure of the Specification $\lambda\delta butterfly$ +

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

component

plane

files

+
+

generic rt-transition counter

rtc ( â©?,?,?,?âª ) ( ðð ) ( ðð ) ( ðð )

rtc_isrc ( ððâ¦?, ?â¦ )

rtc_shift ( â? )

rtc_max ( ? â¨ ? )

rtc_plus ( ? + ? )

+
+

multiple relocation

rtmap

rtmap_eq ( ? â ? )

rtmap_pushs ( â*[?]? )

rtmap_tl ( â«±? )

rtmap_tls ( â«±*[?]? )

rtmap_isid ( ðâ¦?â¦ )

rtmap_id

rtmap_fcla ( ðâ¦?â¦ â¡ ? )

rtmap_isfin ( ðâ¦?â¦ )

rtmap_isuni ( ðâ¦?â¦ )

rtmap_uni ( ðâ´?âµ )

rtmap_sle ( ? â ? )

rtmap_sand ( ? â ? â¡ ? )

rtmap_sor ( ? â ? â¡ ? )

rtmap_at ( @â¦?,?â¦ â¡ ? )

rtmap_istot ( ðâ¦?â¦ )

rtmap_after ( ? â ? â¡ ? )

rtmap_coafter ( ? ~â ? â¡ ? )

+
+

nstream ( â? ) ( â«¯? )

nstream_eq

nstream_isid

nstream_id ( ðð )

nstream_sand

nstream_istot ( ?@â´?âµ )

nstream_after ( ? â ? )

nstream_coafter ( ? ~â ? )

+
+

mr2

mr2_at ( @â¦?,?â¦ â¡ ? )

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

+
+

natural numbers with infinity

ynat ( â )

ynat_pred ( â«°? )

ynat_succ ( â«¯? )

ynat_le ( ? â¤ ? )

ynat_lt ( ? < ? )

ynat_plus ( ? + ? )

+
+

extensions to the library

stream ( ? @ ? )

stream_eq ( ? â ? )

stream_hdtl ( â? )

stream_tls ( â*[?]? )

+
+

list ( â ) ( ? @ ? ) ( |?| )

list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

+
+

bool ( â» ) ( â )

arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? )

+
+

star

lstar

+
+

generated logical decomposables

xoa ( ââ ) ( â¨â¨ ) ( â§â§ )

xoa_props ( â¥ ) ( â¤ )

+
+

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index c58614f4c..b4c9a726d 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -1,99 +1,295 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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)

Foreword $\lambda\delta butterfly$

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Foreword $\lambda\delta butterfly$ +

The formal systems of the Î»Î´ (\lambda\delta) family are typed Î»-calculi aiming to support the foundational frameworks for Mathematics that require an underlying specification language (for example the Minimalist Foundation and its predecessors). -

The Î»Î´ family is developed within the Hypertextual Electronic Library of Mathematics as a set of machine-checked digital specifications. -

This is the family logo: crux_177.png (revised 2012-09). -

Notice for the user of Internet Explorer. +

+ Notice for the user of Internet Explorer. To view this site correctly, please select a font with Unicode support. For example "Lucida Sans Unicode" (it should be already installed on your system). To change the current font follow: "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button. -

Citations $\lambda\delta butterfly$

+ +

Citations $\lambda\delta butterfly$ +

This is a list of publications citing Î»Î´ documentation. -

M.E. Maietti, S. Maschio: An extensional Kleene realizability semantics for the Minimalist Foundation (2015). In Leibniz International Proceedings in Informatics, 39, pp 162-186. Schloss Dagstuhl, Leibniz-Zentrum fÃ¼r Informatik. -

C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: ELPI: Fast, Embeddable, Î»Prolog Interpreter (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer. -

A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: Formal metatheory of programming languages in the Matita interactive theorem prover (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer. -

M.E. Maietti: Consistency of the minimalist foundation with Church thesis and Bar Induction (2012). Submitted article. -

W. Ricciotti: Theoretical and implementation aspects in the mechanization of the metatheory of programming languages (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. -

C.E. Brown: Faithful Reproductions of the Automath Landau Formalization (2011). Technical report. -

M.E. Maietti: A minimalist two-level foundation for constructive mathematics (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. -

V. Rahili: First Year Report: Realisability methods of proof and semantics with application to expansion (July 2007). Technical report. -

Disclaimer $\lambda\delta butterfly$

+ + + +

Disclaimer $\lambda\delta butterfly$ +

The systems of the Î»Î´ family are not related intentionally to any other system having (variations of) the symbols Î» and Î´ in its name or syntax. Examples include (but are not limited to): -

Î»-Î´ of +

+ Î»-Î´ of A. Church: The calculi of lambda-conversion (1941). Annals of Mathematics Studies 6. Princeton University Press. -

âÎ of +

+ âÎ of N.G. de Bruijn: Generalizing Automath by means of a lambda-typed lambda calculus (1987). In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92. Marcel Dekker. -

Î»_â of +

+ Î»_â + of N.J. Rehof, M.H. SÃ¸rensen: The Î»_â-calculus (1994). In Lecture Notes in Computer Science, 789, pp. 516â542. Springer. -

Î»â of +

+ Î»â of S. Ronchi Della Rocca, L. Paolini: The Parametric Lambda Calculus (2004). Texts in Theoretical Computer Science, An EATCS Series. Springer. -

Î»D of +

+ Î»D of R. Nederpelt, H. Geuvers: Type Theory and Formal Proof (2014). Cambridge University Press. -

CÎ»Î¾ of +

+ CÎ»Î¾ of N.G. de Bruijn: A namefree lambda calculus with facilities for internal definition of expressions and segments (1978). TH-report 78-WSK-03. Eindhoven University of Technology, Eindhoven. -

+ + +

Moreover, the systems of the Î»Î´ family are not related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. -

$\lambda\delta rainbow rule$

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

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index b5e25b9d9..e6cb4c1f7 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,22 +1,137 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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)

Tools $\lambda\delta butterfly$

Open Symbolic Notation

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Tools $\lambda\delta butterfly$ +

+ +

+ Open Symbolic Notation

Open Symbolic Notation, abbreviated OSN, is an easy and flexible data-interchange text format intended for the lightweight representation of generic abstract syntax trees in the domain of formal languages. Additional information is available at OSN web site. -

Helena

Helena is a processor for the systems of the Î»Î´ family, implemented in Caml as a part of the HELM software, meant for testing both their stable and unstable features. -

The processor source code is available in the directory /trunk/helm/software/helena/ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. -

Version 0.8.3 (2015-12). +

+ Version 0.8.3 (2015-12). Supports exportation to Î»Prolog (two formats for ELPI, and two formats for Teyjus). @@ -27,10 +142,18 @@ Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2: +3% with optimized compilation, +5% without optimized compilation. [Svn revision: 13108] (archived source code). -
- 2015-06. +
  - + 2015-06. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in a Î»Prolog implementation of Î»Î´ version 3. -
- Version 0.8.2 (2015-02). +
+

+ Version 0.8.2 (2015-02). Uses Î»Î´ version 3 with layer variables as core language. Supports exportation to Gallina (the specification language of Coq), @@ -40,69 +163,145 @@ increases of 34% with respect to version 0.8.1. Documentation (J3a). [Svn revision: 13035] (archived source code). -
- +
  - The specification of Landau's "Grundlagen der Analysis" for Coq 8: grundlagen_2.v (revised 2015-02). -
  - +
  - The specification of Landau's "Grundlagen der Analysis" for Matita 0.99.2: grundlagen_2.tar.bz2 (revised 2015-02). -
  - +
  - The corrected specification of Landau's "Grundlagen der Analysis": grundlagen_2.aut (revised 2014-12). -
  - 2015-02. +
  - + 2015-02. The translated specification of Landau's "Grundlagen der Analysis" is successfully validated in CC by Coq 8.4.3. -
  - 2014-12. +
  - + 2014-12. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in Î»Î´ version 3. -
- Version 0.8.1 (2010-11). +
+

+ Version 0.8.1 (2010-11). Uses a subset of Î»Î´ version 4 as intermediate language. Features importation from ".hln" files containing Î»Î´ textual syntax. The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. [Svn revision: 11032] (archived source code). -
- +
  - A Jed mode for editing ".hln" files (containing Î»Î´ textual syntax): helena.sl (revised 2010-11). -
  - 2009-12. +
  - + 2009-12. Helena appears in F. Wiedijk's index of computer math systems. -
- Version 0.8.0 (2009-09). +
+

+ Version 0.8.0 (2009-09). Supports Î»Î´ version 2 with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. Documentation (R2a). [Svn revision: 10304] (archived source code). -
- +
  - A Jed mode for editing ".aut" files (containing Automath textual syntax): automath.sl (revised 2008-07). -
  - 2009-09. +
  - + 2009-09. Jutting's specification of Landau's "Grundlagen der Analysis" enters Î»Î´ Digital Library. -
  - 2009-06. +
  - + 2009-06. Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion. -
$[\lambda\delta digital library logo]$ Î»Î´ Digital Library (LDDL)
+

+ + +

+ $[\lambda\delta digital library logo]$ Î»Î´ Digital Library (LDDL)

The Î»Î´ Digital Library is part of HELM and contains resources expressed in the systems of the Î»Î´ family. -

Contents: + +
- + Contents: Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath). -
- Access:static pages (updated 2015-01), +
+
- + Access: + static pages (updated 2015-01), data set (updated 2014-12), HELM server URL (updated 2014-12). -
- Examples: +
+
- + Examples: + Grundlagen's definition "t234" in Î»Î´ version 4. -
$\lambda\delta rainbow rule$

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

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index d4d07a06a..a92c560b7 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -1,97 +1,385 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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)

Milestones $\lambda\delta butterfly$

December 2015.Second journal paper on Î»Î´ + + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

+ +

Milestones $\lambda\delta butterfly$ +

+ December 2015. + Second journal paper on Î»Î´ accepted for publication. -

December 2015."Helena 0.8.3" is released. -

August 2015. +

+ December 2015. + "Helena 0.8.3" is released. +

+ August 2015. The specification of Î»Î´ version 2A1 is concluded. -

June 2015. +

+ June 2015. The corrected specification of Landau's "Grundlagen der Analysis" is validated in a Î»Prolog implementation of Î»Î´ version 3. -

March 2015. +

+ March 2015. The specification of Î»Î´ version 1 is validated by Matita 0.99.2. -

February 2015."Helena 0.8.2" is updated. -
- +
+
- + February 2015. + "Helena 0.8.2" is updated. +
  - The translated specification of Landau's "Grundlagen der Analysis" is validated in CC by Coq 8.4.3. -
- January 2015. +
+

+ January 2015. The specification of Î»Î´ version 1 is updated with backports from the abandoned specification of Î»Î´ version 2. -

December 2014."Helena 0.8.2" is released. -
- +
+
- + December 2014. + "Helena 0.8.2" is released. +
  - The corrected specification of Landau's "Grundlagen der Analysis" is validated in Î»Î´ version 3. -
- October 2014.Î»Î´ version 2A1 +
+

+ October 2014. + Î»Î´ version 2A1 is released. -

July 2014. +

+ July 2014. A new version of this site is online. -

June 2014.First communication on Î»Î´ version 2.

December 2012. +

+ June 2014. + First communication on Î»Î´ version 2. +

+ December 2012. The character "_" is removed from the denomination "lambda_delta": -
- +
  - The denomination "\lambda\delta" is used in Î»Î´-related texts. -
  - +
  - The denomination "lambdadelta" is used in Î»Î´-related identifiers. -
  - +
  - Permanent Î»Î´ URL acquired: http://lambdadelta.info/ (pointing at this site). -
- September 2011. +
+

+ September 2011. The denomination "lambda-delta" changes to "lambda_delta": -
- +
  - The character "-" is reserved in Î»Î´ textual syntax (recognized by "Helena 0.8.1"). -
  - +
  - Eventually, the occurrences of the character "-" will be replaced by "_" in all Î»Î´-related identifiers. -
  - +
  - In particular, this refactoring involves file names and path names. -
- April 2011. +
+

+ April 2011. The specification of Î»Î´ version 2 and related topics is restarted in Matita 0.5. -

February 2011. +

+ February 2011. The specification of Î»Î´ version 2 with Coq 7.3.1 is abandoned. -

December 2010. +

+ December 2010. Transient Î»Î´ URL acquired: http://lambda-delta.info/ (expires on December 2012). -

November 2010."Helena 0.8.1" is released. -

September 2009."Helena 0.8.0" is released and the +

+ November 2010. + "Helena 0.8.1" is released. +

+ September 2009. + "Helena 0.8.0" is released and the Î»Î´ Digital Library is started. -

June 2009. +

+ June 2009. "Helena", a validator for Î»Î´ version 2, is available as a part of the HELM software. -

September 2008. +

+ September 2008. This site is online. -

July 2008.First journal paper on Î»Î´ +

+ July 2008. + First journal paper on Î»Î´ accepted for publication. -

July 2008. +

+ July 2008. First procedural reconstruction for Matita 0.5 of the Î»Î´ version 1 for Coq 7.3.1. -

June 2008. +

+ June 2008. The HTML pages of the specification of Î»Î´ version 1 for Matita 0.5 are online. -

May 2008. +

+ May 2008. The specification of Î»Î´ version 1 is concluded. -

March 2008. +

+ March 2008. The specification of Î»Î´ version 2 is started with Coq 7.3.1 (false start). -

September 2007. +

+ September 2007. The specification of Î»Î´ version 1 for Matita 0.4 is online. -

November 2006.Î»Î´ version 1 +

+ November 2006. + Î»Î´ version 1 is released. -

December 2005.First communication on Î»Î´ version 1. -

May 2004. +

+ December 2005. + First communication on Î»Î´ version 1. +

+ May 2004. The specification of Î»Î´ version 1 is started with Coq 7.3.1. -

Visibility $\lambda\delta butterfly$

June 2014. +

+ +

Visibility $\lambda\delta butterfly$ +

+ June 2014. The Google search for "formal system lambda delta" gives 5 resources about the Î»Î´ family in the first 6 results. -

June 2014. +

+ June 2014. The Yahoo search for "formal system lambda delta" gives 4 resources about the Î»Î´ family in the first 5 results. -

$\lambda\delta rainbow rule$

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

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:40 +0100

+ + diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 26b1014dc..45166f8ad 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -1,12 +1,39 @@ -\lambda\delta home page: Open Symbolic Notation

Open Symbolic Notation

$\lambda\delta rainbow rule$

+ + + + + + + + \lambda\delta home page: Open Symbolic Notation + + + + + + +

+ +

Open Symbolic Notation

+ $\lambda\delta rainbow rule$ +

Open Symbolic Notation, abbreviated OSN, is an easy and flexible data-interchange text format intended for the lightweight representation of generic abstract syntax trees in the domain of formal languages. In order to meet these design goals, OSN pursues the following features. -

Symbolic expressions +

+ + Symbolic expressions based on widely accepted syntactical conventions provide for a lightweight and generic grammar, which is both easy for machines to process, @@ -20,54 +47,156 @@ as well as the support for canonicalization. Apparently, these features fall outside the scope of OSN, which targets the data structures of formal languages. -

+ Optionally qualified symbolic expressions allow OSN texts to mix data from different domains preserving their own semantics because name conflicts can be avoided. As a consequence OSN documents are easy to extend in that domain-specific OSN applications can work as expected even if data from different domains is added to the text they process. -

+ The US-ASCII character set, extended to UTF-8 in free-form text strings for the convenience of human readers, makes OSN documents easy to visualize and transport over communication media. OSN design aims at supporting application-independent standard encodings. -

Grammar $\lambda\delta butterfly$

+ + + +

Grammar $\lambda\delta butterfly$ +

An OSN text uses the UTF-8 character set and contains the next seven tokens that we define in a very common EBNF variant. Characters not starting a token are not allowed. The ones in the range U+0021 ... U+007E are ! # $ % & * / ? @ \ ^ | ~ and are available for extensions of OSN. -

This token can represent the identifiers and the numerical constants of most programming languages: -
symbol = 1 * symbol-char ;
symbol-char = '+' | '-' | '.' | '0' | ... | '9' | 'A' | ... | 'Z' | '_' | '`' | 'a' | ... | 'z' ;

+
+ symbol = 1 * symbol-char ;
symbol-char = '+' | '-' | '.' | '0' | ... | '9' | 'A' | ... | 'Z' | '_' | '`' | 'a' | ... | 'z' ; +

This token contains free-form text with commonly accepted escape sequences: -
string = '"' , * ( string-char | "'" | '\' escape ) , '"' ;
string-char = ( #0 | ... | #10FFFF ) - ( #0 | ... | #1F | "'" | '\' | '"' | #7F ) ;
escape = 1 * space | '"' | "'" | '(' | ')' | '0' | '\' | 'a' | 'b' | 'e' | 'f' | 'n' | 'r' | 't' | ( 'u' , 4 * 4 hex ) | 'v' | ( 'x' , 2 * 2 hex ) ;
space = #9 | ... | #D | #20 ;
hex = '0' | ... | '9' | 'A' | ... | 'F' | 'a' | ... | 'f' ;

+
+ string = '"' , * ( string-char | "'" | '\' escape ) , '"' ;
string-char = ( #0 | ... | #10FFFF ) - ( #0 | ... | #1F | "'" | '\' | '"' | #7F ) ;
escape = 1 * space | '"' | "'" | '(' | ')' | '0' | '\' | 'a' | 'b' | 'e' | 'f' | 'n' | 'r' | 't' | ( 'u' , 4 * 4 hex ) | 'v' | ( 'x' , 2 * 2 hex ) ;
space = #9 | ... | #D | #20 ;
hex = '0' | ... | '9' | 'A' | ... | 'F' | 'a' | ... | 'f' ; +

This token is a widely used alternative of the former token: -
string-alt = "'" , * ( string-char | '"' | '\' escape ) , "'" ;

+
+ string-alt = "'" , * ( string-char | '"' | '\' escape ) , "'" ; +

This token separates the qualifiers of a symbolic expression: -
sep = ':' ;

+
+ sep = ':' ; +

This token starts a compound symbolic expression: -
open = '(' | '<' | '[' | '{' ;

+
+ open = '(' | '<' | '[' | '{' ; +

This token ends a compound symbolic expression: -
close = ')' | '>' | ']' | '}' ;

+
+ close = ')' | '>' | ']' | '}' ; +

This token is ignored and separates the other tokens: -
gap = space | ',' | ';' | '=' ;

+
+ gap = space | ',' | ';' | '=' ; + + +

The grammar of OSN is very liberal by design. Spaces of the form 1 * gap can appear between any pair of tokens. -

An OSN text: -
text = * q-expr ;

+
+ text = * q-expr ; +

A qualified symbolic expression: -
q-expr = * ( symbol , 1 * sep ) , expr ;

+
+ q-expr = * ( symbol , 1 * sep ) , expr ; +

An unqualified symbolic expression: -
expr = symbol | string | string-alt | ( open , text , close ) ;

Semantics $\lambda\delta butterfly$

+
+ expr = symbol | string | string-alt | ( open , text , close ) ; + + +

Semantics $\lambda\delta butterfly$ +

Forthcoming ... -

Implementation $\lambda\delta butterfly$

+--> +

Implementation $\lambda\delta butterfly$ +

Forthcoming ... -

$\lambda\delta rainbow rule$

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

+ $\lambda\delta rainbow rule$ +

+
+

+ +

+ + +

+ +

+
+

Last update: Sat, 11 Mar 2017 19:30:39 +0100

+ + diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 380924ebd..c627c3cb1 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -1,9 +1,114 @@ -\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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)

Computer-checked formal specifications $\lambda\delta butterfly$

+ + + + + + + + \lambda\delta home page + + + + + + +

+ + $[\lambda\delta home]$ + +

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$ +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ 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)

Computer-checked formal specifications $\lambda\delta butterfly$ +

The systems of the Î»Î´ family are developed as machine-checked digital specifications, and are listed in the next table, which includes the major milestones. -

The life cycle of a specification consists of four periods. Alpha: the definitions are designed and the major propositions are proved, @@ -15,71 +120,264 @@ while major changes and additions are announced and reported on paper. Delta: after its conclusion, the specification is modified just for maintenance. -

version	name	stage	developed with	started	announced	released	concluded	references
Version 3	"basic_3"							J3a
Version 2	"basic_2"	"A2"	Matita 0.99.3	October 2015
		"A1"	Matita 0.99.2	April 2011	June 2014	October 2014	August 2015	V2a R2c
Abandoned			Coq 7.3.1	March 2008			February 2011
Version 1	"basic_1"		Coq 7.3.1	May 2004	December 2005	November 2006	May 2008	V1a J1a

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

version	name	stage	developed with	started	announced	released	concluded	references
+ Version 3 +	"basic_3"	+	+	+	+	+	+	+ J3a +
+ Version 2 +	"basic_2"	"A2"	+ Matita 0.99.3 +	October 2015	+	+	+	+
+ +	+ +	"A1"	+ Matita 0.99.2 +	April 2011	June 2014	October 2014	August 2015	+ V2a + R2c +
Abandoned	+	+	+ Coq 7.3.1 +	March 2008	+	+	February 2011	+
+ Version 1 +	"basic_1"	+	+ Coq 7.3.1 +	May 2004	December 2005	November 2006	May 2008	+ V1a + J1a +

Informational pages on the specifications are provided. -

Notice on displayed numerical acounts: +

+ Notice on displayed numerical acounts: nodes are counted according to the "intrinsic complexity measure" [F. Guidi: "Procedural Representation of CIC Proof Terms" Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. -

Notice on displayed logical structures: +

+ Notice on displayed logical structures: from the logical standpoint, the source scripts are grouped in "planes" and these are grouped in "components"; the notation for the relations or functions introduced in each script, is shown in parentheses (? are placeholders). -

$\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

+ + + +

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

The formal specification of Î»Î´ version 3 is forthcoming. -

$\lambda\delta butterfly$ Î»Î´ version 2 (active)

+ +

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: -

lambdadelta_2A1 for Matita 0.99.2 +
+
- +
  + lambdadelta_2A1 for Matita 0.99.2 (revised 2014-10). Source scripts. Documentation (R2c). -
  +
  +
  The scripts are grouped in directories, first by part, then by component. -
  Notice: +
  +
  + Notice: the scripts are checked by the latest version of Matita from HELM Subversion repository at path <trunk/matita/>. -
+
+

Informational pages on the parts of the specification: Background, Core, Applications. -

$\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

+ +

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats: -

lambdadelta_1 for Coq 7.3.1 +
+
- +
  + lambdadelta_1 for Coq 7.3.1 (revised 2015-09). Source scripts. Documentation (J1a). -
  - 2015 January 15. +
    - + 2015 January 15. 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg". -
  +
+