From 4e75ab41fb7a0a9a4f66cb777a791ce3950c57ce Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 11 Mar 2017 18:32:41 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/BTM.html | 226 +- helm/www/lambdadelta/apps_2.html | 279 +- helm/www/lambdadelta/basic_1.html | 830 ++- helm/www/lambdadelta/basic_2.html | 854 ++- helm/www/lambdadelta/core.html | 7120 +++++++++++++++++++++- helm/www/lambdadelta/documentation.html | 405 +- helm/www/lambdadelta/ground_1.html | 296 +- helm/www/lambdadelta/ground_2.html | 824 ++- helm/www/lambdadelta/home.html | 240 +- helm/www/lambdadelta/implementation.html | 245 +- helm/www/lambdadelta/news.html | 366 +- helm/www/lambdadelta/osn.html | 169 +- helm/www/lambdadelta/specification.html | 348 +- 13 files changed, 11996 insertions(+), 206 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index b6c0bdac6..e63f9accc 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -1,5 +1,227 @@ -BTM
[\lambda\delta home]
cic:/matita/BTM/
[Spacer]
Character classes
This table shows how the first 45 positive integers + + + + + + + + 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: Thu, 09 Mar 2017 13:38:17 +0100
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
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: Sat, 11 Mar 2017 19:30:41 +0100
+ + diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index e23bd8edd..e754a6e29 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,26 +1,283 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Contents of the Specification [butterfly]
This specification comprises a collection of checked + + + + + + + + \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 + + +
Summary of the Specification [butterfly] +
+
Here is a numerical account of the specification's contents and its timeline. -
categoryobjects




sizesfiles1characters377nodes775
propositionstheorems2lemmas1total3
conceptsdeclared0defined3total3
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+
+
+
+
+
+
+
+
+
sizesfiles1characters377nodes779
propositionstheorems2lemmas1total3
conceptsdeclared0defined3total3
+
+ + + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

relocationlift ( ↑[?,?] ? )
examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
+
+
relocationlift ( ↑[?,?] ? ) +
+
examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta +
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 8560a6fcf..d160de5dd 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -1,18 +1,828 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(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 + + + + + + + + \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
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+
+
+
+
+
+
+
+
+
sizesfiles120characters198089nodes1449099
propositionstheorems81lemmas618total699
conceptsdeclared39defined47total86
+
+ + + + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles
examplesterms with special featureslevels_ex0ty3_ex1nf2_ex2

dynamic typingwell-formed contextswf3_defswf3_props

context ref. for native type assignmentcsubt_defscsubt_propscsubt_arity_props

native type assignmentty3_defsty3_propsty3_genty3_gen_contextty3_gen_nf2ty3_liftty3_subst0ty3_arity_propsty3_nf2_genty3_sredty3_sred_propsty3_dec
equivalencecontext-sensitive equivalencepc3_defspc3_propspc3_genpc3_gen_contextpc3_subst0

context-free equivalencepc1_defspc1_props

computationcontext ref. for reducibilitycsubc_defscsubc_props

reducibilitysc3_defssc3_propssc3_arity

strongly normalizing computationsn3_defssn3_gensn3_props

context-sensitive computationpr3_defspr3_propspr3_genpr3_gen_contextpr3_isopr3_subst1pr3_confluence

context-free computationpr1_defspr1_propspr1_confluence
reductionnormal forms for context-sensitive reductionnf2_defsnf2_propsnf2_gennf2_dec

context-sensitive reductionpr2_defspr2_genpr2_gen_contextpr2_liftpr2_subst1pr2_confluence

normal forms for context-free reductionnf0_dec

context-free reductionwcpr0_defs


pr0_defspr0_genpr0_liftpr0_subst0pr0_subst1pr0_confluence
unfolditerated static type assignmentsty1_defssty1_props
static typingstatic type assignmentsty0_defssty0_props

context ref. for binary arity assignmentcsuba_defscsuba_props

binary arity assignmentarity_defsarity_propsarity_genarity_subst0arity_sred

binary aritylevels_defsllt_defsaprem_defs

parametersparameter_defs

basic context ref.csubv_defs
multiple substitutioniterated context slicingdrop1_defsdrop1_props

generic term relocationlift1_defslift1_props
substitutionordinary substitutionsubst_defssubst_props


csubst1_defscsubst1_props


subst1_defssubst1_gensubst1_liftsubst1_subst1subst1_confluence

normal forms for ordinary strict substitutiondnf_dec

ordinary strict substitutionfsubst0_defs


csubst0_defs


subst0_defssubst0_gensubst0_tltsubst0_liftsubst0_subst0subst0_confluence

basic local env. slicinggetl_defsgetl_props


drop_defsdrop_props

basic term relocationlift_defslift_propslift_genlift_tlt
grammarclosuresflt_defs

contextscontexts_defsclt_defsctail_defsapp_defscnt_defs

termstlist_defs


terms_defstlt_defsiso_defs
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
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: Sat, 11 Mar 2017 19:30:41 +0100
+ + diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 765da9830..c694c00df 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,6 +1,108 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents +--> +
Summary of the Specification [butterfly] +
+
Here is a numerical account of the specification's contents and its timeline. -
categoryobjects




sizesfiles213characters224056nodes1100545
propositionstheorems61lemmas743total804
conceptsdeclared29defined66total95
Stage "B"
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+
+
+
+
+
+
+
+
+
sizesfiles213characters224345nodes1097549
propositionstheorems61lemmas743total804
conceptsdeclared29defined65total94
+
+
Stage "B"
+
Stage "A2": "Extending the Applicability Condition"
+
Stage "A2": "Extending the Applicability Condition"
+ + + + + +
Stage "A1": "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. -
componentplanefiles
rt-computationuncounted context-sensitive rt-transitioncsx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )


csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_cnx csx_cpxs csx_csx


lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_fqup


cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transitionparallel qrst-transitionfpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )

t-bound context-sensitive rt-transitionlfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr


cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )cpr_drops


cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx

uncounted context-sensitive rt-transitioncnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops


lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx


cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs

counted context-sensitive rt-transitioncpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr
iterated static typingiterated extension on referred entriestc_lfxs ( ? ⦻**[?,?] ? )
static typinggeneric reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drops lsubc_lsubr lsubc_lsuba


gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa


gcp

atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba


aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfdeq aaa_aaa

degree-based equivalence on referred entriesffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )ffdeq_fqup ffdeq_ffdeq


lfdeq ( ? ≡[?,?,?] ? )lfdeq_length lfdeq_fqup lfdeq_lfdeq

generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs

context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_frees


frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_drops frees_fqup frees_frees

restricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
s-computationiterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_weight fqus_drops fqus_fqup fqus_fqus


fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_weight fqup_drops fqup_fqup
s-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight


fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )


drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops

generic relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector


lifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_tdeq lifts_lifts

ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq

generic entrywise extensionlexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs
syntaxappend for local environmentsappend ( ? @@ ? )append_length

degree-based equivalence for termsdeq ( ? ≡[?,?] ? ) deq_deq

same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector

closurescl_weight ( ♯{?,?,?} )


cl_restricted_weight ( ♯{?,?} )

global environmentsgenv

local environmentslenv_length ( |?| )


lenv_weight ( ♯{?} )


lenv

termsterm_vector ( Ⓐ?.? )


term_simple ( 𝐒⦃?⦄ )


term_weight ( ♯{?} )


term

itemsitem_sd


item_sh


item

atomic aritiesaarity
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
rt-computationuncounted context-sensitive rt-transitioncsx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) +
+
+
+
+
+
csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )csx_cnx csx_cpxs csx_csx
+
+
+
+
lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )lfpxs_length lfpxs_fqup lfpxs_cpxs
+
+
+
+
cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )cpxs_tdeq cpxs_drops cpxs_lfpx cpxs_cpxs
rt-transitionparallel qrst-transitionfpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) +
+
+
+
t-bound context-sensitive rt-transitionlfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
+
+
+
+
cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )cpr_drops
+
+
+
+
cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
+
+
uncounted context-sensitive rt-transitioncnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )cnx_simple cnx_drops
+
+
+
+
lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx
+
+
+
+
cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
+
+
counted context-sensitive rt-transitioncpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )cpg_simple cpg_drops cpg_lsubr
iterated static typingiterated extension on referred entriestc_lfxs ( ? ⦻**[?,?] ? ) +
+
static typinggeneric reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drops lsubc_lsubr lsubc_lsuba
+
+
+
+
gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
+
+
+
+
gcp +
+
+
+
atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
+
+
+
+
aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
+
+
degree-based equivalence on referred entriesffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )ffdeq_fqup ffdeq_ffdeq
+
+
+
+
lfdeq ( ? ≡[?,?,?] ? )lfdeq_length lfdeq_fqup lfdeq_lfdeq
+
+
generic extension on referred entrieslfxs ( ? ⦻*[?,?] ? )lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
+
+
context-sensitive free variableslsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )lsubf_frees
+
+
+
+
frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_drops frees_fqup frees_frees
+
+
restricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
s-computationiterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_weight fqus_drops fqus_fqup fqus_fqus
+
+
+
+
fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_weight fqup_drops fqup_fqup
s-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight
+
+
+
+
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) +
+
+
+
+
+
drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
+
+
generic relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector
+
+
+
+
lifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_tdeq lifts_lifts
+
+
ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq
+
+
generic entrywise extensionlexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs
syntaxappend for local environmentsappend ( ? @@ ? )append_length
+
+
degree-based equivalence for termsdeq ( ? ≡[?,?] ? ) deq_deq
+
+
same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector
+
+
closurescl_weight ( ♯{?,?,?} ) +
+
+
+
+
+
cl_restricted_weight ( ♯{?,?} ) +
+
+
+
global environmentsgenv +
+
+
+
local environmentslenv_length ( |?| ) +
+
+
+
+
+
lenv_weight ( ♯{?} ) +
+
+
+
+
+
lenv +
+
+
+
termsterm_vector ( Ⓐ?.? ) +
+
+
+
+
+
term_simple ( 𝐒⦃?⦄ ) +
+
+
+
+
+
term_weight ( ♯{?} ) +
+
+
+
+
+
term +
+
+
+
itemsitem_sd +
+
+
+
+
+
item_sh +
+
+
+
+
+
item +
+
+
+
atomic aritiesaarity +
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:41 +0100
+ + diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index a82d853eb..170d355dd 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -1,3 +1,7121 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(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: Thu, 09 Mar 2017 13:38:17 +0100
+ + + + + + + + \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: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 346916416..9a7d91b3a 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,15 +1,406 @@ -\lambda\delta home page
[\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Documentation [butterfly]
+ + + + + + + + \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: - downloadlambdadelta.bib, - viewlambdadelta.txt + download + lambdadelta.bib, + view + lambdadelta.txt (revised 2015-09). -
[butterfly] λδ version 3 (proposed)
+
+
+ [butterfly] λδ version 3 (proposed)
+
The main source of information is J3a. -
[butterfly] λδ version 2 (active)
+
+
+ + + + + + + + + + +
+ J3a. + F. Guidi: Verified Representations of Landau's "Grundlagen" in the λδ Family and in the Calculus of Constructions (2015-12). In JFR 8(1), Univerity of Bologna, pp. 93-116. BibTeX entry.
+ +
+
+
+
+ [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)
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ 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 (accepted2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.

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

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

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

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

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

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

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

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

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

[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:16 +0100
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ J1a. + F. Guidi: The Formal System λδ (2009-11). In ACM ToCL 11(1), pp. 5:1-5:37 online app. pp. 1-11 (accepted + 2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
+ +
+
+ R1c. + F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). BibTeX entry.
+ +
+
+ R1b. + F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.
+ +
+
+ R1a. + F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification (2006-01). University of Bologna, technical report UBLCS-2006-01. BibTeX entry.
+ +
+
+ P1e. + F. Guidi: The Formal System λδ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).
+ +
+
+ P1d. + F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).
+ +
+
+ P1c. + F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).
+ +
+
+ P1b. + F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).
+ +
+
+ P1a. + F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).
+ +
+
+ V1a. + F. Guidi: lambdadelta_1 (revised 2015-01). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry.
+ +
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 61e02fdb8..768502a4d 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -1,12 +1,296 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)
+
+ [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
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+
+
+
+
+
+
+
+
+
sizesfiles10characters15063nodes14881
propositionstheorems0lemmas50total50
conceptsdeclared24defined4total28
+
+ + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles


multiple relocationbg_plist


extensions to the librarybg_hintsbg_blt

generated logical decomposablesbg_typesbg_props

preamblebg_requirebg_rewritebg_tacticsbg_subst
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
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: Sat, 11 Mar 2017 19:30:41 +0100
+ + diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index d0349b2ad..36c3513b0 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -1,18 +1,824 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
+
+ [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




sizesfiles93characters135543nodes314125
propositionstheorems38lemmas647total685
conceptsdeclared63defined67total130
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+
+
+
+
+
+
+
+
+
sizesfiles95characters135595nodes314345
propositionstheorems38lemmas647total685
conceptsdeclared63defined67total130
+
+ + + + + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles
















generic rt-transition counterrtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )rtc_shift ( ↓? )rtc_max ( ? ∨ ? )rtc_plus ( ? + ? )












multiple relocationrtmaprtmap_eq ( ? ≗ ? )rtmap_pushs ( ↑*[?]? )rtmap_tl ( ⫱? )rtmap_tls ( ⫱*[?]? )rtmap_isid ( 𝐈⦃?⦄ )rtmap_idrtmap_fcla ( 𝐂⦃?⦄ ≡ ? )rtmap_isfin ( 𝐅⦃?⦄ )rtmap_isuni ( 𝐔⦃?⦄ )rtmap_uni ( 𝐔❴?❵ )rtmap_sle ( ? ⊆ ? )rtmap_sand ( ? ⋒ ? ≡ ? )rtmap_sor ( ? ⋓ ? ≡ ? )rtmap_at ( @⦃?,?⦄ ≡ ? )rtmap_istot ( 𝐓⦃?⦄ )rtmap_after ( ? ⊚ ? ≡ ? )rtmap_coafter ( ? ~⊚ ? ≡ ? )


nstream ( ↑? ) ( ⫯? )nstream_eqnstream_isidnstream_id ( 𝐈𝐝 )nstream_sandnstream_istot ( ?@❴?❵ )nstream_after ( ? ∘ ? )nstream_coafter ( ? ~∘ ? )


mr2mr2_at ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )













natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_plus ( ? + ? )











extensions to the librarystream ( ? @ ? )stream_eq ( ? ≐ ? )stream_hdtl ( ↓? )stream_tls ( ↓*[?]? )















list ( ◊ ) ( ? @ ? ) ( |?| )list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

















bool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )

















starlstar















generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )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: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
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_tl ( ⫱? )rtmap_tls ( ⫱*[?]? )rtmap_isid ( 𝐈⦃?⦄ )rtmap_idrtmap_fcla ( 𝐂⦃?⦄ ≡ ? )rtmap_isfin ( 𝐅⦃?⦄ )rtmap_isuni ( 𝐔⦃?⦄ )rtmap_uni ( 𝐔❴?❵ )rtmap_sle ( ? ⊆ ? )rtmap_sand ( ? ⋒ ? ≡ ? )rtmap_sor ( ? ⋓ ? ≡ ? )rtmap_at ( @⦃?,?⦄ ≡ ? )rtmap_istot ( 𝐓⦃?⦄ )rtmap_after ( ? ⊚ ? ≡ ? )rtmap_coafter ( ? ~⊚ ? ≡ ? )
+
+
+
+
nstream ( ↑? ) ( ⫯? )nstream_eq + + + nstream_isidnstream_id ( 𝐈𝐝 ) + + + + + nstream_sand + + 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 ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index c58614f4c..b4c9a726d 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -1,99 +1,295 @@ -\lambda\delta home page
[\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Foreword [butterfly]
+ + + + + + + + \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. +
+
+ 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]
+
+ +
Citations [butterfly] +
+
This is a list of publications citing λδ documentation. -
+ + + + + + + +
Disclaimer [butterfly]
+ + + +
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] + + +
+ [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: Thu, 09 Mar 2017 13:38:16 +0100
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index b5e25b9d9..e6cb4c1f7 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,22 +1,137 @@ -\lambda\delta home page
[\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Tools [butterfly]
[Open Symbolic Notation logo] Open Symbolic Notation
+ + + + + + + + \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 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: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index d4d07a06a..a92c560b7 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -1,97 +1,385 @@ -\lambda\delta home page
[\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Milestones [butterfly]
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:40 +0100
+ + diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index 26b1014dc..45166f8ad 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -1,12 +1,39 @@ -\lambda\delta home page: Open Symbolic Notation
[Open Symbolic Notation logo]
Open Symbolic Notation
[Spacer]
+ + + + + + + + \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]
+ + + +
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. -
+ + + + + + +
+
+ gap = space | ',' | ';' | '=' ; + + +
The grammar of OSN is very liberal by design. Spaces of the form 1 * gap can appear between any pair of tokens. -
+ + +
Semantics [butterfly]
+
+ expr = symbol | string | string-alt | ( open , text , close ) ; + + +
Semantics [butterfly] +
+
Forthcoming ... -
Implementation [butterfly]
+--> +
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: Thu, 09 Mar 2017 13:38:16 +0100
+
+
+ [Spacer] +
+
+
+
+ +
+
+
+
Last update: Sat, 11 Mar 2017 19:30:39 +0100
+ + diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 380924ebd..c627c3cb1 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -1,9 +1,114 @@ -\lambda\delta home page
[\lambda\delta home]
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]

Computer-checked formal specifications [butterfly]
+ + + + + + + + \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, @@ -15,71 +120,264 @@ while major changes and additions are announced and reported on paper. Delta: after its conclusion, the specification is modified just for maintenance. -
versionnamestagedeveloped withstartedannouncedreleasedconcludedreferences
Version 3"basic_3"J3a
Version 2"basic_2""A2"Matita 0.99.3October 2015


"A1"Matita 0.99.2April 2011June 2014October 2014August 2015V2aR2c
AbandonedCoq 7.3.1March 2008February 2011
Version 1"basic_1"Coq 7.3.1May 2004December 2005November 2006May 2008V1aJ1a
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
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. -
  • Notice on displayed numerical acounts: +
+ +
[butterfly] λδ version 3 (proposed)
+ + + +
+ [butterfly] λδ version 3 (proposed)
+
The formal specification of λδ version 3 is forthcoming. -
[butterfly] λδ version 2 (active)
+
+ +
+ [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)
+
+ +
+ [butterfly] λδ version 1 (superseded)
+
The formal specification of λδ version 1 is available in the following formats: -
+
The scripts are grouped in directories, one for each part. -
+ + + +
+ Notice: the HELM rendering engine is offline. + + +
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: Thu, 09 Mar 2017 13:38:16 +0100
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:40 +0100
+ + -- 2.39.2