From 528f8ea107f689d07d060e1d31ba32bf65b4e6ba Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 13 Jan 2018 20:55:24 +0100 Subject: [PATCH] \lambda\delta web site update for git --- .gitignore | 22 + helm/www/lambdadelta/BTM.html | 227 - helm/www/lambdadelta/Makefile | 33 +- helm/www/lambdadelta/apps_2.html | 261 - helm/www/lambdadelta/basic_1.html | 828 -- helm/www/lambdadelta/basic_2.html | 1114 --- helm/www/lambdadelta/bin/Makefile.common | 47 +- helm/www/lambdadelta/bin/xhtbl/Makefile | 7 +- helm/www/lambdadelta/core.html | 7121 ----------------- helm/www/lambdadelta/documentation.html | 406 - helm/www/lambdadelta/download/lambdadelta.bib | 32 +- helm/www/lambdadelta/download/lambdadelta.txt | 32 +- helm/www/lambdadelta/ground_1.html | 296 - helm/www/lambdadelta/ground_2.html | 918 --- helm/www/lambdadelta/home.html | 302 - helm/www/lambdadelta/implementation.html | 307 - helm/www/lambdadelta/news.html | 385 - helm/www/lambdadelta/osn.html | 202 - helm/www/lambdadelta/specification.html | 383 - .../web/home/documentation.ldw.xml | 2 +- .../lambdadelta/web/home/documentation_1.tbl | 12 +- .../lambdadelta/web/home/documentation_2.tbl | 12 +- .../lambdadelta/web/home/documentation_3.tbl | 12 +- .../web/home/implementation.ldw.xml | 4 +- helm/www/lambdadelta/web/home/news.ldw.xml | 36 +- helm/www/lambdadelta/web/home/sitemap.tbl | 40 +- .../web/home/specification.ldw.xml | 14 +- helm/www/lambdadelta/web/home/versions.tbl | 12 +- 28 files changed, 190 insertions(+), 12877 deletions(-) delete mode 100644 helm/www/lambdadelta/BTM.html delete mode 100644 helm/www/lambdadelta/apps_2.html delete mode 100644 helm/www/lambdadelta/basic_1.html delete mode 100644 helm/www/lambdadelta/basic_2.html delete mode 100644 helm/www/lambdadelta/core.html delete mode 100644 helm/www/lambdadelta/documentation.html delete mode 100644 helm/www/lambdadelta/ground_1.html delete mode 100644 helm/www/lambdadelta/ground_2.html delete mode 100644 helm/www/lambdadelta/home.html delete mode 100644 helm/www/lambdadelta/implementation.html delete mode 100644 helm/www/lambdadelta/news.html delete mode 100644 helm/www/lambdadelta/osn.html delete mode 100644 helm/www/lambdadelta/specification.html diff --git a/.gitignore b/.gitignore index 78b201214..29933ad99 100644 --- a/.gitignore +++ b/.gitignore @@ -40,6 +40,28 @@ helm/software/helena/scripts/lp/grundlagen_2b_lyp.elpi helm/software/helena/scripts/cc helm/software/helena/etc +helm/www/lambdadelta/html +helm/www/lambdadelta/etc/BTM +helm/www/lambdadelta/etc/lambdadelta +helm/www/lambdadelta/etc/coq-contribs +helm/www/lambdadelta/xslt/apps_2_src.xsl +helm/www/lambdadelta/xslt/basic_2_blk.xsl +helm/www/lambdadelta/xslt/basic_2_src.xsl +helm/www/lambdadelta/xslt/ground_2_src.xsl +helm/www/lambdadelta/xslt/basic_1_blk.xsl +helm/www/lambdadelta/xslt/basic_1_src.xsl +helm/www/lambdadelta/xslt/basic_1_sum.xsl +helm/www/lambdadelta/xslt/ground_1_src.xsl +helm/www/lambdadelta/xslt/ground_1_sum.xsl +helm/www/lambdadelta/xslt/documentation_1.xsl +helm/www/lambdadelta/xslt/documentation_2.xsl +helm/www/lambdadelta/xslt/documentation_3.xsl +helm/www/lambdadelta/xslt/sitemap.xsl +helm/www/lambdadelta/xslt/versions.xsl +helm/www/lambdadelta/xslt/core.xsl +helm/www/lambdadelta/xslt/chc_45.xsl +helm/www/lambdadelta/xslt/xhtbl.xsl + matita/matita/contribs/lambdadelta/token matita/matita/contribs/lambdadelta/2A1 matita/matita/contribs/lambdadelta/apps_2/notation diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html deleted file mode 100644 index d19919f15..000000000 --- a/helm/www/lambdadelta/BTM.html +++ /dev/null @@ -1,227 +0,0 @@ - - - - - - - - - - BTM - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/BTM/
-
- [Spacer] -
-
Character classes
-
This table shows how the first 45 positive integers - are distributed in the four classes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
classcontents -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
p -
- 		147101316192225283134374043
q -
- 		5111517232933354145 -
- 		-
- 		-
- 		-
- 		-
-
s -
- 		268141820242632384244 -
- 		-
- 		-
-
t -
- 		39122127303639 -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 5366cc649..938529c63 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -1,6 +1,6 @@ H=@ -TAGS = www up \ +TAGS = www up-html \ lint-xml index lddl install-xml \ test-html html install-html \ install-jed install-bib install-2 install-1 install-coq \ @@ -8,7 +8,7 @@ TAGS = www up \ LDURL = http://lambdadelta.info/ -HOMEDIR = . +SITEDIR = html ETCDIR = etc DOWNDIR = download XSLTDIR = xslt @@ -52,6 +52,8 @@ XMLLINT = xmllint --noout XSLT = xalan XHTBL = $(XHTBLDIR)/xhtbl.native +XHTBLOPTS = + ifeq ($(XSLT), xsltproc) XSLT_PARAM := --param XSLT_OUT := -o @@ -70,7 +72,7 @@ endif XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"' define HTML_TEMPLATE - HTML_$(2) = $$(HOMEDIR)/$(2).html + HTML_$(2) = $$(SITEDIR)/$(2).html HTMLS += $$(HTML_$(2)) $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%) @@ -84,19 +86,20 @@ ifeq ($(MAKECMDGOALS), www) XSLS = $(addprefix $(XSLTDIR)/,xhtbl.xsl $(notdir $(TBLS:%.tbl=%.xsl))) $(XSLS): $(TBLS) $(XHTBL) - @echo " XHTBL *.tbl" - $(H)$(XHTBL) -b $(LDURL) -O $(XSLTDIR) $(TBLS) + @echo " XHTBL $(XHTBLOPTS) *.tbl" + $(H)$(XHTBL) $(XHTBLOPTS) -b $(LDURL) -O $(XSLTDIR) $(TBLS) $(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%))))) endif -all: www +all: + @echo $(HTMLS) www: $(HTMLS) $(TBLS) $(XHTBL) lint-xml: $(XMLS:%=$(XMLDIR)/%) @echo XMLLINT --valid - $(H)$(XMLLINT) --valid $^ + $(H)$(XMLLINT) --valid $^ $(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index: @echo " GENERATE INDEXES" @@ -105,9 +108,9 @@ $(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index: $(DOWNDIR)/lddl.tar.bz2 lddl: $(ETCDIR)/exclude.txt $(XMLDIR)/index.txt @echo " GENERATE lddl.tar.bz2" - $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) + $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) -install-xml: $(DOWNDIR)/lddl.tar.bz2 +install-xml: $(DOWNDIR)/lddl.tar.bz2 @echo " INSTALL xml" $(H)scp $^ $(RDOWNDIR) $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2" @@ -121,7 +124,7 @@ html: $(ETCDIR)/make_html.sh install-html $(DOWNDIR)/static_lddl.tar.bz2: $(ETCDIR)/exclude.txt $(ETCDIR)/make_html.sh @echo " INSTALL html" - $(H)tar -cjf $(DOWNDIR)/static_lddl.tar.bz2 -C static -X $< lddl + $(H)tar -cjf $(DOWNDIR)/static_lddl.tar.bz2 -C static -X $< lddl $(H)scp $(DOWNDIR)/static_lddl.tar.bz2 $(RDOWNDIR) $(H)ssh $(REMOTE) "cd $(RSTATICDIR) && tar -xjf ../../lambdadelta/download/static_lddl.tar.bz2 @@ -158,9 +161,13 @@ install-v: $(HELENADIR)/$(COQ) @echo " INSTALL $(notdir $<)" $(H)scp $< $(DOWNDIR) -up: - @echo " UPDATE $(RHOMEDIR)" - $(H)ssh $(REMOTE) "svn up $(RDIR)" +up-html: + @echo " UPDATE $(RHOMEDIR)/html" + $(H)scp -q -r html $(RHOMEDIR) + +up-download: + @echo " UPDATE $(RHOMEDIR)/download" + $(H)scp -q -r download $(RHOMEDIR) %.ld: @echo " XSLT $@" diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html deleted file mode 100644 index eb3ac6cda..000000000 --- a/helm/www/lambdadelta/apps_2.html +++ /dev/null @@ -1,261 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Contents of the Specification [butterfly] -
-
This specification comprises a collection of checked - applications of λδ version 2. - In particular it contains the components below. -
- - - -
Summary of the Specification [butterfly] -
-
Here is a numerical account of the specification's contents - and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryunits -
- 		-
- 		-
- 		-
- 		-
-
sizescharacters (files)377 (1)nodes (objects)779 (6)intrinsic loss factor2.1
propositionstheorems2lemmas1total3
conceptsdeclared0defined3total3
-
- - - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - -
componentplanefiles
examplesterms with special featuresex_cpr_omega
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html deleted file mode 100644 index b6f6ce3b2..000000000 --- a/helm/www/lambdadelta/basic_1.html +++ /dev/null @@ -1,828 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Abstract Syntax and Behavior [butterfly] -
-
This is a summary of available syntactic items and reductions (block structure). -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
domainblockleader→ζ *annotator (with →ϵ *)applicator (with →θ *)reference *reduction
{X | Γ ⊢ ⊤}exclusionΓ ⊢ χyesnononono
{X | Γ ⊢ X : W}typed abstractionΓ ⊢ λWno<W>(V)#i→β *
{X | Γ ⊢ X = V}abbreviationΓ ⊢ δVyesnono#i→δ
nosortΓ ⊢ ⋆knonononono
-
-
* In terms only. -
-
Summary of the Specification [butterfly] -
-
Here is a numerical account of the specification's contents - and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryobjects -
- 		-
- 		-
- 		-
- 		-
-
sizesfiles120characters198089nodes1449099
propositionstheorems81lemmas618total699
conceptsdeclared39defined47total86
-
- - - - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
componentplanefiles -
-
examplesterms with special features - levels_ex0 - ty3_ex1 - nf2_ex2 - -
-
- - - -
-
dynamic typingwell-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 -
equivalencecontext-sensitive equivalence - pc3_defs - - pc3_props - pc3_gen - pc3_gen_context - pc3_subst0 -
-
- 		context-free equivalence - pc1_defs - - pc1_props -
- - - -
-
computationcontext 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 -
reductionnormal 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 -
unfolditerated static type assignment - sty1_defs - - sty1_props -
static typingstatic 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 substitutioniterated context slicing - drop1_defs - - drop1_props -
-
- 		generic term relocation - lift1_defs - - lift1_props -
substitutionordinary 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 -
grammarclosures - flt_defs - -
-
-
- 		contexts - contexts_defs - clt_defs - ctail_defs - app_defs - cnt_defs - -
-
-
- 		terms - tlist_defs - -
-
-
- 		-
- 		- terms_defs - tlt_defs - iso_defs - -
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html deleted file mode 100644 index e3a69b03a..000000000 --- a/helm/www/lambdadelta/basic_2.html +++ /dev/null @@ -1,1114 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
- -
Summary of the Specification [butterfly] -
-
Here is a numerical account of the specification's contents - and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryunits -
- 		-
- 		-
- 		-
- 		-
-
sizescharacters (files)315581 (309)nodes (objects)1458870 (1431)intrinsic loss factor4.6
propositionstheorems92lemmas1085total1177
conceptsdeclared34defined93total127
-
-
Stage "B"
- -
Stage "A2": "Extending the Applicability Condition"
- - - - - - - - - -
Stage "A1": "Extending the Applicability Condition"
- - - - - - - - - - - - - - - - - - - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
componentsectionplanefiles -
-
rt-conversioncontext-sensitive parallel r-conversionfor termscpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )cpc_cpc
rt-computationuncounted context-sensitive parallel rt-computationrefinement for lenvslsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )lsubsx_lfsx lsubsx_lsubsx
-
- 		-
- 		strongly normalizing for lenvs on referred entrieslfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx
-
- 		-
- 		strongly normalizing for term vectorscsx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_cnx_vector csx_csx_vector
-
- 		-
- 		strongly normalizing for termscsx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx
-
- 		-
- 		for lenvs on referred entrieslfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs
-
- 		-
- 		for lenvs on all entrieslpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? ) -
-
-
- 		-
- 		for termscpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transitionuncounted parallel rst-transitionfor closuresfpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )fpbq_aaa
-
- 		-
- 		proper for closuresfpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )fpb_lfdeq
-
- 		context-sensitive parallel r-transitionfor lenvs on referred entrieslfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
-
- 		-
- 		for binderscpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) -
-
-
- 		-
- 		for termscpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )cpr_drops
-
- 		t-bound context-sensitive parallel rt-transitionfor termscpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
-
- 		uncounted context-sensitive parallel rt-transitionnormal form for termscnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops cnx_cnx
-
- 		-
- 		for lenvs on referred entrieslfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx
-
- 		-
- 		for lenvs on all entrieslpx ( ⦃?,?⦄ ⊢ ⬈[?] ? ) -
-
-
- 		-
- 		for binderscpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) -
-
-
- 		-
- 		for termscpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq
-
- 		counted context-sensitive parallel rt-transitionfor termscpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr
iterated static typingiterated generic extension of a context-sensitive relationfor lenvs on referred entriestc_lfxs ( ? ⦻**[?,?] ? )tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs
static typinggeneric reducibilityrestricted refinement for lenvslsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drops lsubc_lsubr lsubc_lsuba
-
- 		-
- 		candidatesgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
-
- 		-
- 		computation propertiesgcp -
-
-
- 		atomic arity assignmentrestricted refinement for lenvslsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
-
- 		-
- 		for termsaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
-
- 		degree-based equivalencefor closures on referred entriesffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )ffdeq_fqup ffdeq_ffdeq
-
- 		-
- 		for lenvs on referred entrieslfdeq ( ? ≛[?,?,?] ? )lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
-
- 		syntactic equivalencefor lenvs on referred entrieslfeq ( ? ≡[?] ? )lfeq_fqup lfeq_lfeq
-
- 		generic extension of a context-sensitive relationfor lenvs on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
-
- 		context-sensitive free variablesrestricted refinement for lenvslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_lsubr lsubf_frees lsubf_lsubf
-
- 		-
- 		for termsfrees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_drops frees_fqup frees_frees
-
- 		local environmentsrestricted refinementlsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
s-computationiterated structural successorfor closuresfqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_weight fqus_drops fqus_fqup fqus_fqus
-
- 		-
- 		proper for closuresfqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_weight fqup_drops fqup_fqup
s-transitionstructural successorfor closuresfquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight
-
- 		-
- 		proper for closuresfqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
relocationgeneric slicingfor lenvsdrops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector
-
- 		generic relocationfor binderslifts_bind ( ⬆*[?] ? ≡ ? )lifts_weight_bind lifts_lifts_bind
-
- 		-
- 		for term vectorslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector
-
- 		-
- 		for termslifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_tdeq lifts_lifts
-
- 		syntactic equivalencefor lenvs on selected entrieslreq ( ? ≡[?] ? )lreq_length lreq_lreq
-
- 		generic entrywise extensionfor lenvs of one contex-sensitive relationlex ( ? ⦻[?] ? )lex_tc
-
- 		-
- 		for lenvs of two contex-sensitive relationslexs ( ? ⦻*[?,?,?] ? )lexs_tc lexs_length lexs_lexs
syntaxappend for local environments - append ( ? @@ ? )append_length
-
- 		head equivalence for terms - theq ( ? ⩳[?,?] ? )theq_simple theq_tdeq theq_theq theq_simple_vector
-
- 		degree-based equivalence - tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? ) -
-
-
- 		-
- 		- tdeq ( ? ≛[?,?] ? )tdeq_tdeq
-
- 		closures - cl_weight ( ♯{?,?,?} ) -
-
-
- 		-
- 		- cl_restricted_weight ( ♯{?,?} ) -
-
-
- 		global environments - genv -
-
-
- 		local environments - ceq_extceq_ext_ceq_ext
-
- 		-
- 		- cext2 -
-
-
- 		-
- 		- lenv_length ( |?| ) -
-
-
- 		-
- 		- lenv_weight ( ♯{?} ) -
-
-
- 		-
- 		- lenv -
-
-
- 		binders for local environments - ext2ext2_tc ext2_ext2
-
- 		-
- 		- bindbind_weight
-
- 		terms - term_vector ( Ⓐ?.? ) -
-
-
- 		-
- 		- term_simple ( 𝐒⦃?⦄ ) -
-
-
- 		-
- 		- term_weight ( ♯{?} ) -
-
-
- 		-
- 		- term -
-
-
- 		items - item_sd -
-
-
- 		-
- 		- item_sh -
-
-
- 		-
- 		- item -
-
-
- 		atomic arities - aarity -
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/bin/Makefile.common b/helm/www/lambdadelta/bin/Makefile.common index bf944971b..7f95f4a23 100644 --- a/helm/www/lambdadelta/bin/Makefile.common +++ b/helm/www/lambdadelta/bin/Makefile.common @@ -1,27 +1,36 @@ H=@ -include ../../etc/Makefile.defs +OCAMLOPTIONS = -linkpkg -package \"$(REQUIRES)\" $(CAMLOPTIONS) +OCAMLFIND = OCAMLPATH=$(OCAMLPATH) ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc -g $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -DIST=$(EXEC)---$(VERSION) -DATE=$(shell date +%y%m%d) +CAMLP_FEATURES = $(F:%=-D%) -OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" -OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) +AMLS = $(wildcard *.aml) + +define BUILD_TEMPLATE +$(1).all: + @echo " OCAMLBUILD $(1)" + $(H)ocamlbuild $$(BUILDOPTIONS) -ocamlc "$$(OCAMLC)" -ocamlopt "$$(OCAMLOPT)" -yaccflags "-v" -pp "$$(CAMLP)" $(1) + +.PHONY: $(1).all +endef + +all:: $(AMLS:%.aml=%.ml) $(EXECS:%=%.native.all) + +byte:: $(AMLS:%.aml=%.ml) $(EXECS:%=%.byte.all) + +$(foreach EXEC, $(EXECS), $(eval $(call BUILD_TEMPLATE,$(EXEC:%=%.native)))) -all: $(EXEC).native +$(foreach EXEC, $(EXECS), $(eval $(call BUILD_TEMPLATE,$(EXEC:%=%.byte)))) -$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll) - @echo " OCAMLBUILD $(EXEC).native" - $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native +clean:: + @echo " OCAMLBUILD -clean" + $(H)ocamlbuild -clean + $(H)$(RM) $(AMLS:%.aml=%.ml) *~ -clean: - ocamlbuild -clean - rm -rf $(DIST) $(DIST).tgz +.PHONY: all clean -dist: - mkdir -p $(DIST)/Sources - cp ReadMe $(DIST) - cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources - cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) - tar -cvzf $(DIST).tgz $(DIST) +%.ml: %.aml + $(H)$(ALPHA) < $< > $@ diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile b/helm/www/lambdadelta/bin/xhtbl/Makefile index e1b330db9..c56f2d8d7 100644 --- a/helm/www/lambdadelta/bin/xhtbl/Makefile +++ b/helm/www/lambdadelta/bin/xhtbl/Makefile @@ -1,11 +1,10 @@ -EXEC = xhtbl -VERSION=0.1.1 +EXECS = xhtbl REQUIRES = str -YACCFLAGS = -v - include ../Makefile.common test: @$(MAKE) --no-print-directory -C ../../ www + +.PHONY: test diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html deleted file mode 100644 index f0ff46f51..000000000 --- a/helm/www/lambdadelta/core.html +++ /dev/null @@ -1,7121 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Summary of the Specification [butterfly] -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Version 2A1Version 2A2
aarityaarity
destruct_apair_apair_auxdestruct_apair_apair_aux
discr_apair_xy_xdiscr_apair_xy_x
discr_tpair_xy_ydiscr_apair_xy_y
eq_aarity_deceq_aarity_dec
item0item0
bind2bind2
flat2flat2
item2item2
destruct_sort_sort_auxdestruct_sort_sort_aux
eq_item0_deceq_item0_dec
eq_bind2_deceq_bind2_dec
eq_flat2_deceq_flat2_dec
eq_item2_deceq_item2_dec
shsh
sh_Nsh_N
nexts_lenexts_le
nexts_ltnexts_lt
nexts_decnexts_dec
nexts_injnexts_inj
sdsd
deg_Odeg_O
sd_Osd_O
deg_SOdeg_SO
deg_SO_inv_pos_auxdeg_SO_inv_succ_aux
deg_SO_inv_posdeg_SO_inv_succ
deg_SO_refldeg_SO_refl
deg_SO_gtdeg_SO_gt
sd_SOsd_SO
sd_dsd_d
deg_inv_preddeg_inv_pred
deg_inv_precdeg_inv_prec
deg_iterdeg_iter
deg_next_SOdeg_next_SO
sd_d_SSsd_d_SS
sd_d_correctsd_d_correct
termterm
eq_term_deceq_term_dec
destruct_tatom_tatom_auxdestruct_tatom_tatom_aux
destruct_tpair_tpair_auxdestruct_tpair_tpair_aux
discr_tpair_xy_xdiscr_tpair_xy_x
discr_tpair_xy_ydiscr_tpair_xy_y
eq_false_inv_tpair_sneq_false_inv_tpair_sn
eq_false_inv_tpair_dxeq_false_inv_tpair_dx
twtw
tw_postw_pos
simplesimple
simple_inv_bind_auxsimple_inv_bind_aux
simple_inv_bindsimple_inv_bind
simple_inv_pairsimple_inv_pair
lenvlenv
eq_lenv_deceq_lenv_dec
destruct_lpair_lpair_auxdestruct_lpair_lpair_aux
discr_lpair_x_xydiscr_lpair_x_xy
- discr_lpair_xy_x
- ceq
- cfull
lwlw
lw_pairlw_pair
lengthlength
length_inv_zero_dxlength_inv_zero_dx
length_inv_zero_snlength_inv_zero_sn
length_inv_pos_dxlength_inv_succ_dx
length_inv_pos_snlength_inv_succ_sn
- length_atom
- length_pair
genvgenv
eq_genv_deceq_genv_dec
rfwrfw
rfw_shiftrfw_shift
rfw_tpair_snrfw_tpair_sn
rfw_tpair_dxrfw_tpair_dx
rfw_lpair_snrfw_lpair_sn
rfw_lpair_dxrfw_lpair_dx
dada
da_inv_sort_auxda_inv_sort_aux
da_inv_sortda_inv_sort
da_inv_lref_auxda_inv_lref_aux
da_inv_lrefda_inv_lref
da_inv_gref_auxda_inv_gref_aux
da_inv_grefda_inv_gref
da_inv_bind_auxda_inv_bind_aux
da_inv_bindda_inv_bind
da_inv_flat_auxda_inv_flat_aux
da_inv_flatda_inv_flat
lstaslstas
lstas_inv_sort1_auxlstas_inv_sort1_aux
lstas_inv_sort1lstas_inv_sort1
lstas_inv_lref1_auxlstas_inv_lref1_aux
lstas_inv_lref1lstas_inv_lref1
lstas_inv_lref1_Olstas_inv_lref1_O
lstas_inv_lref1_Slstas_inv_lref1_S
lstas_inv_gref1_auxlstas_inv_gref1_aux
lstas_inv_gref1lstas_inv_gref1
lstas_inv_bind1_auxlstas_inv_bind1_aux
lstas_inv_bind1lstas_inv_bind1
lstas_inv_appl1_auxlstas_inv_appl1_aux
lstas_inv_appl1lstas_inv_appl1
lstas_inv_cast1_auxlstas_inv_cast1_aux
lstas_inv_cast1lstas_inv_cast1
- -
liftlift
lift_inv_O2_auxlift_inv_O2_aux
lift_inv_O2lift_inv_O2
lift_inv_sort1_auxlift_inv_sort1_aux
lift_inv_sort1lift_inv_sort1
lift_inv_lref1_auxlift_inv_lref1_aux
lift_inv_lref1lift_inv_lref1
lift_inv_lref1_ltlift_inv_lref1_lt
lift_inv_lref1_gelift_inv_lref1_ge
lift_inv_gref1_auxlift_inv_gref1_aux
lift_inv_gref1lift_inv_gref1
lift_inv_bind1_auxlift_inv_bind1_aux
lift_inv_bind1lift_inv_bind1
lift_inv_flat1_auxlift_inv_flat1_aux
lift_inv_flat1lift_inv_flat1
lift_inv_sort2_auxlift_inv_sort2_aux
lift_inv_sort2lift_inv_sort2
lift_inv_lref2_auxlift_inv_lref2_aux
lift_inv_lref2lift_inv_lref2
lift_inv_lref2_ltlift_inv_lref2_lt
lift_inv_lref2_belift_inv_lref2_be
lift_inv_lref2_gelift_inv_lref2_ge
lift_inv_gref2_auxlift_inv_gref2_aux
lift_inv_gref2lift_inv_gref2
lift_inv_bind2_auxlift_inv_bind2_aux
lift_inv_bind2lift_inv_bind2
lift_inv_flat2_auxlift_inv_flat2_aux
lift_inv_flat2lift_inv_flat2
lift_inv_pair_xy_xlift_inv_pair_xy_x
lift_inv_pair_xy_ylift_inv_pair_xy_y
lift_fwd_pair1lift_fwd_pair1
lift_fwd_pair2lift_fwd_pair2
lift_fwd_twlift_fwd_tw
lift_simple_dxlift_simple_dx
lift_simple_snlift_simple_sn
lift_lref_ge_minuslift_lref_ge_minus
lift_lref_ge_minus_eqlift_lref_ge_minus_eq
lift_refllift_refl
lift_totallift_total
lift_splitlift_split
is_lift_decis_lift_dec
dropdrop
d_liftabled_liftable
d_deliftable_snd_deliftable_sn
dropable_sndropable_sn
dropable_dxdropable_dx
drop_inv_atom1_auxdrop_inv_atom1_aux
drop_inv_atom1drop_inv_atom1
drop_inv_O1_pair1_auxdrop_inv_O1_pair1_aux
drop_inv_O1_pair1drop_inv_O1_pair1
drop_inv_pair1drop_inv_pair1
drop_inv_drop1_ltdrop_inv_drop1_lt
drop_inv_drop1drop_inv_drop1
drop_inv_skip1_auxdrop_inv_skip1_aux
drop_inv_skip1drop_inv_skip1
drop_inv_O1_pair2drop_inv_O1_pair2
drop_inv_skip2_auxdrop_inv_skip2_aux
drop_inv_skip2drop_inv_skip2
drop_inv_O1_gtdrop_inv_O1_gt
drop_refl_atom_O2drop_refl_atom_O2
drop_refldrop_refl
drop_drop_ltdrop_drop_lt
drop_skip_ltdrop_skip_lt
drop_O1_ledrop_O1_le
drop_O1_ltdrop_O1_lt
drop_O1_pairdrop_O1_pair
drop_O1_gedrop_O1_ge
drop_O1_eqdrop_O1_eq
drop_splitdrop_split
drop_FTdrop_FT
drop_gendrop_gen
drop_Tdrop_T
d_liftable_LTCd_liftable_LTC
d_deliftable_sn_LTCd_deliftable_sn_LTC
dropable_sn_TCdropable_sn_TC
dropable_dx_TCdropable_dx_TC
d_deliftable_sn_llstard_deliftable_sn_llstar
drop_fwd_drop2drop_fwd_drop2
drop_fwd_length_gedrop_fwd_length_ge
drop_fwd_length_le_ledrop_fwd_length_le_le
drop_fwd_length_le_gedrop_fwd_length_le_ge
drop_fwd_lengthdrop_fwd_length
drop_fwd_length_minus2drop_fwd_length_minus2
drop_fwd_length_minus4drop_fwd_length_minus4
drop_fwd_length_le2drop_fwd_length_le2
drop_fwd_length_le4drop_fwd_length_le4
drop_fwd_length_lt2drop_fwd_length_lt2
drop_fwd_length_lt4drop_fwd_length_lt4
drop_fwd_length_eq1drop_fwd_length_eq1
drop_fwd_length_eq2drop_fwd_length_eq2
drop_fwd_lwdrop_fwd_lw
drop_fwd_lw_ltdrop_fwd_lw_lt
drop_fwd_rfwdrop_fwd_rfw
drop_inv_O2_auxdrop_inv_O2_aux
drop_inv_O2drop_inv_O2
drop_inv_length_eqdrop_inv_length_eq
drop_inv_refldrop_inv_refl
drop_inv_FT_auxdrop_inv_FT_aux
drop_inv_FTdrop_inv_FT
drop_inv_gendrop_inv_gen
drop_inv_Tdrop_inv_T
lsubrlsubr
lsubr_refllsubr_refl
lsubr_inv_atom1_auxlsubr_inv_atom1_aux
lsubr_inv_atom1lsubr_inv_atom1
lsubr_inv_abst1_auxlsubr_inv_abst1_aux
lsubr_inv_abst1lsubr_inv_abst1
lsubr_inv_abbr2_auxlsubr_inv_abbr2_aux
lsubr_inv_abbr2lsubr_inv_abbr2
lsubr_fwd_lengthlsubr_fwd_length
lsubr_fwd_drop2_pairlsubr_fwd_drop2_pair
lsubr_fwd_drop2_abbrlsubr_fwd_drop2_abbr
cprcpr
lsubr_cpr_translsubr_cpr_trans
tpr_cprtpr_cpr
cpr_reflcpr_refl
cpr_pair_sncpr_pair_sn
cpr_deliftcpr_delift
lstas_cpr_auxlstas_cpr_aux
lstas_cprlstas_cpr
cpr_inv_atom1_auxcpr_inv_atom1_aux
cpr_inv_atom1cpr_inv_atom1
cpr_inv_sort1cpr_inv_sort1
cpr_inv_lref1cpr_inv_lref1
cpr_inv_gref1cpr_inv_gref1
cpr_inv_bind1_auxcpr_inv_bind1_aux
cpr_inv_bind1cpr_inv_bind1
cpr_inv_abbr1cpr_inv_abbr1
cpr_inv_abst1cpr_inv_abst1
cpr_inv_flat1_auxcpr_inv_flat1_aux
cpr_inv_flat1cpr_inv_flat1
cpr_inv_appl1cpr_inv_appl1
cpr_inv_appl1_simplecpr_inv_appl1_simple
cpr_inv_cast1cpr_inv_cast1
cpr_fwd_bind1_minuscpr_fwd_bind1_minus
cnrcnr
cnr_inv_deltacnr_inv_delta
cnr_inv_abstcnr_inv_abst
cnr_inv_abbrcnr_inv_abbr
cnr_inv_zetacnr_inv_zeta
cnr_inv_applcnr_inv_appl
cnr_inv_epscnr_inv_eps
cnr_sortcnr_sort
cnr_lref_freecnr_lref_free
cnr_lref_atomcnr_lref_atom
cnr_abstcnr_abst
cnr_appl_simplecnr_appl_simple
cnr_deccnr_dec
cprscprs
cprs_indcprs_ind
cprs_ind_dxcprs_ind_dx
cpr_cprscpr_cprs
cprs_reflcprs_refl
cprs_strap1cprs_strap1
cprs_strap2cprs_strap2
lsubr_cprs_translsubr_cprs_trans
tprs_cprstprs_cprs
cprs_bind_dxcprs_bind_dx
cprs_flat_dxcprs_flat_dx
cprs_flat_sncprs_flat_sn
cprs_zetacprs_zeta
cprs_epscprs_eps
cprs_beta_dxcprs_beta_dx
cprs_theta_dxcprs_theta_dx
cprs_inv_sort1cprs_inv_sort1
cprs_inv_cast1cprs_inv_cast1
cprs_inv_cnr1cprs_inv_cnr1
scpdsscpds
sta_cprs_scpdssta_cprs_scpds
lstas_scpdslstas_scpds
scpds_strap1scpds_strap1
scpds_fwd_cprsscpds_fwd_cprs
scpesscpes
scpds_divscpds_div
scpes_symscpes_sym
lift_injlift_inj
lift_div_lelift_div_le
lift_div_belift_div_be
lift_monolift_mono
lift_trans_belift_trans_be
lift_trans_lelift_trans_le
lift_trans_gelift_trans_ge
lift_conf_O1lift_conf_O1
lift_conf_belift_conf_be
drop_monodrop_mono
drop_conf_gedrop_conf_ge
drop_conf_bedrop_conf_be
drop_conf_ledrop_conf_le
drop_trans_gedrop_trans_ge
drop_trans_ledrop_trans_le
d_liftable_llstard_liftable_llstar
drop_conf_ltdrop_conf_lt
drop_trans_ltdrop_trans_lt
drop_trans_ge_commdrop_trans_ge_comm
drop_conf_divdrop_conf_div
drop_fwd_bedrop_fwd_be
aaaaaa
aaa_inv_sort_auxaaa_inv_sort_aux
aaa_inv_sortaaa_inv_sort
aaa_inv_lref_auxaaa_inv_lref_aux
aaa_inv_lrefaaa_inv_lref
aaa_inv_gref_auxaaa_inv_gref_aux
aaa_inv_grefaaa_inv_gref
aaa_inv_abbr_auxaaa_inv_abbr_aux
aaa_inv_abbraaa_inv_abbr
aaa_inv_abst_auxaaa_inv_abst_aux
aaa_inv_abstaaa_inv_abst
aaa_inv_appl_auxaaa_inv_appl_aux
aaa_inv_applaaa_inv_appl
aaa_inv_cast_auxaaa_inv_cast_aux
aaa_inv_castaaa_inv_cast
aaa_liftaaa_lift
aaa_inv_liftaaa_inv_lift
aaa_monoaaa_mono
lsubalsuba
lsuba_inv_atom1_auxlsuba_inv_atom1_aux
lsuba_inv_atom1lsuba_inv_atom1
lsuba_inv_pair1_auxlsuba_inv_pair1_aux
lsuba_inv_pair1lsuba_inv_pair1
lsuba_inv_atom2_auxlsuba_inv_atom2_aux
lsubc_inv_atom2lsubc_inv_atom2
lsuba_inv_pair2_auxlsuba_inv_pair2_aux
lsuba_inv_pair2lsuba_inv_pair2
lsuba_fwd_lsubrlsuba_fwd_lsubr
lsuba_refllsuba_refl
lsuba_drop_O1_conflsuba_drop_O1_conf
lsuba_drop_O1_translsuba_drop_O1_trans
lsuba_aaa_conflsuba_aaa_conf
lsuba_aaa_translsuba_aaa_trans
lreqlreq
lreq_pair_ltlreq_pair_lt
lreq_succ_ltlreq_succ_lt
lreq_pair_O_Ylreq_pair_O_Y
lreq_refllreq_refl
lreq_O2lreq_O2
lreq_symlreq_sym
lreq_inv_atom1_auxlreq_inv_atom1_aux
lreq_inv_atom1lreq_inv_atom1
lreq_inv_zero1_auxlreq_inv_zero1_aux
lreq_inv_zero1lreq_inv_zero1
lreq_inv_pair1_auxlreq_inv_pair1_aux
lreq_inv_pair1lreq_inv_pair1
lreq_inv_pairlreq_inv_pair
lreq_inv_succ1_auxlreq_inv_succ1_aux
lreq_inv_succ1lreq_inv_succ1
lreq_inv_atom2lreq_inv_atom2
lreq_inv_succlreq_inv_succ
lreq_inv_zero2lreq_inv_zero2
lreq_inv_pair2lreq_inv_pair2
lreq_inv_succ2lreq_inv_succ2
lreq_fwd_lengthlreq_fwd_length
lreq_inv_O_Y_auxlreq_inv_O_Y_aux
lreq_inv_O_Ylreq_inv_O_Y
lreq_translreq_trans
lreq_canc_snlreq_canc_sn
lreq_canc_dxlreq_canc_dx
lreq_joinlreq_join
dedropable_sndedropable_sn
lreq_drop_trans_belreq_drop_trans_be
lreq_drop_conf_belreq_drop_conf_be
drop_O1_exdrop_O1_ex
dedropable_sn_TCdedropable_sn_TC
drop_O1_injdrop_O1_inj
lpx_snlpx_sn
lpx_sn_refllpx_sn_refl
lpx_sn_inv_atom1_auxlpx_sn_inv_atom1_aux
lpx_sn_inv_atom1lpx_sn_inv_atom1
lpx_sn_inv_pair1_auxlpx_sn_inv_pair1_aux
lpx_sn_inv_pair1lpx_sn_inv_pair1
lpx_sn_inv_atom2_auxlpx_sn_inv_atom2_aux
lpx_sn_inv_atom2lpx_sn_inv_atom2
lpx_sn_inv_pair2_auxlpx_sn_inv_pair2_aux
lpx_sn_inv_pair2lpx_sn_inv_pair2
lpx_sn_inv_pairlpx_sn_inv_pair
lpx_sn_fwd_lengthlpx_sn_fwd_length
lpx_sn_drop_conflpx_sn_drop_conf
lpx_sn_drop_translpx_sn_drop_trans
lpx_sn_deliftable_dropablelpx_sn_deliftable_dropable
lpx_sn_liftable_dedropablelpx_sn_liftable_dedropable
lpx_sn_dropable_auxlpx_sn_dropable_aux
lpx_sn_dropablelpx_sn_dropable
fwfw
fw_shiftfw_shift
fw_tpair_snfw_tpair_sn
fw_tpair_dxfw_tpair_dx
fw_lpair_snfw_lpair_sn
fqufqu
fqu_drop_ltfqu_drop_lt
fqu_lref_S_ltfqu_lref_S_lt
fqu_fwd_fwfqu_fwd_fw
fqu_fwd_length_lref1_auxfqu_fwd_length_lref1_aux
fqu_fwd_length_lref1fqu_fwd_length_lref1
fqu_inv_eq_auxfqu_inv_eq_aux
fqu_inv_eqfqu_inv_eq
fqu_wf_indfqu_wf_ind
fquqfquq
fquq_reflfquq_refl
fqu_fquqfqu_fquq
fquq_fwd_fwfquq_fwd_fw
fquq_fwd_length_lref1_auxfquq_fwd_length_lref1_aux
fquq_fwd_length_lref1fquq_fwd_length_lref1
fquqafquqa
fquqa_reflfquqa_refl
fquqa_dropfquqa_drop
fquq_fquqafquq_fquqa
fquqa_inv_fquqfquqa_inv_fquq
fquq_inv_genfquq_inv_gen
fqupfqup
fqu_fqupfqu_fqup
fqup_strap1fqup_strap1
fqup_strap2fqup_strap2
fqup_dropfqup_drop
fqup_lreffqup_lref
fqup_pair_snfqup_pair_sn
fqup_bind_dxfqup_bind_dx
fqup_flat_dxfqup_flat_dx
fqup_flat_dx_pair_snfqup_flat_dx_pair_sn
fqup_bind_dx_flat_dxfqup_bind_dx_flat_dx
fqup_flat_dx_bind_dxfqup_flat_dx_bind_dx
fqup_indfqup_ind
fqup_ind_dxfqup_ind_dx
fqup_fwd_fwfqup_fwd_fw
fqup_wf_indfqup_wf_ind
fqup_wf_ind_eqfqup_wf_ind_eq
fqusfqus
fqus_indfqus_ind
fqus_ind_dxfqus_ind_dx
fqus_reflfqus_refl
fquq_fqusfquq_fqus
fqus_strap1fqus_strap1
fqus_strap2fqus_strap2
fqus_dropfqus_drop
fqup_fqusfqup_fqus
fqus_fwd_fwfqus_fwd_fw
fqup_inv_step_snfqup_inv_step_sn
fqus_inv_genfqus_inv_gen
fqus_strap1_fqufqus_strap1_fqu
fqus_strap2_fqufqus_strap2_fqu
fqus_fqup_transfqus_fqup_trans
fqup_fqus_transfqup_fqus_trans
cpxcpx
lsubr_cpx_translsubr_cpx_trans
cpx_reflcpx_refl
cpr_cpxcpr_cpx
cpx_pair_sncpx_pair_sn
cpx_deliftcpx_delift
cpx_inv_atom1_auxcpx_inv_atom1_aux
cpx_inv_atom1cpx_inv_atom1
cpx_inv_sort1cpx_inv_sort1
cpx_inv_lref1cpx_inv_lref1
cpx_inv_lref1_gecpx_inv_lref1_ge
cpx_inv_gref1cpx_inv_gref1
cpx_inv_bind1_auxcpx_inv_bind1_aux
cpx_inv_bind1cpx_inv_bind1
cpx_inv_abbr1cpx_inv_abbr1
cpx_inv_abst1cpx_inv_abst1
cpx_inv_flat1_auxcpx_inv_flat1_aux
cpx_inv_flat1cpx_inv_flat1
cpx_inv_appl1cpx_inv_appl1
cpx_inv_appl1_simplecpx_inv_appl1_simple
cpx_inv_cast1cpx_inv_cast1
cpx_fwd_bind1_minuscpx_fwd_bind1_minus
sta_cpx_auxsta_cpx_aux
sta_cpxsta_cpx
cpx_liftcpx_lift
cpx_inv_lift1cpx_inv_lift1
fqu_cpx_transfqu_cpx_trans
fqu_sta_transfqu_sta_trans
fquq_cpx_transfquq_cpx_trans
fquq_sta_transfquq_sta_trans
fqup_cpx_transfqup_cpx_trans
fqus_cpx_transfqus_cpx_trans
fqu_cpx_trans_neqfqu_cpx_trans_neq
fquq_cpx_trans_neqfquq_cpx_trans_neq
fqup_cpx_trans_neqfqup_cpx_trans_neq
fqus_cpx_trans_neqfqus_cpx_trans_neq
lprlpr
lpr_inv_atom1lpr_inv_atom1
lpr_inv_pair1lpr_inv_pair1
lpr_inv_atom2lpr_inv_atom2
lpr_inv_pair2lpr_inv_pair2
lpr_refllpr_refl
lpr_pairlpr_pair
lpr_fwd_lengthlpr_fwd_length
lpxlpx
lpx_inv_atom1lpx_inv_atom1
lpx_inv_pair1lpx_inv_pair1
lpx_inv_atom2lpx_inv_atom2
lpx_inv_pair2lpx_inv_pair2
lpx_inv_pairlpx_inv_pair
lpx_refllpx_refl
lpx_pairlpx_pair
lpr_lpxlpr_lpx
lpx_fwd_lengthlpx_fwd_length
lpx_drop_conflpx_drop_conf
drop_lpx_transdrop_lpx_trans
lpx_drop_trans_O1lpx_drop_trans_O1
fqu_lpx_transfqu_lpx_trans
fquq_lpx_transfquq_lpx_trans
lpx_fqu_translpx_fqu_trans
lpx_fquq_translpx_fquq_trans
cpx_lpx_aaa_confcpx_lpx_aaa_conf
cpx_aaa_confcpx_aaa_conf
lpx_aaa_conflpx_aaa_conf
cpr_aaa_confcpr_aaa_conf
lpr_aaa_conflpr_aaa_conf
cnxcnx
cnx_inv_sortcnx_inv_sort
cnx_inv_deltacnx_inv_delta
cnx_inv_abstcnx_inv_abst
cnx_inv_abbrcnx_inv_abbr
cnx_inv_zetacnx_inv_zeta
cnx_inv_applcnx_inv_appl
cnx_inv_epscnx_inv_eps
cnx_fwd_cnrcnx_fwd_cnr
cnx_sortcnx_sort
cnx_sort_itercnx_sort_iter
cnx_lref_freecnx_lref_free
cnx_lref_atomcnx_lref_atom
cnx_abstcnx_abst
cnx_appl_simplecnx_appl_simple
cnx_deccnx_dec
cpxscpxs
cpxs_indcpxs_ind
cpxs_ind_dxcpxs_ind_dx
cpxs_reflcpxs_refl
cpx_cpxscpx_cpxs
cpxs_strap1cpxs_strap1
cpxs_strap2cpxs_strap2
lsubr_cpxs_translsubr_cpxs_trans
cprs_cpxscprs_cpxs
cpxs_sortcpxs_sort
cpxs_bind_dxcpxs_bind_dx
cpxs_flat_dxcpxs_flat_dx
cpxs_flat_sncpxs_flat_sn
cpxs_pair_sncpxs_pair_sn
cpxs_zetacpxs_zeta
cpxs_epscpxs_eps
cpxs_ctcpxs_ct
cpxs_beta_dxcpxs_beta_dx
cpxs_theta_dxcpxs_theta_dx
cpxs_inv_sort1cpxs_inv_sort1
cpxs_inv_cast1cpxs_inv_cast1
cpxs_inv_cnx1cpxs_inv_cnx1
cpxs_neq_inv_step_sncpxs_neq_inv_step_sn
cpxs_aaa_confcpxs_aaa_conf
cprs_aaa_confcprs_aaa_conf
lpx_sn_confluentlpx_sn_confluent
lpx_sn_transitivelpx_sn_transitive
lpx_sn_translpx_sn_trans
lpx_sn_conflpx_sn_conf
cpr_liftcpr_lift
cpr_inv_lift1cpr_inv_lift1
lpr_drop_conflpr_drop_conf
drop_lpr_transdrop_lpr_trans
lpr_drop_trans_O1lpr_drop_trans_O1
fqu_cpr_trans_dxfqu_cpr_trans_dx
fquq_cpr_trans_dxfquq_cpr_trans_dx
fqu_cpr_trans_snfqu_cpr_trans_sn
fquq_cpr_trans_snfquq_cpr_trans_sn
fqu_lpr_transfqu_lpr_trans
fquq_lpr_transfquq_lpr_trans
cpr_conf_lpr_atom_atomcpr_conf_lpr_atom_atom
cpr_conf_lpr_atom_deltacpr_conf_lpr_atom_delta
cpr_conf_lpr_delta_deltacpr_conf_lpr_delta_delta
cpr_conf_lpr_bind_bindcpr_conf_lpr_bind_bind
cpr_conf_lpr_bind_zetacpr_conf_lpr_bind_zeta
cpr_conf_lpr_zeta_zetacpr_conf_lpr_zeta_zeta
cpr_conf_lpr_flat_flatcpr_conf_lpr_flat_flat
cpr_conf_lpr_flat_epscpr_conf_lpr_flat_eps
cpr_conf_lpr_eps_epscpr_conf_lpr_eps_eps
cpr_conf_lpr_flat_betacpr_conf_lpr_flat_beta
cpr_conf_lpr_flat_thetacpr_conf_lpr_flat_theta
cpr_conf_lpr_beta_betacpr_conf_lpr_beta_beta
cpr_conf_lpr_theta_thetacpr_conf_lpr_theta_theta
cpr_conf_lprcpr_conf_lpr
cpr_confcpr_conf
lpr_cpr_conf_dxlpr_cpr_conf_dx
lpr_cpr_conf_snlpr_cpr_conf_sn
lpr_conflpr_conf
cprs_deltacprs_delta
cprs_inv_lref1cprs_inv_lref1
cprs_liftcprs_lift
cprs_inv_lift1cprs_inv_lift1
cprs_transcprs_trans
cprs_confcprs_conf
cprs_bindcprs_bind
cprs_flatcprs_flat
cprs_beta_rccprs_beta_rc
cprs_betacprs_beta
cprs_theta_rccprs_theta_rc
cprs_thetacprs_theta
cprs_inv_appl1cprs_inv_appl1
lpr_cpr_translpr_cpr_trans
cpr_bind2cpr_bind2
lpr_cprs_translpr_cprs_trans
cprs_stripcprs_strip
cprs_lpr_conf_dxcprs_lpr_conf_dx
cprs_lpr_conf_sncprs_lpr_conf_sn
cprs_bind2_dxcprs_bind2_dx
TC_lpx_sn_pair_reflTC_lpx_sn_pair_refl
TC_lpx_sn_pairTC_lpx_sn_pair
lpx_sn_LTC_TC_lpx_snlpx_sn_LTC_TC_lpx_sn
TC_lpx_sn_inv_atom2TC_lpx_sn_inv_atom2
TC_lpx_sn_inv_pair2TC_lpx_sn_inv_pair2
TC_lpx_sn_indTC_lpx_sn_ind
TC_lpx_sn_inv_atom1TC_lpx_sn_inv_atom1
TC_lpx_sn_inv_pair1_auxTC_lpx_sn_inv_pair1_aux
TC_lpx_sn_inv_pair1TC_lpx_sn_inv_pair1
TC_lpx_sn_inv_lpx_sn_LTCTC_lpx_sn_inv_lpx_sn_LTC
TC_lpx_sn_fwd_lengthTC_lpx_sn_fwd_length
lprslprs
lprs_indlprs_ind
lprs_ind_dxlprs_ind_dx
lpr_lprslpr_lprs
lprs_refllprs_refl
lprs_strap1lprs_strap1
lprs_strap2lprs_strap2
lprs_pair_refllprs_pair_refl
lprs_inv_atom1lprs_inv_atom1
lprs_inv_atom2lprs_inv_atom2
lprs_fwd_lengthlprs_fwd_length
lprs_pairlprs_pair
lprs_inv_pair1lprs_inv_pair1
lprs_inv_pair2lprs_inv_pair2
lprs_ind_altlprs_ind_alt
lprs_cpr_translprs_cpr_trans
lprs_cprs_translprs_cprs_trans
lprs_cprs_conf_dxlprs_cprs_conf_dx
lprs_cpr_conf_dxlprs_cpr_conf_dx
lprs_cprs_conf_snlprs_cprs_conf_sn
lprs_cpr_conf_snlprs_cpr_conf_sn
cprs_bind2cprs_bind2
cprs_inv_abst1cprs_inv_abst1
cprs_inv_abstcprs_inv_abst
cprs_inv_abbr1cprs_inv_abbr1
lprs_pair2lprs_pair2
cpccpc
cpc_reflcpc_refl
cpc_symcpc_sym
cpc_fwd_cprcpc_fwd_cpr
cpc_confcpc_conf
cpcscpcs
cpcs_indcpcs_ind
cpcs_ind_dxcpcs_ind_dx
cpcs_reflcpcs_refl
cpcs_symcpcs_sym
cpc_cpcscpc_cpcs
cpcs_strap1cpcs_strap1
cpcs_strap2cpcs_strap2
cpr_cpcs_dxcpr_cpcs_dx
cpr_cpcs_sncpr_cpcs_sn
cpcs_cpr_strap1cpcs_cpr_strap1
cpcs_cpr_strap2cpcs_cpr_strap2
cpcs_cpr_divcpcs_cpr_div
cpr_divcpr_div
cpcs_cpr_confcpcs_cpr_conf
cpcs_cprs_dxcpcs_cprs_dx
cpcs_cprs_sncpcs_cprs_sn
cpcs_cprs_strap1cpcs_cprs_strap1
cpcs_cprs_strap2cpcs_cprs_strap2
cpcs_cprs_divcpcs_cprs_div
cpcs_cprs_confcpcs_cprs_conf
cprs_divcprs_div
cprs_cpr_divcprs_cpr_div
cpr_cprs_divcpr_cprs_div
cpcs_inv_cprscpcs_inv_cprs
cpcs_inv_sortcpcs_inv_sort
cpcs_inv_abst1cpcs_inv_abst1
cpcs_inv_abst2cpcs_inv_abst2
cpcs_inv_sort_abstcpcs_inv_sort_abst
cpcs_inv_liftcpcs_inv_lift
lpr_cpcs_translpr_cpcs_trans
lprs_cpcs_translprs_cpcs_trans
cpr_cprs_conf_cpcscpr_cprs_conf_cpcs
cprs_cpr_conf_cpcscprs_cpr_conf_cpcs
cprs_conf_cpcscprs_conf_cpcs
lprs_cprs_conflprs_cprs_conf
lpr_cprs_conflpr_cprs_conf
lpr_cpr_conflpr_cpr_conf
cpcs_flatcpcs_flat
cpcs_flat_dx_cpr_revcpcs_flat_dx_cpr_rev
cpcs_bind_dxcpcs_bind_dx
cpcs_bind_sncpcs_bind_sn
lsubr_cpcs_translsubr_cpcs_trans
cpcs_liftcpcs_lift
cpcs_stripcpcs_strip
cpcs_inv_abst_sncpcs_inv_abst_sn
cpcs_inv_abst_dxcpcs_inv_abst_dx
cpcs_transcpcs_trans
cpcs_canc_sncpcs_canc_sn
cpcs_canc_dxcpcs_canc_dx
cpcs_bind1cpcs_bind1
cpcs_bind2cpcs_bind2
lpr_cpcs_conflpr_cpcs_conf
cpcs_aaa_monocpcs_aaa_mono
da_liftda_lift
da_inv_liftda_inv_lift
da_monoda_mono
lstas_liftlstas_lift
lstas_inv_lift1lstas_inv_lift1
lstas_split_auxlstas_split_aux
lstas_splitlstas_split
lstas_lstaslstas_lstas
lstas_translstas_trans
lstas_monolstas_mono
lstas_correctlstas_correct
lstas_conf_lelstas_conf_le
lstas_conflstas_conf
da_lstasda_lstas
lstas_da_conflstas_da_conf
lstas_inv_dalstas_inv_da
lstas_inv_da_gelstas_inv_da_ge
lstas_inv_refl_poslstas_inv_refl_pos
fqus_transfqus_trans
cpxs_deltacpxs_delta
lstas_cpxslstas_cpxs
cpxs_inv_lref1cpxs_inv_lref1
cpxs_liftcpxs_lift
cpxs_inv_lift1cpxs_inv_lift1
fqu_cpxs_transfqu_cpxs_trans
fquq_cpxs_transfquq_cpxs_trans
fquq_lstas_transfquq_lstas_trans
fqup_cpxs_transfqup_cpxs_trans
fqus_cpxs_transfqus_cpxs_trans
fqus_lstas_transfqus_lstas_trans
cpxs_transcpxs_trans
cpxs_bindcpxs_bind
cpxs_flatcpxs_flat
cpxs_beta_rccpxs_beta_rc
cpxs_betacpxs_beta
cpxs_theta_rccpxs_theta_rc
cpxs_thetacpxs_theta
cpxs_inv_appl1cpxs_inv_appl1
lpx_cpx_translpx_cpx_trans
cpx_bind2cpx_bind2
lpx_cpxs_translpx_cpxs_trans
cpxs_bind2_dxcpxs_bind2_dx
fqu_cpxs_trans_neqfqu_cpxs_trans_neq
fquq_cpxs_trans_neqfquq_cpxs_trans_neq
fqup_cpxs_trans_neqfqup_cpxs_trans_neq
fqus_cpxs_trans_neqfqus_cpxs_trans_neq
scpds_strap2scpds_strap2
scpds_cprs_transscpds_cprs_trans
lstas_scpds_translstas_scpds_trans
scpds_inv_abst1scpds_inv_abst1
scpds_inv_abbr_abstscpds_inv_abbr_abst
scpds_inv_lstas_eqscpds_inv_lstas_eq
scpds_fwd_cpxsscpds_fwd_cpxs
scpds_conf_eqscpds_conf_eq
scpes_inv_lstas_eqscpes_inv_lstas_eq
cpcs_scpescpcs_scpes
scpes_inv_abst2scpes_inv_abst2
scpes_reflscpes_refl
lstas_scpes_translstas_scpes_trans
cprs_scpds_divcprs_scpds_div
scpes_transscpes_trans
scpes_canc_snscpes_canc_sn
scpes_canc_dxscpes_canc_dx
aaa_lstasaaa_lstas
lstas_aaa_conflstas_aaa_conf
scpds_aaa_confscpds_aaa_conf
scpes_aaa_monoscpes_aaa_mono
lsubr_inv_pair1_auxlsubr_inv_pair1_aux
lsubr_inv_pair1lsubr_inv_pair1
lsubr_translsubr_trans
applvapplv
applv_simpleapplv_simple
atat
at_inv_nil_auxat_inv_nil_aux
at_inv_nilat_inv_nil
at_inv_cons_auxat_inv_cons_aux
at_inv_consat_inv_cons
at_inv_cons_ltat_inv_cons_lt
at_inv_cons_geat_inv_cons_ge
minussminuss
minuss_inv_nil1_auxminuss_inv_nil1_aux
minuss_inv_nil1minuss_inv_nil1
minuss_inv_cons1_auxminuss_inv_cons1_aux
minuss_inv_cons1minuss_inv_cons1
minuss_inv_cons1_geminuss_inv_cons1_ge
minuss_inv_cons1_ltminuss_inv_cons1_lt
liftvliftv
liftv_inv_nil1_auxliftv_inv_nil1_aux
liftv_inv_nil1liftv_inv_nil1
liftv_inv_cons1_auxliftv_inv_cons1_aux
liftv_inv_cons1liftv_inv_cons1
liftv_totalliftv_total
plusspluss
pluss_inv_nil2pluss_inv_nil2
pluss_inv_cons2pluss_inv_cons2
liftslifts
lifts_inv_nil_auxlifts_inv_nil_aux
lifts_inv_nillifts_inv_nil
lifts_inv_cons_auxlifts_inv_cons_aux
lifts_inv_conslifts_inv_cons
lifts_inv_sort1lifts_inv_sort1
lifts_inv_lref1lifts_inv_lref1
lifts_inv_gref1lifts_inv_gref1
lifts_inv_bind1lifts_inv_bind1
lifts_inv_flat1lifts_inv_flat1
lifts_simple_dxlifts_simple_dx
lifts_simple_snlifts_simple_sn
lifts_bindlifts_bind
lifts_flatlifts_flat
lifts_totallifts_total
liftsvliftsv
lifts_inv_applv1lifts_inv_applv1
lifts_applvlifts_applv
dropsdrops
d_liftable1d_liftable1
d_liftables1d_liftables1
d_liftables1_alld_liftables1_all
drops_inv_nil_auxdrops_inv_nil_aux
drops_inv_nildrops_inv_nil
drops_inv_cons_auxdrops_inv_cons_aux
drops_inv_consdrops_inv_cons
drops_inv_skip2drops_inv_skip2
drops_skipdrops_skip
d1_liftable_liftablesd1_liftable_liftables
d1_liftables_liftables_alld1_liftables_liftables_all
aaa_liftsaaa_lifts
aaa_fqu_confaaa_fqu_conf
aaa_fquq_confaaa_fquq_conf
aaa_fqup_confaaa_fqup_conf
aaa_fqus_confaaa_fqus_conf
lsubdlsubd
lsubd_fwd_lsubrlsubd_fwd_lsubr
lsubd_inv_atom1_auxlsubd_inv_atom1_aux
lsubd_inv_atom1lsubd_inv_atom1
lsubd_inv_pair1_auxlsubd_inv_pair1_aux
lsubd_inv_pair1lsubd_inv_pair1
lsubd_inv_atom2_auxlsubd_inv_atom2_aux
lsubd_inv_atom2lsubd_inv_atom2
lsubd_inv_pair2_auxlsubd_inv_pair2_aux
lsubd_inv_pair2lsubd_inv_pair2
lsubd_refllsubd_refl
lsubd_drop_O1_conflsubd_drop_O1_conf
lsubd_drop_O1_translsubd_drop_O1_trans
lsubd_da_translsubd_da_trans
lsubd_da_conflsubd_da_conf
lsubd_translsubd_trans
aaa_daaaa_da
llpx_snllpx_sn
llpx_sn_inv_bind_auxllpx_sn_inv_bind_aux
llpx_sn_inv_bindllpx_sn_inv_bind
llpx_sn_inv_flat_auxllpx_sn_inv_flat_aux
llpx_sn_inv_flatllpx_sn_inv_flat
llpx_sn_fwd_lengthllpx_sn_fwd_length
llpx_sn_fwd_drop_snllpx_sn_fwd_drop_sn
llpx_sn_fwd_drop_dxllpx_sn_fwd_drop_dx
llpx_sn_fwd_lref_auxllpx_sn_fwd_lref_aux
llpx_sn_fwd_lrefllpx_sn_fwd_lref
llpx_sn_fwd_bind_snllpx_sn_fwd_bind_sn
llpx_sn_fwd_bind_dxllpx_sn_fwd_bind_dx
llpx_sn_fwd_flat_snllpx_sn_fwd_flat_sn
llpx_sn_fwd_flat_dxllpx_sn_fwd_flat_dx
llpx_sn_fwd_pair_snllpx_sn_fwd_pair_sn
llpx_sn_reflllpx_sn_refl
llpx_sn_Yllpx_sn_Y
llpx_sn_ge_upllpx_sn_ge_up
llpx_sn_gellpx_sn_ge
llpx_sn_bind_Ollpx_sn_bind_O
llpx_sn_collpx_sn_co
lreq_llpx_sn_translreq_llpx_sn_trans
llpx_sn_lreq_transllpx_sn_lreq_trans
llpx_sn_lreq_replllpx_sn_lreq_repl
llpx_sn_bind_repl_SOllpx_sn_bind_repl_SO
llpx_sn_fwd_lref_dxllpx_sn_fwd_lref_dx
llpx_sn_fwd_lref_snllpx_sn_fwd_lref_sn
llpx_sn_inv_lref_ge_dxllpx_sn_inv_lref_ge_dx
llpx_sn_inv_lref_ge_snllpx_sn_inv_lref_ge_sn
llpx_sn_inv_lref_ge_billpx_sn_inv_lref_ge_bi
llpx_sn_inv_S_auxllpx_sn_inv_S_aux
llpx_sn_inv_Sllpx_sn_inv_S
llpx_sn_inv_bind_Ollpx_sn_inv_bind_O
llpx_sn_fwd_bind_O_dxllpx_sn_fwd_bind_O_dx
llpx_sn_bind_repl_Ollpx_sn_bind_repl_O
llpx_sn_decllpx_sn_dec
llpx_sn_lift_lellpx_sn_lift_le
llpx_sn_lift_gellpx_sn_lift_ge
llpx_sn_inv_lift_lellpx_sn_inv_lift_le
llpx_sn_inv_lift_bellpx_sn_inv_lift_be
llpx_sn_inv_lift_gellpx_sn_inv_lift_ge
llpx_sn_inv_lift_Ollpx_sn_inv_lift_O
llpx_sn_drop_conf_Ollpx_sn_drop_conf_O
llpx_sn_drop_trans_Ollpx_sn_drop_trans_O
nllpx_sn_inv_bindnllpx_sn_inv_bind
nllpx_sn_inv_flatnllpx_sn_inv_flat
nllpx_sn_inv_bind_Onllpx_sn_inv_bind_O
ceqceq
lleqlleq
lleq_transitivelleq_transitive
lleq_indlleq_ind
lleq_inv_bindlleq_inv_bind
lleq_inv_flatlleq_inv_flat
lleq_fwd_lengthlleq_fwd_length
lleq_fwd_lreflleq_fwd_lref
lleq_fwd_drop_snlleq_fwd_drop_sn
lleq_fwd_drop_dxlleq_fwd_drop_dx
lleq_fwd_bind_snlleq_fwd_bind_sn
lleq_fwd_bind_dxlleq_fwd_bind_dx
lleq_fwd_flat_snlleq_fwd_flat_sn
lleq_fwd_flat_dxlleq_fwd_flat_dx
lleq_sortlleq_sort
lleq_skiplleq_skip
lleq_lreflleq_lref
lleq_freelleq_free
lleq_greflleq_gref
lleq_bindlleq_bind
lleq_flatlleq_flat
lleq_refllleq_refl
lleq_Ylleq_Y
lleq_symlleq_sym
lleq_ge_uplleq_ge_up
lleq_gelleq_ge
lleq_bind_Olleq_bind_O
llpx_sn_lreflllpx_sn_lrefl
lleq_bind_repl_Olleq_bind_repl_O
lleq_declleq_dec
lleq_llpx_sn_translleq_llpx_sn_trans
lleq_llpx_sn_conflleq_llpx_sn_conf
lleq_inv_lref_ge_dxlleq_inv_lref_ge_dx
lleq_inv_lref_ge_snlleq_inv_lref_ge_sn
lleq_inv_lref_ge_billeq_inv_lref_ge_bi
lleq_inv_lref_gelleq_inv_lref_ge
lleq_inv_Slleq_inv_S
lleq_inv_bind_Olleq_inv_bind_O
lleq_fwd_lref_dxlleq_fwd_lref_dx
lleq_fwd_lref_snlleq_fwd_lref_sn
lleq_fwd_bind_O_dxlleq_fwd_bind_O_dx
lleq_lift_lelleq_lift_le
lleq_lift_gelleq_lift_ge
lleq_inv_lift_lelleq_inv_lift_le
lleq_inv_lift_belleq_inv_lift_be
lleq_inv_lift_gelleq_inv_lift_ge
nlleq_inv_bindnlleq_inv_bind
nlleq_inv_flatnlleq_inv_flat
nlleq_inv_bind_Onlleq_inv_bind_O
lleq_aaa_translleq_aaa_trans
aaa_lleq_confaaa_lleq_conf
lsuba_translsuba_trans
ri2ri2
ib2ib2
crrcrr
crr_inv_sort_auxcrr_inv_sort_aux
crr_inv_sortcrr_inv_sort
crr_inv_lref_auxcrr_inv_lref_aux
crr_inv_lrefcrr_inv_lref
crr_inv_gref_auxcrr_inv_gref_aux
crr_inv_grefcrr_inv_gref
trr_inv_atomtrr_inv_atom
crr_inv_ib2_auxcrr_inv_ib2_aux
crr_inv_ib2crr_inv_ib2
crr_inv_appl_auxcrr_inv_appl_aux
crr_inv_applcrr_inv_appl
circir
cir_inv_deltacir_inv_delta
cir_inv_ri2cir_inv_ri2
cir_inv_ib2cir_inv_ib2
cir_inv_bindcir_inv_bind
cir_inv_applcir_inv_appl
cir_inv_flatcir_inv_flat
cir_sortcir_sort
cir_grefcir_gref
tir_atomtir_atom
cir_ib2cir_ib2
cir_applcir_appl
crxcrx
crr_crxcrr_crx
crx_inv_sort_auxcrx_inv_sort_aux
crx_inv_sortcrx_inv_sort
crx_inv_lref_auxcrx_inv_lref_aux
crx_inv_lrefcrx_inv_lref
crx_inv_gref_auxcrx_inv_gref_aux
crx_inv_grefcrx_inv_gref
trx_inv_atomtrx_inv_atom
crx_inv_ib2_auxcrx_inv_ib2_aux
crx_inv_ib2crx_inv_ib2
crx_inv_appl_auxcrx_inv_appl_aux
crx_inv_applcrx_inv_appl
cixcix
cix_inv_sortcix_inv_sort
cix_inv_deltacix_inv_delta
cix_inv_ri2cix_inv_ri2
cix_inv_ib2cix_inv_ib2
cix_inv_bindcix_inv_bind
cix_inv_applcix_inv_appl
cix_inv_flatcix_inv_flat
cix_inv_circix_inv_cir
cix_sortcix_sort
tix_lreftix_lref
cix_grefcix_gref
cix_ib2cix_ib2
cix_applcix_appl
cpx_fwd_cixcpx_fwd_cix
nlift_lref_be_SOnlift_lref_be_SO
nlift_bind_snnlift_bind_sn
nlift_bind_dxnlift_bind_dx
nlift_flat_snnlift_flat_sn
nlift_flat_dxnlift_flat_dx
nlift_inv_lref_be_SOnlift_inv_lref_be_SO
nlift_inv_bindnlift_inv_bind
nlift_inv_flatnlift_inv_flat
freesfrees
frees_transfrees_trans
frees_invfrees_inv
frees_inv_sortfrees_inv_sort
frees_inv_greffrees_inv_gref
frees_inv_lreffrees_inv_lref
frees_inv_lref_freefrees_inv_lref_free
frees_inv_lref_skipfrees_inv_lref_skip
frees_inv_lref_gefrees_inv_lref_ge
frees_inv_lref_ltfrees_inv_lref_lt
frees_inv_bindfrees_inv_bind
frees_inv_flatfrees_inv_flat
frees_lref_eqfrees_lref_eq
frees_lref_befrees_lref_be
frees_bind_snfrees_bind_sn
frees_bind_dxfrees_bind_dx
frees_flat_snfrees_flat_sn
frees_flat_dxfrees_flat_dx
frees_weakfrees_weak
frees_inv_bind_Ofrees_inv_bind_O
frees_decfrees_dec
frees_Sfrees_S
frees_bind_dx_Ofrees_bind_dx_O
frees_lift_gefrees_lift_ge
frees_inv_lift_befrees_inv_lift_be
frees_inv_lift_gefrees_inv_lift_ge
appendappend
d_appendable_snd_appendable_sn
append_atom_snappend_atom_sn
append_assocappend_assoc
append_lengthappend_length
ltail_lengthltail_length
lpair_ltaillpair_ltail
append_inj_snappend_inj_sn
append_inj_dxappend_inj_dx
append_inv_refl_dxappend_inv_refl_dx
append_inv_pair_dxappend_inv_pair_dx
length_inv_pos_dx_ltaillength_inv_pos_dx_ltail
length_inv_pos_sn_ltaillength_inv_pos_sn_ltail
lenv_ind_altlenv_ind_alt
drop_O1_append_sn_le_auxdrop_O1_append_sn_le_aux
drop_O1_append_sn_ledrop_O1_append_sn_le
drop_O1_inv_append1_gedrop_O1_inv_append1_ge
drop_O1_inv_append1_ledrop_O1_inv_append1_le
frees_appendfrees_append
frees_inv_append_auxfrees_inv_append_aux
frees_inv_appendfrees_inv_append
llorllor
llor_atomllor_atom
llor_tail_freesllor_tail_frees
llor_tail_cofreesllor_tail_cofrees
llor_skipllor_skip
llor_totalllor_total
lpx_sn_altlpx_sn_alt
lpx_sn_alt_fwd_lengthlpx_sn_alt_fwd_length
lpx_sn_alt_inv_atom1lpx_sn_alt_inv_atom1
lpx_sn_alt_inv_pair1lpx_sn_alt_inv_pair1
lpx_sn_alt_inv_atom2lpx_sn_alt_inv_atom2
lpx_sn_alt_inv_pair2lpx_sn_alt_inv_pair2
lpx_sn_alt_atomlpx_sn_alt_atom
lpx_sn_alt_pairlpx_sn_alt_pair
lpx_sn_lpx_sn_altlpx_sn_lpx_sn_alt
lpx_sn_alt_inv_lpx_snlpx_sn_alt_inv_lpx_sn
lpx_sn_intro_altlpx_sn_intro_alt
lpx_sn_inv_altlpx_sn_inv_alt
llpx_sn_alt_rllpx_sn_alt_r
llpx_sn_alt_r_intro_altllpx_sn_alt_r_intro_alt
llpx_sn_alt_r_ind_altllpx_sn_alt_r_ind_alt
llpx_sn_alt_r_inv_altllpx_sn_alt_r_inv_alt
llpx_sn_alt_r_inv_flatllpx_sn_alt_r_inv_flat
llpx_sn_alt_r_inv_bindllpx_sn_alt_r_inv_bind
llpx_sn_alt_r_fwd_lengthllpx_sn_alt_r_fwd_length
llpx_sn_alt_r_fwd_lrefllpx_sn_alt_r_fwd_lref
llpx_sn_alt_r_sortllpx_sn_alt_r_sort
llpx_sn_alt_r_grefllpx_sn_alt_r_gref
llpx_sn_alt_r_skipllpx_sn_alt_r_skip
llpx_sn_alt_r_freellpx_sn_alt_r_free
llpx_sn_alt_r_lrefllpx_sn_alt_r_lref
llpx_sn_alt_r_flatllpx_sn_alt_r_flat
llpx_sn_alt_r_bindllpx_sn_alt_r_bind
llpx_sn_lpx_sn_alt_rllpx_sn_lpx_sn_alt_r
llpx_sn_alt_r_inv_lpx_snllpx_sn_alt_r_inv_lpx_sn
llpx_sn_intro_alt_rllpx_sn_intro_alt_r
llpx_sn_ind_alt_rllpx_sn_ind_alt_r
llpx_sn_inv_alt_rllpx_sn_inv_alt_r
llpx_sn_altllpx_sn_alt
llpx_sn_llpx_sn_altllpx_sn_llpx_sn_alt
llpx_sn_alt_inv_llpx_snllpx_sn_alt_inv_llpx_sn
lleq_intro_altlleq_intro_alt
lleq_inv_altlleq_inv_alt
llpx_sn_llor_fwd_snllpx_sn_llor_fwd_sn
lpx_sn_llpx_snlpx_sn_llpx_sn
lreq_lleq_translreq_lleq_trans
lleq_lreq_translleq_lreq_trans
lleq_lreq_repllleq_lreq_repl
lleq_bind_repl_SOlleq_bind_repl_SO
llpx_sn_frees_trans_auxllpx_sn_frees_trans_aux
llpx_sn_frees_transllpx_sn_frees_trans
llpx_sn_llor_dxllpx_sn_llor_dx
llpx_sn_llor_dx_symllpx_sn_llor_dx_sym
lreq_cpx_translreq_cpx_trans
cpx_llpx_sn_confcpx_llpx_sn_conf
lleq_cpx_translleq_cpx_trans
cpx_lleq_confcpx_lleq_conf
cpx_lleq_conf_sncpx_lleq_conf_sn
cpx_lleq_conf_dxcpx_lleq_conf_dx
lreq_frees_translreq_frees_trans
frees_lreq_conffrees_lreq_conf
lpx_cpx_frees_translpx_cpx_frees_trans
cpx_frees_transcpx_frees_trans
lpx_frees_translpx_frees_trans
lleq_lpx_translleq_lpx_trans
lpx_lleq_fqu_translpx_lleq_fqu_trans
lpx_lleq_fquq_translpx_lleq_fquq_trans
lpx_lleq_fqup_translpx_lleq_fqup_trans
lpx_lleq_fqus_translpx_lleq_fqus_trans
lreq_lpx_trans_lleq_auxlreq_lpx_trans_lleq_aux
lreq_lpx_trans_lleqlreq_lpx_trans_lleq
cnx_inv_crxcnx_inv_crx
fleqfleq
fleq_reflfleq_refl
fleq_symfleq_sym
fleq_inv_genfleq_inv_gen
lleq_fqu_translleq_fqu_trans
lleq_fquq_translleq_fquq_trans
lleq_fqup_translleq_fqup_trans
lleq_fqus_translleq_fqus_trans
lleq_translleq_trans
lleq_canc_snlleq_canc_sn
lleq_canc_dxlleq_canc_dx
lleq_nlleq_translleq_nlleq_trans
nlleq_lleq_divnlleq_lleq_div
fpbfpb
cpr_fpbcpr_fpb
lpr_fpblpr_fpb
lleq_fpb_translleq_fpb_trans
fleq_fpb_transfleq_fpb_trans
fpb_inv_fleqfpb_inv_fleq
fpbqfpbq
fpbq_reflfpbq_refl
cpr_fpbqcpr_fpbq
lpr_fpbqlpr_fpbq
fpbqafpbqa
fleq_fpbqfleq_fpbq
fpb_fpbqfpb_fpbq
fpbq_fpbqafpbq_fpbqa
fpbqa_inv_fpbqfpbqa_inv_fpbq
fpbq_ind_altfpbq_ind_alt
fpb_fpbq_altfpb_fpbq_alt
fpbq_inv_fpb_altfpbq_inv_fpb_alt
fpbq_aaa_conffpbq_aaa_conf
cpr_fwd_circpr_fwd_cir
sta_fpbsta_fpb
crr_liftcrr_lift
crr_inv_liftcrr_inv_lift
cir_liftcir_lift
cir_inv_liftcir_inv_lift
cpr_llpx_sn_confcpr_llpx_sn_conf
crx_liftcrx_lift
crx_inv_liftcrx_inv_lift
cnx_liftcnx_lift
cnx_inv_liftcnx_inv_lift
cnr_inv_crrcnr_inv_crr
cnr_lref_abstcnr_lref_abst
cnr_liftcnr_lift
cnr_inv_liftcnr_inv_lift
cir_cnrcir_cnr
cnr_inv_circnr_inv_cir
cix_lrefcix_lref
cix_liftcix_lift
cix_inv_liftcix_inv_lift
sta_fpbqsta_fpbq
cix_cnxcix_cnx
cnx_inv_cixcnx_inv_cix
lstas_llpx_sn_conflstas_llpx_sn_conf
unfoldunfold
lsubylsuby
lsuby_pair_ltlsuby_pair_lt
lsuby_succ_ltlsuby_succ_lt
lsuby_pair_O_Ylsuby_pair_O_Y
lsuby_refllsuby_refl
lsuby_O2lsuby_O2
lsuby_symlsuby_sym
lsuby_inv_atom1_auxlsuby_inv_atom1_aux
lsuby_inv_atom1lsuby_inv_atom1
lsuby_inv_zero1_auxlsuby_inv_zero1_aux
lsuby_inv_zero1lsuby_inv_zero1
lsuby_inv_pair1_auxlsuby_inv_pair1_aux
lsuby_inv_pair1lsuby_inv_pair1
lsuby_inv_succ1_auxlsuby_inv_succ1_aux
lsuby_inv_succ1lsuby_inv_succ1
lsuby_inv_zero2_auxlsuby_inv_zero2_aux
lsuby_inv_zero2lsuby_inv_zero2
lsuby_inv_pair2_auxlsuby_inv_pair2_aux
lsuby_inv_pair2lsuby_inv_pair2
lsuby_inv_succ2_auxlsuby_inv_succ2_aux
lsuby_inv_succ2lsuby_inv_succ2
lsuby_fwd_lengthlsuby_fwd_length
lsuby_drop_trans_belsuby_drop_trans_be
cpycpy
lsuby_cpy_translsuby_cpy_trans
cpy_reflcpy_refl
cpy_fullcpy_full
cpy_weakcpy_weak
cpy_weak_topcpy_weak_top
cpy_weak_fullcpy_weak_full
cpy_split_upcpy_split_up
cpy_split_downcpy_split_down
cpy_fwd_upcpy_fwd_up
cpy_fwd_twcpy_fwd_tw
cpy_inv_atom1_auxcpy_inv_atom1_aux
cpy_inv_atom1cpy_inv_atom1
cpy_inv_sort1cpy_inv_sort1
cpy_inv_lref1cpy_inv_lref1
cpy_inv_gref1cpy_inv_gref1
cpy_inv_bind1_auxcpy_inv_bind1_aux
cpy_inv_bind1cpy_inv_bind1
cpy_inv_flat1_auxcpy_inv_flat1_aux
cpy_inv_flat1cpy_inv_flat1
cpy_inv_refl_O2_auxcpy_inv_refl_O2_aux
cpy_inv_refl_O2cpy_inv_refl_O2
cpy_inv_lift1_eqcpy_inv_lift1_eq
cpy_lift_lecpy_lift_le
cpy_lift_becpy_lift_be
cpy_lift_gecpy_lift_ge
cpy_inv_lift1_lecpy_inv_lift1_le
cpy_inv_lift1_becpy_inv_lift1_be
cpy_inv_lift1_gecpy_inv_lift1_ge
cpy_inv_lift1_ge_upcpy_inv_lift1_ge_up
cpy_inv_lift1_be_upcpy_inv_lift1_be_up
cpy_inv_lift1_le_upcpy_inv_lift1_le_up
cpy_conf_eqcpy_conf_eq
cpy_conf_neqcpy_conf_neq
cpy_trans_gecpy_trans_ge
cpy_trans_downcpy_trans_down
cpy_fwd_nlift2_gecpy_fwd_nlift2_ge
ggetgget
gget_inv_gtgget_inv_gt
gget_inv_eqgget_inv_eq
gget_inv_lt_auxgget_inv_lt_aux
gget_inv_ltgget_inv_lt
gget_totalgget_total
gget_monogget_mono
gget_decgget_dec
lsuby_translsuby_trans
liftv_monoliftv_mono
csxcsx
csx_indcsx_ind
csx_introcsx_intro
csx_cpx_transcsx_cpx_trans
cnx_csxcnx_csx
csx_sortcsx_sort
csx_castcsx_cast
csx_fwd_pair_sn_auxcsx_fwd_pair_sn_aux
csx_fwd_pair_sncsx_fwd_pair_sn
csx_fwd_bind_dx_auxcsx_fwd_bind_dx_aux
csx_fwd_bind_dxcsx_fwd_bind_dx
csx_fwd_flat_dx_auxcsx_fwd_flat_dx_aux
csx_fwd_flat_dxcsx_fwd_flat_dx
csx_fwd_bindcsx_fwd_bind
csx_fwd_flatcsx_fwd_flat
cprecpre
csx_cprecsx_cpre
cpre_monocpre_mono
lpxslpxs
lpxs_indlpxs_ind
lpxs_ind_dxlpxs_ind_dx
lprs_lpxslprs_lpxs
lpx_lpxslpx_lpxs
lpxs_refllpxs_refl
lpxs_strap1lpxs_strap1
lpxs_strap2lpxs_strap2
lpxs_pair_refllpxs_pair_refl
lpxs_inv_atom1lpxs_inv_atom1
lpxs_inv_atom2lpxs_inv_atom2
lpxs_fwd_lengthlpxs_fwd_length
fpbsfpbs
fpbs_indfpbs_ind
fpbs_ind_dxfpbs_ind_dx
fpbs_reflfpbs_refl
fpbq_fpbsfpbq_fpbs
fpbs_strap1fpbs_strap1
fpbs_strap2fpbs_strap2
fqup_fpbsfqup_fpbs
fqus_fpbsfqus_fpbs
cpxs_fpbscpxs_fpbs
lpxs_fpbslpxs_fpbs
lleq_fpbslleq_fpbs
cprs_fpbscprs_fpbs
lprs_fpbslprs_fpbs
fpbs_fqus_transfpbs_fqus_trans
fpbs_fqup_transfpbs_fqup_trans
fpbs_cpxs_transfpbs_cpxs_trans
fpbs_lpxs_transfpbs_lpxs_trans
fpbs_lleq_transfpbs_lleq_trans
fqus_fpbs_transfqus_fpbs_trans
cpxs_fpbs_transcpxs_fpbs_trans
lpxs_fpbs_translpxs_fpbs_trans
lleq_fpbs_translleq_fpbs_trans
cpxs_fqus_fpbscpxs_fqus_fpbs
cpxs_fqup_fpbscpxs_fqup_fpbs
fqus_lpxs_fpbsfqus_lpxs_fpbs
cpxs_fqus_lpxs_fpbscpxs_fqus_lpxs_fpbs
lpxs_lleq_fpbslpxs_lleq_fpbs
cpr_lpr_fpbscpr_lpr_fpbs
fpbgfpbg
fpb_fpbgfpb_fpbg
fpbg_fpbq_transfpbg_fpbq_trans
sta_fpbgsta_fpbg
csx_lleq_confcsx_lleq_conf
csx_lleq_transcsx_lleq_trans
fpbs_transfpbs_trans
lreq_cpxs_translreq_cpxs_trans
lpxs_drop_conflpxs_drop_conf
drop_lpxs_transdrop_lpxs_trans
lpxs_drop_trans_O1lpxs_drop_trans_O1
lpxs_pairlpxs_pair
lpxs_inv_pair1lpxs_inv_pair1
lpxs_inv_pair2lpxs_inv_pair2
lpxs_ind_altlpxs_ind_alt
lpxs_cpx_translpxs_cpx_trans
lpxs_cpxs_translpxs_cpxs_trans
cpxs_bind2cpxs_bind2
cpxs_inv_abst1cpxs_inv_abst1
cpxs_inv_abbr1cpxs_inv_abbr1
lpxs_pair2lpxs_pair2
lpx_fqup_translpx_fqup_trans
lpx_fqus_translpx_fqus_trans
lpxs_fquq_translpxs_fquq_trans
lpxs_fqup_translpxs_fqup_trans
lpxs_fqus_translpxs_fqus_trans
lleq_lpxs_translleq_lpxs_trans
lpxs_nlleq_inv_step_snlpxs_nlleq_inv_step_sn
lpxs_lleq_fqu_translpxs_lleq_fqu_trans
lpxs_lleq_fquq_translpxs_lleq_fquq_trans
lpxs_lleq_fqup_translpxs_lleq_fqup_trans
lpxs_lleq_fqus_translpxs_lleq_fqus_trans
lreq_lpxs_trans_lleq_auxlreq_lpxs_trans_lleq_aux
lreq_lpxs_trans_lleqlreq_lpxs_trans_lleq
lstas_fpbslstas_fpbs
sta_fpbssta_fpbs
cpr_lpr_sta_fpbscpr_lpr_sta_fpbs
fleq_transfleq_trans
fleq_canc_snfleq_canc_sn
fleq_canc_dxfleq_canc_dx
fpbg_fleq_transfpbg_fleq_trans
fleq_fpbg_transfleq_fpbg_trans
fleq_fpbsfleq_fpbs
fpbg_fwd_fpbsfpbg_fwd_fpbs
fpbs_fpbgfpbs_fpbg
fpbs_fpb_transfpbs_fpb_trans
fpb_fpbg_transfpb_fpbg_trans
fpbq_fpbg_transfpbq_fpbg_trans
fpbs_fpbg_transfpbs_fpbg_trans
fpbg_fpbs_transfpbg_fpbs_trans
fqup_fpbgfqup_fpbg
cpxs_fpbgcpxs_fpbg
lstas_fpbglstas_fpbg
lpxs_fpbglpxs_fpbg
fsbfsb
fsb_ind_altfsb_ind_alt
fsb_inv_csxfsb_inv_csx
fsbafsba
fsba_ind_altfsba_ind_alt
fsba_fpbs_transfsba_fpbs_trans
fsb_fsbafsb_fsba
fsba_inv_fsbfsba_inv_fsb
fsb_fpbs_transfsb_fpbs_trans
fsb_ind_fpbgfsb_ind_fpbg
lpxs_translpxs_trans
lsxlsx
lsx_indlsx_ind
lsx_introlsx_intro
lsx_atomlsx_atom
lsx_sortlsx_sort
lsx_greflsx_gref
lsx_ge_uplsx_ge_up
lsx_gelsx_ge
lsx_fwd_bind_snlsx_fwd_bind_sn
lsx_fwd_flat_snlsx_fwd_flat_sn
lsx_fwd_flat_dxlsx_fwd_flat_dx
lsx_fwd_pair_snlsx_fwd_pair_sn
lsx_inv_flatlsx_inv_flat
lsxalsxa
lsxa_indlsxa_ind
lsxa_introlsxa_intro
lsxa_intro_auxlsxa_intro_aux
lsxa_lleq_translsxa_lleq_trans
lsxa_lpxs_translsxa_lpxs_trans
lsxa_intro_lpxlsxa_intro_lpx
lsx_lsxalsx_lsxa
lsxa_inv_lsxlsxa_inv_lsx
lsx_intro_altlsx_intro_alt
lsx_lpxs_translsx_lpxs_trans
lsx_ind_altlsx_ind_alt
lsx_bind_lpxs_auxlsx_bind_lpxs_aux
lsx_bindlsx_bind
lsx_flat_lpxslsx_flat_lpxs
lsx_flatlsx_flat
tstststs
tsts_inv_atom1_auxtsts_inv_atom1_aux
tsts_inv_atom1tsts_inv_atom1
tsts_inv_pair1_auxtsts_inv_pair1_aux
tsts_inv_pair1tsts_inv_pair1
tsts_inv_atom2_auxtsts_inv_atom2_aux
tsts_inv_atom2tsts_inv_atom2
tsts_inv_pair2_auxtsts_inv_pair2_aux
tsts_inv_pair2tsts_inv_pair2
tsts_refltsts_refl
tsts_symtsts_sym
tsts_dectsts_dec
simple_tsts_repl_dxsimple_tsts_repl_dx
simple_tsts_repl_snsimple_tsts_repl_sn
tsts_tranststs_trans
tsts_canc_sntsts_canc_sn
tsts_canc_dxtsts_canc_dx
csxacsxa
csxa_indcsxa_ind
csx_intro_cpxscsx_intro_cpxs
csxa_introcsxa_intro
csxa_intro_auxcsxa_intro_aux
csxa_cpxs_transcsxa_cpxs_trans
csxa_intro_cpxcsxa_intro_cpx
csx_csxacsx_csxa
csxa_csxcsxa_csx
csx_cpxs_transcsx_cpxs_trans
csx_ind_altcsx_ind_alt
nfnf
candidatecandidate
CP0CP0
CP1CP1
CP2CP2
CP3CP3
gcpgcp
gcp0_liftsgcp0_lifts
gcp2_liftsgcp2_lifts
gcp2_lifts_allgcp2_lifts_all
csx_liftcsx_lift
csx_inv_liftcsx_inv_lift
csx_inv_lref_bindcsx_inv_lref_bind
csx_lref_bindcsx_lref_bind
csx_appl_simplecsx_appl_simple
csx_fqu_confcsx_fqu_conf
csx_fquq_confcsx_fquq_conf
csx_fqup_confcsx_fqup_conf
csx_fqus_confcsx_fqus_conf
csx_gcpcsx_gcp
csx_lpx_confcsx_lpx_conf
csx_abstcsx_abst
csx_abbrcsx_abbr
csx_appl_beta_auxcsx_appl_beta_aux
csx_appl_betacsx_appl_beta
csx_appl_theta_auxcsx_appl_theta_aux
csx_appl_thetacsx_appl_theta
csx_appl_simple_tstscsx_appl_simple_tsts
csx_lpxs_confcsx_lpxs_conf
lsx_lref_freelsx_lref_free
lsx_lref_skiplsx_lref_skip
lsx_fwd_lref_belsx_fwd_lref_be
lsx_lift_lelsx_lift_le
lsx_lift_gelsx_lift_ge
lsx_inv_lift_lelsx_inv_lift_le
lsx_inv_lift_belsx_inv_lift_be
lsx_inv_lift_gelsx_inv_lift_ge
lsx_lleq_translsx_lleq_trans
lsx_lpx_translsx_lpx_trans
lsx_lreq_conflsx_lreq_conf
lsx_fwd_bind_dxlsx_fwd_bind_dx
lsx_inv_bindlsx_inv_bind
lcosxlcosx
lcosx_Olcosx_O
lcosx_drop_trans_ltlcosx_drop_trans_lt
lcosx_inv_succ_auxlcosx_inv_succ_aux
lcosx_inv_succlcosx_inv_succ
lcosx_inv_pairlcosx_inv_pair
lsx_cpx_trans_lcosxlsx_cpx_trans_lcosx
lsx_cpx_trans_Olsx_cpx_trans_O
lsx_lref_be_lpxslsx_lref_be_lpxs
lsx_lref_belsx_lref_be
csx_lsxcsx_lsx
fpbs_aaa_conffpbs_aaa_conf
at_monoat_mono
lifts_lift_trans_lelifts_lift_trans_le
lifts_lift_translifts_lift_trans
liftsv_liftv_trans_leliftsv_liftv_trans_le
drops_drop_transdrops_drop_trans
S1S1
S2S2
S3S3
S4S4
S5S5
S6S6
S7S7
gcrgcr
cfuncfun
acracr
gcr_liftgcr_lift
gcr_liftsgcr_lifts
acr_gcracr_gcr
acr_abstacr_abst
cpxs_fwd_cnxcpxs_fwd_cnx
cpxs_fwd_sortcpxs_fwd_sort
cpxs_fwd_betacpxs_fwd_beta
cpxs_fwd_deltacpxs_fwd_delta
cpxs_fwd_thetacpxs_fwd_theta
cpxs_fwd_castcpxs_fwd_cast
lleq_cpxs_translleq_cpxs_trans
cpxs_lleq_confcpxs_lleq_conf
cpxs_lleq_conf_dxcpxs_lleq_conf_dx
cpxs_lleq_conf_sncpxs_lleq_conf_sn
lprs_drop_conflprs_drop_conf
drop_lprs_transdrop_lprs_trans
lprs_drop_trans_O1lprs_drop_trans_O1
fpbg_transfpbg_trans
scpds_liftscpds_lift
scpds_inv_lift1scpds_inv_lift1
lifts_translifts_trans
drops_transdrops_trans
lsubclsubc
lsubc_inv_atom1_auxlsubc_inv_atom1_aux
lsubc_inv_atom1lsubc_inv_atom1
lsubc_inv_pair1_auxlsubc_inv_pair1_aux
lsubc_inv_pair1lsubc_inv_pair1
lsubc_inv_atom2_auxlsubc_inv_atom2_aux
lsubc_inv_atom2lsubc_inv_atom2
lsubc_inv_pair2_auxlsubc_inv_pair2_aux
lsubc_inv_pair2lsubc_inv_pair2
lsubc_fwd_lsubrlsubc_fwd_lsubr
lsubc_refllsubc_refl
lsubc_drop_O1_translsubc_drop_O1_trans
drop_lsubc_transdrop_lsubc_trans
drops_lsubc_transdrops_lsubc_trans
acr_aaa_csubc_liftsacr_aaa_csubc_lifts
acr_aaaacr_aaa
gcr_aaagcr_aaa
tsts_inv_bind_applv_simpletsts_inv_bind_applv_simple
cpxs_fwd_cnx_vectorcpxs_fwd_cnx_vector
cpxs_fwd_sort_vectorcpxs_fwd_sort_vector
cpxs_fwd_beta_vectorcpxs_fwd_beta_vector
cpxs_fwd_delta_vectorcpxs_fwd_delta_vector
cpxs_fwd_theta_vectorcpxs_fwd_theta_vector
cpxs_fwd_cast_vectorcpxs_fwd_cast_vector
csxvcsxv
csxv_inv_conscsxv_inv_cons
csx_fwd_applvcsx_fwd_applv
csx_applv_cnxcsx_applv_cnx
csx_applv_sortcsx_applv_sort
csx_applv_betacsx_applv_beta
csx_applv_deltacsx_applv_delta
csx_applv_thetacsx_applv_theta
csx_applv_castcsx_applv_cast
csx_gcrcsx_gcr
aaa_csxaaa_csx
aaa_ind_csx_auxaaa_ind_csx_aux
aaa_ind_csxaaa_ind_csx
aaa_ind_csx_alt_auxaaa_ind_csx_alt_aux
aaa_ind_csx_altaaa_ind_csx_alt
lprs_striplprs_strip
lprs_conflprs_conf
lprs_translprs_trans
fpbsafpbsa
fpb_fpbsa_transfpb_fpbsa_trans
fpbs_fpbsafpbs_fpbsa
fpbsa_inv_fpbsfpbsa_inv_fpbs
fpbs_intro_altfpbs_intro_alt
fpbs_inv_altfpbs_inv_alt
fpbs_cpx_trans_neqfpbs_cpx_trans_neq
fpb_fpbsfpb_fpbs
csx_fpb_confcsx_fpb_conf
csx_fpbs_confcsx_fpbs_conf
csx_fsb_fpbscsx_fsb_fpbs
csx_fsbcsx_fsb
csx_ind_fpbcsx_ind_fpb
csx_ind_fpbgcsx_ind_fpbg
aaa_fsbaaa_fsb
aaa_fsbaaaa_fsba
aaa_ind_fpb_auxaaa_ind_fpb_aux
aaa_ind_fpbaaa_ind_fpb
aaa_ind_fpbg_auxaaa_ind_fpbg_aux
aaa_ind_fpbgaaa_ind_fpbg
cpxecpxe
csx_cpxecsx_cpxe
lpxs_aaa_conflpxs_aaa_conf
lprs_aaa_conflprs_aaa_conf
lsuba_lsubclsuba_lsubc
ApplDeltaApplDelta
ApplOmega1ApplOmega1
ApplOmega2ApplOmega2
ApplOmega3ApplOmega3
ApplDelta_liftApplDelta_lift
cpr_ApplOmega_12cpr_ApplOmega_12
cpr_ApplOmega_23cpr_ApplOmega_23
cpxs_ApplOmega_13cpxs_ApplOmega_13
fqup_ApplOmega_13fqup_ApplOmega_13
fpbg_reflfpbg_refl
DeltaDelta
Omega1Omega1
Omega2Omega2
Delta_liftDelta_lift
cpr_Omega_12cpr_Omega_12
cpr_Omega_21cpr_Omega_21
sta_ldecsta_ldec
snvsnv
snv_inv_lref_auxsnv_inv_lref_aux
snv_inv_lrefsnv_inv_lref
snv_inv_gref_auxsnv_inv_gref_aux
snv_inv_grefsnv_inv_gref
snv_inv_bind_auxsnv_inv_bind_aux
snv_inv_bindsnv_inv_bind
snv_inv_appl_auxsnv_inv_appl_aux
snv_inv_applsnv_inv_appl
snv_inv_cast_auxsnv_inv_cast_aux
snv_inv_castsnv_inv_cast
snv_extendedsnv_extended
snv_restrictedsnv_restricted
snv_fwd_aaasnv_fwd_aaa
snv_fwd_dasnv_fwd_da
snv_fwd_lstassnv_fwd_lstas
snv_fwd_fsbsnv_fwd_fsb
snv_liftsnv_lift
snv_inv_liftsnv_inv_lift
snv_fqu_confsnv_fqu_conf
snv_fquq_confsnv_fquq_conf
snv_fqup_confsnv_fqup_conf
snv_fqus_confsnv_fqus_conf
IH_snv_cpr_lprIH_snv_cpr_lpr
IH_da_cpr_lprIH_da_cpr_lpr
IH_lstas_cpr_lprIH_lstas_cpr_lpr
IH_snv_lstasIH_snv_lstas
snv_cprs_lpr_auxsnv_cprs_lpr_aux
da_cprs_lpr_auxda_cprs_lpr_aux
da_scpds_lpr_auxda_scpds_lpr_aux
da_scpes_auxda_scpes_aux
lstas_cprs_lpr_auxlstas_cprs_lpr_aux
scpds_cpr_lpr_auxscpds_cpr_lpr_aux
scpes_cpr_lpr_auxscpes_cpr_lpr_aux
lstas_scpds_auxlstas_scpds_aux
scpes_le_auxscpes_le_aux
snv_cast_scpessnv_cast_scpes
shnvshnv
shnv_inv_cast_auxshnv_inv_cast_aux
shnv_inv_castshnv_inv_cast
shnv_inv_snvshnv_inv_snv
snv_shnv_castsnv_shnv_cast
lsubsvlsubsv
lsubsv_inv_atom1_auxlsubsv_inv_atom1_aux
lsubsv_inv_atom1lsubsv_inv_atom1
lsubsv_inv_pair1_auxlsubsv_inv_pair1_aux
lsubsv_inv_pair1lsubsv_inv_pair1
lsubsv_inv_atom2_auxlsubsv_inv_atom2_aux
lsubsv_inv_atom2lsubsv_inv_atom2
lsubsv_inv_pair2_auxlsubsv_inv_pair2_aux
lsubsv_inv_pair2lsubsv_inv_pair2
lsubsv_fwd_lsubrlsubsv_fwd_lsubr
lsubsv_refllsubsv_refl
lsubsv_cprs_translsubsv_cprs_trans
lsubsv_drop_O1_conflsubsv_drop_O1_conf
lsubsv_drop_O1_translsubsv_drop_O1_trans
lsubsv_fwd_lsubdlsubsv_fwd_lsubd
lsubsv_lstas_translsubsv_lstas_trans
lsubsv_sta_translsubsv_sta_trans
lsubsv_scpds_translsubsv_scpds_trans
lsubsv_snv_translsubsv_snv_trans
snv_cpr_lpr_auxsnv_cpr_lpr_aux
lstas_cpr_lpr_auxlstas_cpr_lpr_aux
snv_lstas_auxsnv_lstas_aux
lsubsv_fwd_lsubalsubsv_fwd_lsuba
da_cpr_lpr_auxda_cpr_lpr_aux
lsubsv_cpcs_translsubsv_cpcs_trans
snv_preservesnv_preserve
da_cpr_lprda_cpr_lpr
snv_cpr_lprsnv_cpr_lpr
snv_lstassnv_lstas
lstas_cpr_lprlstas_cpr_lpr
snv_cprs_lprsnv_cprs_lpr
da_cprs_lprda_cprs_lpr
lstas_cprs_lprlstas_cprs_lpr
lstas_cpcs_lprlstas_cpcs_lpr
cpyscpys
cpys_indcpys_ind
cpys_ind_dxcpys_ind_dx
cpy_cpyscpy_cpys
cpys_strap1cpys_strap1
cpys_strap2cpys_strap2
lsuby_cpys_translsuby_cpys_trans
cpys_reflcpys_refl
cpys_bindcpys_bind
cpys_flatcpys_flat
cpys_weakcpys_weak
cpys_weak_topcpys_weak_top
cpys_weak_fullcpys_weak_full
cpys_fwd_upcpys_fwd_up
cpys_fwd_twcpys_fwd_tw
cpys_inv_sort1cpys_inv_sort1
cpys_inv_gref1cpys_inv_gref1
cpys_inv_bind1cpys_inv_bind1
cpys_inv_flat1cpys_inv_flat1
cpys_inv_refl_O2cpys_inv_refl_O2
cpys_inv_lift1_eqcpys_inv_lift1_eq
cpys_substcpys_subst
cpys_subst_Y2cpys_subst_Y2
cpys_inv_atom1cpys_inv_atom1
cpys_inv_lref1cpys_inv_lref1
cpys_inv_lref1_Y2cpys_inv_lref1_Y2
cpys_inv_lref1_dropcpys_inv_lref1_drop
cpys_lift_lecpys_lift_le
cpys_lift_becpys_lift_be
cpys_lift_gecpys_lift_ge
cpys_inv_lift1_lecpys_inv_lift1_le
cpys_inv_lift1_becpys_inv_lift1_be
cpys_inv_lift1_gecpys_inv_lift1_ge
cpys_inv_lift1_ge_upcpys_inv_lift1_ge_up
cpys_inv_lift1_be_upcpys_inv_lift1_be_up
cpys_inv_lift1_le_upcpys_inv_lift1_le_up
cpys_inv_lift1_substcpys_inv_lift1_subst
cpysacpysa
lsuby_cpysa_translsuby_cpysa_trans
cpysa_reflcpysa_refl
cpysa_cpy_transcpysa_cpy_trans
cpys_cpysacpys_cpysa
cpysa_inv_cpyscpysa_inv_cpys
cpys_ind_altcpys_ind_alt
cpys_inv_SO2cpys_inv_SO2
cpys_strip_eqcpys_strip_eq
cpys_strip_neqcpys_strip_neq
cpys_strap1_downcpys_strap1_down
cpys_strap2_downcpys_strap2_down
cpys_split_upcpys_split_up
cpys_inv_lift1_upcpys_inv_lift1_up
cpys_conf_eqcpys_conf_eq
cpys_conf_neqcpys_conf_neq
cpys_trans_eqcpys_trans_eq
cpys_trans_downcpys_trans_down
cpys_antisym_eqcpys_antisym_eq
llpx_sn_TC_pair_dxllpx_sn_TC_pair_dx
fqup_transfqup_trans
lleq_intro_alt_rlleq_intro_alt_r
lleq_ind_alt_rlleq_ind_alt_r
lleq_inv_alt_rlleq_inv_alt_r
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html deleted file mode 100644 index f77e224f3..000000000 --- a/helm/www/lambdadelta/documentation.html +++ /dev/null @@ -1,406 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Documentation [butterfly] -
-
- BibTeX database of λδ documentation: - download - lambdadelta.bib, - view - lambdadelta.txt - (revised 2017-09). -
-
- [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.
- -
-
-
-
- [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.
- -
-
-
-
- [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 (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.
- -
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 70ddb4a96..6863484b7 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -1,5 +1,16 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@techreport{lambdadeltaR3a, + author="Ferruccio {Guidi}", + title="{The Formal System $\lambda\Upsilon\mathrm{P}$}", + type="Technical Report", + number="AMS Acta 5754", + institution="University of Bologna", + address="Bologna, Italy", + year="2018", + month="January" +} + @article{lambdadeltaJ3a, author="Ferruccio {Guidi}", title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}", @@ -25,7 +36,7 @@ } @techreport{lambdadeltaR2c, - author="Ferruccio {Guidi}", + author="Ferruccio {Guidi}", title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}", type="Technical Report", number="AMS Acta 4411", @@ -45,8 +56,8 @@ } @incollection{lambdadeltaR2b, - author="Ferruccio {Guidi}", - title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}" + author="Ferruccio {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", editor="Fernando {Ferreira} and H\'elia {Guerra} and Elvira {Mayordomo} and Jo\~ao {Rasga}", booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", pages="204--213", @@ -57,8 +68,8 @@ } @techreport{lambdadeltaR2a, - author="Ferruccio {Guidi}", - title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + author="Ferruccio {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", type="Technical Report", number="UBLCS 2009-16", institution="University of Bologna", @@ -84,9 +95,6 @@ @incollection{lambdadeltaR1c, author="Ferruccio {Guidi}", - - - title="{Lambda Types on the Lambda Calculus with Abbreviations}", editor="Stuart Barry {Cooper} and Thomas F. {Kent} and Benedikt {L\"owe} and Andrea {Sorbi}", @comment="{\"}", booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", @@ -98,8 +106,8 @@ } @techreport{lambdadeltaR1b, - author="Ferruccio {Guidi}", - title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + author="Ferruccio {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", type="Technical Report", number="UBLCS 2006-25", institution="University of Bologna", @@ -109,8 +117,8 @@ } @techreport{lambdadeltaR1a, - author="Ferruccio {Guidi}", - title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + author="Ferruccio {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", type="Technical Report", number="UBLCS 2006-01", institution="University of Bologna", diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 70ddb4a96..6863484b7 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -1,5 +1,16 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@techreport{lambdadeltaR3a, + author="Ferruccio {Guidi}", + title="{The Formal System $\lambda\Upsilon\mathrm{P}$}", + type="Technical Report", + number="AMS Acta 5754", + institution="University of Bologna", + address="Bologna, Italy", + year="2018", + month="January" +} + @article{lambdadeltaJ3a, author="Ferruccio {Guidi}", title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}", @@ -25,7 +36,7 @@ } @techreport{lambdadeltaR2c, - author="Ferruccio {Guidi}", + author="Ferruccio {Guidi}", title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}", type="Technical Report", number="AMS Acta 4411", @@ -45,8 +56,8 @@ } @incollection{lambdadeltaR2b, - author="Ferruccio {Guidi}", - title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}" + author="Ferruccio {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", editor="Fernando {Ferreira} and H\'elia {Guerra} and Elvira {Mayordomo} and Jo\~ao {Rasga}", booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", pages="204--213", @@ -57,8 +68,8 @@ } @techreport{lambdadeltaR2a, - author="Ferruccio {Guidi}", - title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + author="Ferruccio {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", type="Technical Report", number="UBLCS 2009-16", institution="University of Bologna", @@ -84,9 +95,6 @@ @incollection{lambdadeltaR1c, author="Ferruccio {Guidi}", - - - title="{Lambda Types on the Lambda Calculus with Abbreviations}", editor="Stuart Barry {Cooper} and Thomas F. {Kent} and Benedikt {L\"owe} and Andrea {Sorbi}", @comment="{\"}", booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", @@ -98,8 +106,8 @@ } @techreport{lambdadeltaR1b, - author="Ferruccio {Guidi}", - title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + author="Ferruccio {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", type="Technical Report", number="UBLCS 2006-25", institution="University of Bologna", @@ -109,8 +117,8 @@ } @techreport{lambdadeltaR1a, - author="Ferruccio {Guidi}", - title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + author="Ferruccio {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", type="Technical Report", number="UBLCS 2006-01", institution="University of Bologna", diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html deleted file mode 100644 index ccc5ff801..000000000 --- a/helm/www/lambdadelta/ground_1.html +++ /dev/null @@ -1,296 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Summary of the Specification [butterfly] -
-
Here is a numerical account of the specification's contents - and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryobjects -
- 		-
- 		-
- 		-
- 		-
-
sizesfiles10characters15063nodes14881
propositionstheorems0lemmas50total50
conceptsdeclared24defined4total28
-
- - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
componentplanefiles -
- 		-
- 		-
-
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 -
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html deleted file mode 100644 index 4fb7ca304..000000000 --- a/helm/www/lambdadelta/ground_2.html +++ /dev/null @@ -1,918 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Summary of the Specification [butterfly] -
-
Here is a numerical account of the specification's contents - and its timeline. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
categoryunits -
- 		-
- 		-
- 		-
- 		-
-
sizescharacters (files)145725 (104)nodes (objects)337452 (911)intrinsic loss factor2.3
propositionstheorems42lemmas693total735
conceptsdeclared66defined73total139
-
- - - - - - -
Logical Structure of the Specification [butterfly] -
-
This table reports the specification's components and their planes. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
componentplanefiles -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
generic rt-transition counter - rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )rtc_shift ( ↓? )rtc_max ( ? ∨ ? )rtc_plus ( ? + ? ) -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
multiple relocation - rtmaprtmap_eq ( ? ≗ ? )rtmap_pushs ( ↑*[?]? )rtmap_nexts ( ⫯*[?]? )rtmap_tl ( ⫱? )rtmap_tls ( ⫱*[?]? )rtmap_isid ( 𝐈⦃?⦄ )rtmap_idrtmap_isdiv ( 𝛀⦃?⦄ )rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )rtmap_isfin ( 𝐅⦃?⦄ )rtmap_isuni ( 𝐔⦃?⦄ )rtmap_uni ( 𝐔❴?❵ )rtmap_sle ( ? ⊆ ? )rtmap_sdj ( ? ∥ ? )rtmap_sand ( ? ⋒ ? ≡ ? )rtmap_sor ( ? ⋓ ? ≡ ? )rtmap_at ( @⦃?,?⦄ ≡ ? )rtmap_istot ( 𝐓⦃?⦄ )rtmap_after ( ? ⊚ ? ≡ ? )rtmap_coafter ( ? ~⊚ ? ≡ ? )
-
- 		-
- 		nstream ( ↑? ) ( ⫯? )nstream_eq - - - - nstream_isidnstream_id ( 𝐈𝐝 ) - - - - - - - - nstream_sor - nstream_istot ( ?@❴?❵ )nstream_after ( ? ∘ ? )nstream_coafter ( ? ~∘ ? )
-
- 		-
- 		mr2mr2_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 ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
-
- 		-
- 		relations ( ? ⊆ ? )starlstar -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
generated logical decomposables - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
- - -
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
- 		-
-
-
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:01 +0100
- - diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html deleted file mode 100644 index 59aae3134..000000000 --- a/helm/www/lambdadelta/home.html +++ /dev/null @@ -1,302 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Foreword [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. - 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 [butterfly] -
-
- This is a list of publications citing λδ documentation. -
- - - - - - - - - - -
Disclaimer [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): -
- - - - - - -
- [Smiling face] - 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. -
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html deleted file mode 100644 index 02abad18e..000000000 --- a/helm/www/lambdadelta/implementation.html +++ /dev/null @@ -1,307 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Tools [butterfly] -
-
- - [Open Symbolic Notation logo] - 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 logo] 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. -
- - - - -
- [\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. -
- - - -
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html deleted file mode 100644 index 31665034e..000000000 --- a/helm/www/lambdadelta/news.html +++ /dev/null @@ -1,385 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
- -
Milestones [butterfly] -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Visibility [butterfly] -
- - -
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html deleted file mode 100644 index 8348a7506..000000000 --- a/helm/www/lambdadelta/osn.html +++ /dev/null @@ -1,202 +0,0 @@ - - - - - - - - - - \lambda\delta home page: Open Symbolic Notation - - - - - - -
- - [Open Symbolic Notation logo] - -
-
Open Symbolic Notation
-
- [Spacer] -
-
- 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. -
- - - -
Grammar [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. -
- - - - - - - -
- The grammar of OSN is very liberal by design. - Spaces of the form 1 * gap can appear between any pair of tokens. -
- - - -
Semantics [butterfly] -
-
- Forthcoming ... -
- -
Implementation [butterfly] -
-
- Forthcoming ... -
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html deleted file mode 100644 index b86e965c0..000000000 --- a/helm/www/lambdadelta/specification.html +++ /dev/null @@ -1,383 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - - Open Symbolic Notation (OSN) -
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Computer-checked formal specifications [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, - then the calculus is announced with a presentation. - Beta: - major changes and additions may occur before the calculus is released on paper. - Gamma: - subsequent improvements occur until the specification is completed or superseded, - while major changes and additions are announced and reported on paper. - Delta: - after its conclusion, the specification is modified just for maintenance. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
versionnamestagedeveloped withstartedannouncedreleasedconcludedreferences
- Version 3 - "basic_3" - - - - - - - J3a -
- Version 2 - "basic_2""A2" - Matita 0.99.3 - October 2015 - - - -
-
- 		-
- 		"A1" - Matita 0.99.2 - April 2011June 2014October 2014August 2015 - V2a - R2c -
Abandoned - - - Coq 7.3.1 - March 2008 - - February 2011 -
- Version 1 - "basic_1" - - Coq 7.3.1 - May 2004December 2005November 2006May 2008 - V1a - J1a -
-
-
- Informational pages on the specifications are provided. -
- - - -
- [butterfly] λδ version 3 (proposed)
-
- The formal specification of λδ version 3 - is forthcoming. -
- -
- [butterfly] λδ version 2 (active)
-
- The formal specification of λδ version 2 - is available in the following formats: -
- -
- Informational pages on the parts of the specification: - Background, - Core, - Applications. -
- -
- [butterfly] λδ version 1 (superseded)
-
- The formal specification of λδ version 1 - is available in the following formats: -
- - - -
- Informational pages on the parts of the specification: - Background, - Core. -
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Fri, 24 Nov 2017 21:00:00 +0100
- - diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index 76725fda4..d8f43a7c9 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -15,7 +15,7 @@ lambdadelta.bib, lambdadelta.txt - (revised ). + (revised ). λδ version 3 (proposed) diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl index befe967a1..2fe3ea0e6 100644 --- a/helm/www/lambdadelta/web/home/documentation_1.tbl +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -13,7 +13,7 @@ table { @("http://arxiv.org/abs/cs/0611040" "cs/0611040") + "[v10] (revised" + "2008-09)." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldR1c" "R1c." "" } { @@ -24,7 +24,7 @@ table { "In CiE 2007 Local Proceedings." + "University of Siena, technical report 487, p. 387" + "(abstract of a presentation)." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldR1b" "R1b." "" } { @@ -33,7 +33,7 @@ table { "Lambda Types on the Lambda Calculus with Abbreviations") + "(2006-11)." + "University of Bologna, technical report UBLCS-2006-25." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldR1a" "R1a." "" } { @@ -42,7 +42,7 @@ table { "Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") + "(2006-01)." + "University of Bologna, technical report UBLCS-2006-01." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldP1e" "P1e." "" } { @@ -88,10 +88,10 @@ table { ] [ { name "ldV1a" "V1a." "" } { "F. Guidi:" + - @@("version_1.html" "lambdadelta_1") + + @@("html/version_1.html" "lambdadelta_1") + "(revised 2015-01)." + "Formal specification for the proof assistant Coq 7.3.1 (scripts)." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] } diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 7b450ff46..6dafba83f 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -12,7 +12,7 @@ table { @("http://arxiv.org/abs/1411.0154" "1411.0154") + "[v2] (revised" + "2015-03)." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] *) @@ -22,7 +22,7 @@ table { "Extending the Applicability Condition in the Formal System λδ") + "(2015-03)." + "University of Bologna, technical report AMS Acta 4411." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldR2b" "R2b." "" } { @@ -32,7 +32,7 @@ table { "(2010-07)." + "In CiE 2010 Local Proceedings." + "University of Azores, CMATI Booklet, pp. 204-213." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldR2a" "R2a." "" } { @@ -41,7 +41,7 @@ table { "Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") + "(2009-09)." + "University of Bologna, technical report UBLCS-2009-16." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] [ { name "ldP2d" "P2d." "" } { @@ -78,10 +78,10 @@ table { ] [ { name "ldV2a" "V2a." "" } { "F. Guidi:" + - @@("version_2.html" "lambdadelta_2A1") + + @@("html/version_2.html" "lambdadelta_2A1") + "(revised 2014-10)." + "Formal specification for the proof assistant Matita 0.99.2 (scripts)." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] } diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl index b4dd848a6..d5d17a570 100644 --- a/helm/www/lambdadelta/web/home/documentation_3.tbl +++ b/helm/www/lambdadelta/web/home/documentation_3.tbl @@ -7,7 +7,17 @@ table { "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." + - @@("documentation.html#bibtex" "BibTeX entry") ^ "." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldR3a" "R3a." "" } { + "F. Guidi:" + + @("http://amsacta.unibo.it/5754/" + "The Formal System λΥP") + + "(2017-12)." + + "University of Bologna, technical report AMS Acta 5754" + + "(accepted 2018-01)." + + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } ] } diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 9ddcbf34e..76bd89b33 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -64,7 +64,7 @@ (the specification language of Matita). The overall validation speed of the "Grundlagen der Analysis" increases of 34% with respect to version 0.8.1. - Documentation (J3a). + Documentation (J3a). [Svn revision: 13035] (archived source code). The specification of Landau's "Grundlagen der Analysis" @@ -116,7 +116,7 @@ Supports λδ version 2 with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. - Documentation (R2a). + Documentation (R2a). [Svn revision: 10304] (archived source code). A Jed mode diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 0bf225624..3f1c9f893 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -13,12 +13,12 @@ Milestones - Second journal paper on λδ + Second journal paper on λδ accepted for publication. - "Helena 0.8.3" is released. + "Helena 0.8.3" is released. @@ -36,7 +36,7 @@ - "Helena 0.8.2" is updated. + "Helena 0.8.2" is updated. The translated specification of Landau's "Grundlagen der Analysis" is validated in CC by Coq 8.4.3. @@ -44,12 +44,12 @@ - The specification of λδ version 1 + The specification of λδ version 1 is updated with backports from the abandoned specification of λδ version 2. - "Helena 0.8.2" is released. + "Helena 0.8.2" is released. The corrected specification of Landau's "Grundlagen der Analysis" is validated in λδ version 3. @@ -57,7 +57,7 @@ - λδ version 2A1 + λδ version 2A1 is released. @@ -66,7 +66,7 @@ - First communication on λδ version 2. + First communication on λδ version 2. @@ -96,7 +96,7 @@ - The specification of λδ version 2 + The specification of λδ version 2 and related topics is restarted in Matita 0.5. @@ -110,16 +110,16 @@ - "Helena 0.8.1" is released. + "Helena 0.8.1" is released. - "Helena 0.8.0" is released and the - λδ Digital Library is started. + "Helena 0.8.0" is released and the + λδ Digital Library is started. - "Helena", a validator for λδ version 2, + "Helena", a validator for λδ version 2, is available as a part of the HELM software. @@ -128,7 +128,7 @@ - First journal paper on λδ + First journal paper on λδ accepted for publication. @@ -139,7 +139,7 @@ - The + The HTML pages of the specification of λδ version 1 for Matita 0.5 are online. @@ -153,22 +153,22 @@ - The + The specification of λδ version 1 for Matita 0.4 is online. - λδ version 1 + λδ version 1 is released. - First communication on λδ version 1. + First communication on λδ version 1. - The specification of λδ version 1 + The specification of λδ version 1 is started with Coq 7.3.1. diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index dec0d13e6..14e8ac71a 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -2,39 +2,39 @@ name "sitemap" table [ class "sky" { - [ @@"home" * ] - [ @@("home#foreword" "foreword") * ] - [ @@("home#citations" "citations") * ] + [ @@("html/home" "home") * ] + [ @@("html/home#foreword" "foreword") * ] + [ @@("html/home#citations" "citations") * ] } class "magenta" { - [ @@"news" * ] - [ @@("news#milestones" "milestones") * ] - [ @@("news#visibility" "visibility") * ] + [ @@("html/news" "news") * ] + [ @@("html/news#milestones" "milestones") * ] + [ @@("html/news#visibility" "visibility") * ] } class "white" { - [ @@"specification" * ] - [ @@("specification#v2" "version 2") - "(" ^ @@("ground_2" "background") + "-" + - @@("basic_2" "core") + "-" + - @@("apps_2" "applications") ^ ")" + [ @@("html/specification" "specification") * ] + [ @@("html/specification#v2" "version 2") + "(" ^ @@("html/ground_2" "background") + "-" + + @@("html/basic_2" "core") + "-" + + @@("html/apps_2" "applications") ^ ")" * ] - [ @@("specification#v1" "version 1") - "(" ^ @@("ground_1" "background") + "-" + - @@("basic_1" "core") ^ ")" + [ @@("html/specification#v1" "version 1") + "(" ^ @@("html/ground_1" "background") + "-" + + @@("html/basic_1" "core") ^ ")" "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")" * ] } class "orange" { - [ @@"documentation" * ] - [ @@("documentation#v2" "version 2") * ] - [ @@("documentation#v1" "version 1") * ] + [ @@("html/documentation" "documentation") * ] + [ @@("html/documentation#v2" "version 2") * ] + [ @@("html/documentation#v1" "version 1") * ] } class "green" { - [ @@"implementation" * ] - [ @@("implementation#helena" "helena") + [ @@("html/implementation" "implementation") * ] + [ @@("html/implementation#helena" "helena") @@("osn/" "Open Symbolic Notation (OSN)") * ] - [ @@("implementation#lddl" "library") + [ @@("html/implementation#lddl" "library") "(" ^ @@("static/lddl/" "static LDDL directory") ^ ")" * ] } diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 10a24009f..93208df02 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -66,7 +66,7 @@ lambdadelta_2A1 for Matita 0.99.2 (revised ). Source scripts [Svn revision: 12964]. - Documentation (R2c). + Documentation (R2c). The scripts are grouped in directories, first by part, then by component. @@ -81,9 +81,9 @@ Informational pages on the parts of the specification: - Background, - Core, - Applications. + Background, + Core, + Applications. @@ -99,7 +99,7 @@ lambdadelta_1 for Coq 7.3.1 (revised ). Source scripts. - Documentation (J1a). + Documentation (J1a). 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg". @@ -146,8 +146,8 @@ Informational pages on the parts of the specification: - Background, - Core. + Background, + Core.