From 076439def28e649ec384fae038ed021dadd5f75c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 18 Jan 2020 23:20:28 +0100 Subject: [PATCH] update in lambdadelta MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + probe: name listing with clash analysis + lambdadelta: name clashes removed from λδ-2A and λδ-2B --- matita/components/binaries/probe/engine.ml | 16 +- matita/components/binaries/probe/engine.mli | 16 +- .../components/binaries/probe/matitaList.ml | 16 +- .../components/binaries/probe/matitaList.mli | 16 +- .../components/binaries/probe/matitaRemove.ml | 16 +- .../binaries/probe/matitaRemove.mli | 16 +- matita/components/binaries/probe/nCicScan.ml | 40 +- matita/components/binaries/probe/nCicScan.mli | 16 +- matita/components/binaries/probe/options.ml | 24 +- matita/components/binaries/probe/options.mli | 20 +- matita/components/binaries/probe/probe.ml | 24 +- matita/matita/contribs/lambdadelta/Makefile | 20 +- .../contribs/lambdadelta/basic_1A/names.txt | 931 ++++++++ .../contribs/lambdadelta/basic_2/names.txt | 1312 ++++++++++- .../basic_2/rt_computation/lprs_cpms.ma | 2 +- .../basic_2/rt_computation/lpxs_cpxs.ma | 20 +- .../basic_2/rt_equivalence/cpcs_lprs.ma | 12 +- .../basic_2/rt_transition/cpg_drops.ma | 2 +- .../lambdadelta/basic_2A/grammar/aarity.ma | 2 +- .../contribs/lambdadelta/basic_2A/names.txt | 1919 +++++++++++++++++ .../lambdadelta/basic_2A/static/lsuba.ma | 2 +- matita/matita/contribs/lambdadelta/names.txt | 105 + .../contribs/lambdadelta/static_2/names.txt | 1276 +++++++++++ .../static_2/relocation/drops_drops.ma | 14 +- .../lambdadelta/static_2/static/feqx_req.ma | 2 +- .../lambdadelta/static_2/static/fsle_fqup.ma | 2 +- .../lambdadelta/static_2/static/lsuba.ma | 2 +- .../lambdadelta/static_2/syntax/lveq.ma | 2 +- 28 files changed, 5607 insertions(+), 238 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_1A/names.txt create mode 100644 matita/matita/contribs/lambdadelta/basic_2A/names.txt create mode 100644 matita/matita/contribs/lambdadelta/names.txt create mode 100644 matita/matita/contribs/lambdadelta/static_2/names.txt diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index 0fe7ace53..bd452674e 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module F = Filename diff --git a/matita/components/binaries/probe/engine.mli b/matita/components/binaries/probe/engine.mli index df8a69ff3..5aed03961 100644 --- a/matita/components/binaries/probe/engine.mli +++ b/matita/components/binaries/probe/engine.mli @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) val out_int: int -> unit diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index d6426e361..d4ea3e584 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module A = Array diff --git a/matita/components/binaries/probe/matitaList.mli b/matita/components/binaries/probe/matitaList.mli index 200c90158..220d4e82f 100644 --- a/matita/components/binaries/probe/matitaList.mli +++ b/matita/components/binaries/probe/matitaList.mli @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) val from_uri: string -> string -> NUri.uri -> unit diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml index 72624f0f0..b34cfc357 100644 --- a/matita/components/binaries/probe/matitaRemove.ml +++ b/matita/components/binaries/probe/matitaRemove.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module A = Array diff --git a/matita/components/binaries/probe/matitaRemove.mli b/matita/components/binaries/probe/matitaRemove.mli index 7e45d9082..eb711bdc9 100644 --- a/matita/components/binaries/probe/matitaRemove.mli +++ b/matita/components/binaries/probe/matitaRemove.mli @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) val objects: unit -> unit diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index f1c2772ec..5b0a10605 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module L = List @@ -32,6 +32,11 @@ let status = new P.status let malformed () = failwith "probe: malformed term" +let add_name str = + let u = U.uri_of_string str in + if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str; + O.names := US.add u !O.names + let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour) let add_ind n = O.add_xflavour n `Inductive @@ -41,12 +46,15 @@ let rec set_list c ts cts = L.fold_left map cts ts let set_funs c rfs cts = - let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in + let map cts (_, s, _, t0, t1) = + add_name s; + set_list c [t0; t1] cts + in L.fold_left map cts rfs -let set_type c cts (_, _, t, css) = - let map cts (_, _, t) = (c, t) :: cts in - (c, t) :: L.fold_left map cts css +let set_type c cts (_, s, t, css) = + let map cts (_, s, t) = add_name s; (c, t) :: cts in + add_name s; (c, t) :: L.fold_left map cts css let inc st = {st with c = succ st.c} @@ -93,11 +101,11 @@ let scan_obj u c = let st = {c; u} in let _, _, _, _, obj = E.get_checked_obj status u in let st = match obj with - | C.Constant (_, _, None, t, m) -> - add_attr 1 m; + | C.Constant (_, s, None, t, m) -> + add_name s; add_attr 1 m; scan_term (inc st) [[], t] - | C.Constant (_, _, Some t0, t1, m) -> - add_attr 1 m; + | C.Constant (_, s, Some t0, t1, m) -> + add_name s; add_attr 1 m; scan_term (inc st) (set_list [] [t0; t1] []) | C.Fixpoint (_, rfs, m) -> add_attr (L.length rfs) m; diff --git a/matita/components/binaries/probe/nCicScan.mli b/matita/components/binaries/probe/nCicScan.mli index be5404956..24e5a5690 100644 --- a/matita/components/binaries/probe/nCicScan.mli +++ b/matita/components/binaries/probe/nCicScan.mli @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) val scan: unit -> unit diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index ce29c1ef0..0b9487d6b 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module A = Array @@ -44,6 +44,8 @@ let default_objs = US.empty let default_srcs = US.empty +let default_names = US.empty + let default_remove = [] let default_exclude = [] @@ -66,6 +68,8 @@ let objs = ref default_objs let srcs = ref default_srcs +let names = ref default_names + let remove = ref default_remove let exclude = ref default_exclude @@ -113,8 +117,8 @@ let out_deps file = let clear () = R.clear (); A.iteri clear_slot slot; - objs := default_objs; srcs := default_srcs; remove := default_remove; - exclude := default_exclude; net := default_net; + objs := default_objs; srcs := default_srcs; names := default_names; + remove := default_remove; exclude := default_exclude; net := default_net; chars := default_chars; debug_lexer := default_debug_lexer; no_devel := default_no_devel; no_init := default_no_init; deps := UPS.empty diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index c36695ef5..4eef17807 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -1,19 +1,19 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) type def_xflavour = [ NCic.def_flavour | `Inductive ] -val add_xflavour: int -> def_xflavour -> unit +val add_xflavour: int -> def_xflavour -> unit val iter_xflavours: (int -> unit) -> unit @@ -21,6 +21,8 @@ val objs: NUri.UriSet.t ref val srcs: NUri.UriSet.t ref +val names: NUri.UriSet.t ref + val remove: string list ref val exclude: NCic.source list ref diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index 94c8707a7..d118fdab2 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module A = Arg @@ -52,6 +52,10 @@ let set_p () = O.exclude := `Provided :: !O.exclude let out_f () = O.iter_xflavours E.out_int +let out_nn () = E.out_length !O.names + +let out_ns () = E.out_uris !O.names + let out_oc () = E.out_int !O.net let out_on () = E.out_length !O.objs @@ -82,6 +86,8 @@ let _ = let help_f = " Print the number of objects grouped by flavour" in let help_g = " Exclude generated objects" in let help_i = " Exclude implied objects" in + let help_nn = " Print the number of names" in + let help_ns = " Print the list of names" in let help_oc = " Print the total intrinsic complexity (objects)" in let help_on = " Print the number of objects" in let help_os = " Print the list of objects" in @@ -96,6 +102,8 @@ let _ = "-f" , A.Unit out_f , help_f; "-g" , A.Unit set_g , help_g; "-i" , A.Unit set_i , help_i; + "-nn", A.Unit out_nn, help_nn; + "-ns", A.Unit out_ns, help_ns; "-oc", A.Unit out_oc, help_oc; "-on", A.Unit out_on, help_on; "-os", A.Unit out_os, help_os; diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 34dd97cd5..d08583562 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -17,14 +17,14 @@ PRB_DIR := ../../../components/binaries/probe PRB := probe.native PRB_OPTS := $(XOA_OPTS) -g -i -ORIG := . ./orig.sh +ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig CONTRIB := lambdadelta_2B WWW := ../../../../helm/www/lambdadelta -TAGS := all xoa orig elim deps top leaf stats tbls odeps trim contrib clean \ +TAGS := all names xoa orig elim deps top leaf stats tbls odeps trim contrib clean \ home up-home PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1 @@ -63,6 +63,16 @@ endef $(foreach PKG, $(XPACKAGES), $(eval $(call XMAS_TEMPLATE,$(PKG)))) +# names ###################################################################### + +NAMES = basic_1A basic_2A static_2 basic_2 + +%/names.txt: %/*/*.ma + @echo "PROBE $* -ns" + $(H)$(PRB_DIR)/$(PRB) $(PRB_OPTS) $* -ns | sort > $@ + +names: $(NAMES:%=%/names.txt) + # xoa ######################################################################## xoa: $(XOA_CONF) @@ -88,7 +98,7 @@ $(DEP_INPUT): LINE = $(MAS:%=%:include \"\".) $(DEP_INPUT): $(MAS) Makefile @echo " GREP include" $(H)grep "include \"" $(MAS) > $(DEP_INPUT) - $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT) + $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT) # dep ######################################################################## @@ -126,7 +136,7 @@ define STATS_TEMPLATE $$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): D1 = $$(word 5, $$(C0)) $$(STT_$(1)): D2 = $$(word 7, $$(C0)) - $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): M1 = $$(word 6, $$(C0)) $$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) @@ -136,7 +146,7 @@ $$(STT_$(1)): $$(MAS_$(1)) $(1)/probe.txt @printf '%-15s %-46s' 'Statistics for:' $(1) @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' - @printf '%-12s' '' + @printf '%-12s' '' @printf ' %-8s %6i' Chars $$(C2) @printf ' %-7s %7i' Nodes $$(C3) @printf ' %-11s' '' diff --git a/matita/matita/contribs/lambdadelta/basic_1A/names.txt b/matita/matita/contribs/lambdadelta/basic_1A/names.txt new file mode 100644 index 000000000..d85e05945 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_1A/names.txt @@ -0,0 +1,931 @@ +A +Abbr +Abst +abst_dec +AHead +ahead_inj_snd +aplus +aplus_ahead_simpl +aplus_asort_le_simpl +aplus_asort_O_simpl +aplus_asort_simpl +aplus_assoc +aplus_asucc +aplus_asucc_false +aplus_gz_ge +aplus_gz_le +aplus_inj +aplus_reg_r +aplus_sort_O_S_simpl +aplus_sort_S_S_simpl +app1 +Appl +aprem +aprem_asucc +aprem_gen_head_O +aprem_gen_head_S +aprem_gen_sort +aprem_repl +aprem_succ +aprem_zero +arity +arity_abbr +arity_abst +arity_appl +arity_appls_abbr +arity_appls_appl +arity_appls_bind +arity_appls_cast +arity_aprem +arity_bind +arity_cast +arity_cimp_conf +arity_fsubst0 +arity_gen_abst +arity_gen_appl +arity_gen_appls +arity_gen_bind +arity_gen_cast +arity_gen_cvoid +arity_gen_cvoid_subst0 +arity_gen_lift +arity_gen_lref +arity_gen_sort +arity_head +arity_lift +arity_lift1 +arity_mono +arity_nf2_inv_all +arity_repellent +arity_repl +arity_sort +arity_sred_pr2 +arity_sred_pr3 +arity_sred_wcpr0_pr0 +arity_sred_wcpr0_pr1 +arity_subst0 +ASort +asucc +asucc_gen_head +asucc_gen_sort +asucc_inj +asucc_repl +B +Bind +bind_dec_not +binder_dec +C +Cast +cbk +CHead +chead_ctail +cimp +cimp_bind +cimp_flat_dx +cimp_flat_sx +cimp_getl_conf +cle +clear +clear_bind +clear_cle +clear_clear +clear_ctail +clear_flat +clear_gen_all +clear_gen_bind +clear_gen_flat +clear_gen_flat_r +clear_gen_sort +clear_getl_trans +clear_mono +clear_pc3_trans +clear_pr2_trans +clear_pr3_trans +clear_trans +clear_wf3_trans +cle_flt_trans +cle_head +clen +cle_r +cle_trans_head +clt +clt_cong +clt_head +clt_thead +clt_wf_ind +clt_wf__q_ind +cnt +cnt_head +cnt_lift +cnt_sort +CSort +csuba +csuba_abst +csuba_arity +csuba_arity_rev +csuba_clear_conf +csuba_clear_trans +csuba_drop_abbr +csuba_drop_abbr_rev +csuba_drop_abst +csuba_drop_abst_rev +csuba_gen_abbr +csuba_gen_abbr_rev +csuba_gen_abst +csuba_gen_abst_rev +csuba_gen_bind +csuba_gen_bind_rev +csuba_gen_flat +csuba_gen_flat_rev +csuba_gen_void +csuba_gen_void_rev +csuba_getl_abbr +csuba_getl_abbr_rev +csuba_getl_abst +csuba_getl_abst_rev +csuba_head +csuba_refl +csuba_sort +csuba_void +csubc +csubc_abst +csubc_arity_conf +csubc_arity_trans +csubc_clear_conf +csubc_csuba +csubc_drop1_conf_rev +csubc_drop_conf_O +csubc_drop_conf_rev +csubc_gen_head_l +csubc_gen_head_r +csubc_gen_sort_l +csubc_gen_sort_r +csubc_getl_conf +csubc_head +csubc_refl +csubc_sort +csubc_void +csubst0 +csubst0_both +csubst0_both_bind +csubst0_clear_O +csubst0_clear_O_back +csubst0_clear_S +csubst0_clear_trans +csubst0_drop_eq +csubst0_drop_eq_back +csubst0_drop_gt +csubst0_drop_gt_back +csubst0_drop_lt +csubst0_drop_lt_back +csubst0_fst +csubst0_fst_bind +csubst0_gen_head +csubst0_gen_S_bind_2 +csubst0_gen_sort +csubst0_getl_ge +csubst0_getl_ge_back +csubst0_getl_lt +csubst0_getl_lt_back +csubst0_snd +csubst0_snd_bind +csubst1 +csubst1_bind +csubst1_flat +csubst1_gen_head +csubst1_getl_ge +csubst1_getl_ge_back +csubst1_getl_lt +csubst1_head +csubst1_refl +csubst1_sing +csubt +csubt_abst +csubt_clear_conf +csubt_csuba +csubt_drop_abbr +csubt_drop_abst +csubt_drop_flat +csubt_gen_abbr +csubt_gen_abst +csubt_gen_bind +csubt_gen_flat +csubt_getl_abbr +csubt_getl_abst +csubt_head +csubt_pc3 +csubt_pr2 +csubt_refl +csubt_sort +csubt_ty3 +csubt_ty3_ld +csubt_void +csubv +csubv_bind +csubv_bind_same +csubv_clear_conf +csubv_clear_conf_void +csubv_drop_conf +csubv_flat +csubv_getl_conf +csubv_getl_conf_void +csubv_refl +csubv_sort +csubv_void +CTail +c_tail_ind +cweight +dnf_dec +dnf_dec2 +drop +drop1 +drop1_cons +drop1_cons_tail +drop1_csubc_trans +drop1_gen_pcons +drop1_gen_pnil +drop1_getl_trans +drop1_nil +drop1_skip_bind +drop1_trans +drop_clear +drop_clear_O +drop_clear_S +drop_conf_ge +drop_conf_lt +drop_conf_rev +drop_csubc_trans +drop_ctail +drop_drop +drop_gen_drop +drop_gen_refl +drop_gen_skip_l +drop_gen_skip_r +drop_gen_sort +drop_getl_trans_ge +drop_getl_trans_le +drop_getl_trans_lt +drop_mono +drop_refl +drop_S +drop_skip +drop_skip_bind +drop_skip_flat +drop_trans_ge +drop_trans_le +ex1_arity +ex1_c +ex1__leq_sort_SS +ex1_t +ex1_ty3 +ex2_arity +ex2_c +ex2_nf2 +ex2_t +F +Flat +flt +flt_arith0 +flt_arith1 +flt_arith2 +flt_shift +flt_thead_dx +flt_thead_sx +flt_trans +flt_wf_ind +flt_wf__q_ind +fsubst0 +fsubst0_both +fsubst0_fst +fsubst0_gen_base +fsubst0_snd +fweight +G +getl +getl_clear_bind +getl_clear_conf +getl_clear_trans +getl_conf_ge_drop +getl_conf_le +getl_csubst1 +getl_ctail +getl_ctail_clen +getl_dec +getl_drop +getl_drop_conf_ge +getl_drop_conf_lt +getl_drop_conf_rev +getl_drop_trans +getl_flat +getl_flt +getl_gen_2 +getl_gen_all +getl_gen_bind +getl_gen_flat +getl_gen_O +getl_gen_S +getl_gen_sort +getl_gen_tail +getl_head +getl_intro +getl_mono +getl_refl +getl_trans +getl_wf3_trans +gz +iso +iso_flats_flat_bind_false +iso_flats_lref_bind_false +iso_gen_head +iso_gen_lref +iso_gen_sort +iso_head +iso_lref +iso_refl +iso_sort +iso_trans +K +leq +leq_ahead_asucc_false +leq_ahead_false_1 +leq_ahead_false_2 +leq_asucc +leq_asucc_false +leq_eq +leq_gen_head1 +leq_gen_head2 +leq_gen_sort1 +leq_gen_sort2 +leq_head +leq_leqz +leq_refl +leq_sort +leq_sym +leq_trans +leqz +leqz_head +leqz_leq +leqz_sort +lift +lift1 +lift1_bind +lift1_cons_tail +lift1_flat +lift1_free +lift1_lift1 +lift1_lref +lift1_sort +lift1_xhg +lift_bind +lift_d +lift_flat +lift_free +lift_free_sym +lift_gen_bind +lift_gen_flat +lift_gen_head +lift_gen_lift +lift_gen_lref +lift_gen_lref_false +lift_gen_lref_ge +lift_gen_lref_lt +lift_gen_sort +lift_head +lift_inj +lift_lref_ge +lift_lref_gt +lift_lref_lt +lift_r +lifts +lifts1 +lifts1_cons +lifts1_flat +lifts1_nil +lifts1_xhg +lifts_inj +lift_sort +lifts_tapp +lift_tle +lift_tlt_dx +lift_weight +lift_weight_add +lift_weight_add_O +lift_weight_map +llt +llt_head_dx +llt_head_sx +llt_repl +llt_trans +llt_wf_ind +llt_wf__q_ind +lref_map +lweight +lweight_repl +minus_s_s +mk_G +next_plus +next_plus_assoc +next_plus_gz +next_plus_lt +next_plus_next +nf0_dec +nf2 +nf2_abst +nf2_abst_shift +nf2_appl_lref +nf2_appls_lref +nf2_csort_lref +nf2_dec +nf2_gen_abbr +nf2_gen_abst +nf2_gen_beta +nf2_gen_cast +nf2_gen_flat +nf2_gen_lref +nf2_gen__nf2_gen_aux +nf2_gen_void +nf2_iso_appls_lref +nf2_lift +nf2_lift1 +nf2_lref_abst +nf2_pr3_confluence +nf2_pr3_unfold +nf2_sn3 +nf2_sort +nfs2 +nfs2_tapp +node_inh +not_abbr_abst +not_abbr_void +not_abst_void +not_void_abst +pc1 +pc1_head +pc1_head_1 +pc1_head_2 +pc1_pr0_r +pc1_pr0_u +pc1_pr0_u2 +pc1_pr0_x +pc1_refl +pc1_s +pc1_t +pc3 +pc3_abst_dec +pc3_dec +pc3_eta +pc3_fsubst0 +pc3_gen_abst +pc3_gen_abst_shift +pc3_gen_appls_lref_abst +pc3_gen_appls_lref_sort +pc3_gen_appls_sort_abst +pc3_gen_cabbr +pc3_gen_lift +pc3_gen_lift_abst +pc3_gen_not_abst +pc3_gen_sort +pc3_gen_sort_abst +pc3_head_1 +pc3_head_12 +pc3_head_2 +pc3_head_21 +pc3_ind_left +pc3_ind_left__pc3_left_pc3 +pc3_ind_left__pc3_left_pr3 +pc3_ind_left__pc3_left_sym +pc3_ind_left__pc3_left_trans +pc3_ind_left__pc3_pc3_left +pc3_left +pc3_left_r +pc3_left_ur +pc3_left_ux +pc3_lift +pc3_nf2 +pc3_nf2_unfold +pc3_pc1 +pc3_pr0_pr2_t +pc3_pr2_fsubst0 +pc3_pr2_fsubst0_back +pc3_pr2_pr2_t +pc3_pr2_pr3_t +pc3_pr2_r +pc3_pr2_u +pc3_pr2_u2 +pc3_pr2_x +pc3_pr3_conf +pc3_pr3_pc3_t +pc3_pr3_r +pc3_pr3_t +pc3_pr3_x +pc3_refl +pc3_s +pc3_t +pc3_thin_dx +pc3_wcpr0 +pc3_wcpr0__pc3_wcpr0_t_aux +pc3_wcpr0_t +pr0 +pr0_beta +pr0_comp +pr0_confluence +pr0_confluence__pr0_cong_delta +pr0_confluence__pr0_cong_upsilon_cong +pr0_confluence__pr0_cong_upsilon_delta +pr0_confluence__pr0_cong_upsilon_refl +pr0_confluence__pr0_cong_upsilon_zeta +pr0_confluence__pr0_delta_delta +pr0_confluence__pr0_delta_tau +pr0_confluence__pr0_upsilon_upsilon +pr0_delta +pr0_delta1 +pr0_gen_abbr +pr0_gen_abst +pr0_gen_appl +pr0_gen_cast +pr0_gen_lift +pr0_gen_lref +pr0_gen_sort +pr0_gen_void +pr0_lift +pr0_refl +pr0_subst0 +pr0_subst0_back +pr0_subst0_fwd +pr0_subst1 +pr0_subst1_back +pr0_subst1_fwd +pr0_tau +pr0_upsilon +pr0_zeta +pr1 +pr1_comp +pr1_confluence +pr1_eta +pr1_head_1 +pr1_head_2 +pr1_pr0 +pr1_refl +pr1_sing +pr1_strip +pr1_t +pr2 +pr2_cflat +pr2_change +pr2_confluence +pr2_confluence__pr2_delta_delta +pr2_confluence__pr2_free_delta +pr2_confluence__pr2_free_free +pr2_ctail +pr2_delta +pr2_delta1 +pr2_free +pr2_gen_abbr +pr2_gen_abst +pr2_gen_appl +pr2_gen_cabbr +pr2_gen_cast +pr2_gen_cbind +pr2_gen_cflat +pr2_gen_csort +pr2_gen_ctail +pr2_gen_lift +pr2_gen_lref +pr2_gen_sort +pr2_gen_void +pr2_head_1 +pr2_head_2 +pr2_lift +pr2_subst1 +pr2_thin_dx +pr3 +pr3_cflat +pr3_confluence +pr3_eta +pr3_flat +pr3_gen_abbr +pr3_gen_abst +pr3_gen_appl +pr3_gen_bind +pr3_gen_cabbr +pr3_gen_cast +pr3_gen_lift +pr3_gen_lref +pr3_gen_sort +pr3_gen_void +pr3_head_1 +pr3_head_12 +pr3_head_2 +pr3_head_21 +pr3_iso_appl_bind +pr3_iso_appls_abbr +pr3_iso_appls_appl_bind +pr3_iso_appls_beta +pr3_iso_appls_bind +pr3_iso_appls_cast +pr3_iso_beta +pr3_lift +pr3_pr0_pr2_t +pr3_pr1 +pr3_pr2 +pr3_pr2_pr2_t +pr3_pr2_pr3_t +pr3_pr3_pr3_t +pr3_refl +pr3_sing +pr3_strip +pr3_subst1 +pr3_t +pr3_thin_dx +pr3_wcpr0_t +ptrans +r +r_arith0 +r_arith1 +r_arith2 +r_arith3 +r_arith4 +r_arith5 +r_arith6 +r_arith7 +r_dis +r_minus +r_plus +r_plus_sym +r_S +s +s_arith0 +s_arith1 +sc3 +sc3_abbr +sc3_abst +sc3_appl +sc3_arity +sc3_arity_csubc +sc3_arity_gen +sc3_bind +sc3_cast +sc3_lift +sc3_lift1 +sc3_props__sc3_sn3_abst +sc3_repl +sc3_sn3 +s_inc +s_inj +s_le +s_le_gen +s_lt +s_lt_gen +s_minus +sn3 +sn3_abbr +sn3_appl_abbr +sn3_appl_appl +sn3_appl_appls +sn3_appl_beta +sn3_appl_bind +sn3_appl_cast +sn3_appl_lref +sn3_appls_abbr +sn3_appls_beta +sn3_appls_bind +sn3_appls_cast +sn3_appls_lref +sn3_beta +sn3_bind +sn3_cast +sn3_cdelta +sn3_cflat +sn3_change +sn3_cpr3_trans +sn3_gen_bind +sn3_gen_cflat +sn3_gen_def +sn3_gen_flat +sn3_gen_head +sn3_gen_lift +sn3_lift +sn3_nf2 +sn3_pr2_intro +sn3_pr3_trans +sn3_shift +sn3_sing +sns3 +sns3_lifts +sns3_lifts1 +s_plus +s_plus_sym +s_r +s_S +sty0 +sty0_abbr +sty0_abst +sty0_appl +sty0_bind +sty0_cast +sty0_correct +sty0_gen_appl +sty0_gen_bind +sty0_gen_cast +sty0_gen_lref +sty0_gen_sort +sty0_lift +sty0_sort +sty1 +sty1_abbr +sty1_appl +sty1_bind +sty1_cast2 +sty1_cnt +sty1_correct +sty1_lift +sty1_sing +sty1_sty0 +sty1_trans +subst +subst0 +subst0_both +subst0_confluence_eq +subst0_confluence_lift +subst0_confluence_neq +subst0_fst +subst0_gen_head +subst0_gen_lift_false +subst0_gen_lift_ge +subst0_gen_lift_lt +subst0_gen_lift_rev_ge +subst0_gen_lref +subst0_gen_sort +subst0_lift_ge +subst0_lift_ge_s +subst0_lift_ge_S +subst0_lift_lt +subst0_lref +subst0_refl +subst0_snd +subst0_subst0 +subst0_subst0_back +subst0_tlt +subst0_tlt_head +subst0_trans +subst0_weight_le +subst0_weight_lt +subst1 +subst1_confluence_eq +subst1_confluence_lift +subst1_confluence_neq +subst1_ex +subst1_gen_head +subst1_gen_lift_eq +subst1_gen_lift_ge +subst1_gen_lift_lt +subst1_gen_lref +subst1_gen_sort +subst1_head +subst1_lift_ge +subst1_lift_lt +subst1_lift_S +subst1_refl +subst1_single +subst1_subst1 +subst1_subst1_back +subst1_trans +subst_head +subst_lift_SO +subst_lref_eq +subst_lref_gt +subst_lref_lt +subst_sort +subst_subst0 +T +TApp +TCons +tcons_tapp_ex +term_dec +terms_props__bind_dec +terms_props__flat_dec +terms_props__kind_dec +THead +THeads +theads_tapp +thead_x_lift_y_y +thead_x_y_y +tle +tle_r +TList +tlist_ind_rev +TLRef +tlt +tlt_head_dx +tlt_head_sx +tlt_trans +tlt_wf_ind +tlt_wf__q_ind +TNil +trans +tslen +tslt +tslt_wf_ind +tslt_wf__q_ind +TSort +tweight +tweight_lt +ty3 +ty3_abbr +ty3_abst +ty3_acyclic +ty3_appl +ty3_arity +ty3_bind +ty3_cast +ty3_conv +ty3_correct +ty3_cred_pr2 +ty3_cred_pr3 +ty3_csubst0 +ty3_fsubst0 +ty3_gen_abst_abst +ty3_gen_appl +ty3_gen_appl_nf2 +ty3_gen_bind +ty3_gen_cabbr +ty3_gen_cast +ty3_gen_cvoid +ty3_gen_lift +ty3_gen_lref +ty3_gen_sort +ty3_getl_subst0 +ty3_inference +ty3_inv_appls_lref_nf2 +ty3_inv_lref_lref_nf2 +ty3_inv_lref_nf2 +ty3_inv_lref_nf2_pc3 +ty3_lift +ty3_nf2_gen__ty3_nf2_inv_abst_aux +ty3_nf2_inv_abst +ty3_nf2_inv_abst_premise +ty3_nf2_inv_abst_premise_csort +ty3_nf2_inv_all +ty3_nf2_inv_sort +ty3_predicative +ty3_repellent +ty3_sconv +ty3_sconv_pc3 +ty3_shift1 +ty3_sn3 +ty3_sort +ty3_sred_back +ty3_sred_pr0 +ty3_sred_pr1 +ty3_sred_pr2 +ty3_sred_pr3 +ty3_sred_wcpr0_pr0 +ty3_sty0 +ty3_subst0 +ty3_tred +ty3_typecheck +ty3_unique +tys3 +tys3_cons +tys3_gen_cons +tys3_gen_nil +tys3_nil +Void +wadd +wadd_le +wadd_lt +wadd_O +wcpr0 +wcpr0_comp +wcpr0_drop +wcpr0_drop_back +wcpr0_gen_head +wcpr0_gen_sort +wcpr0_getl +wcpr0_getl_back +wcpr0_refl +weight +weight_add_O +weight_add_S +weight_eq +weight_le +weight_map +wf3 +wf3_bind +wf3_clear_conf +wf3_flat +wf3_gen_bind1 +wf3_gen_flat1 +wf3_gen_head2 +wf3_gen_sort1 +wf3_getl_conf +wf3_idem +wf3_mono +wf3_pc3_conf +wf3_pr2_conf +wf3_pr3_conf +wf3_sort +wf3_total +wf3_ty3 +wf3_ty3_conf +wf3_void diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index d80ea011a..852ff574b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -1,105 +1,1207 @@ -NAMING CONVENTIONS FOR METAVARIABLES - -A,B : arity -C : candidate of reducibility -D,E : RTM environment -F,G : global environment -H : reserved: transient premise -IH : reserved: inductive premise -I,J : item -K,L : local environment -M,N : reserved: future use -O : -P : relocation environment -Q : elimination predicate -R : generic predicate/relation -S : RTM stack -T,U,V,W: term -X,Y,Z : reserved: transient objet denoted by a capital letter - -a : applicability condition (true = restricted, false = general) -b : local dropping kind parameter (true = restricted, false = general) -c : rt-reduction count parameter -d : term degree -e : reserved: future use (\lambda\delta 3) -f,g : local reference transforming map -h : sort hierarchy parameter -i,j : local reference depth (de Bruijn's) -k,l : global reference level -m,n : iterations -o : sort degree parameter (origin) -p,q : binder polarity -r : -s : sort index -t,u : -v,w : local reference position level (de Bruijn's) (RTM) -x,y,z : reserved: transient objet denoted by a small letter - -NAMING CONVENTIONS FOR CONSTRUCTORS - -0: atomic -2: binary - -A: application to vector -E: empty list -F: boolean false -T: boolean true - -a: application -b: generic binder with one argument -d: abbreviation -f: generic flat with one argument -i: generic binder for local environments -l: typed abstraction -n: native type annotation -u: generic binder with zero argument -x: exclusion - -NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS - -- prefix and first letter - -b: bi contex-sensitive for local environments -c: contex-sensitive for terms -f: context-freee for closures -l: sn contex-sensitive for local environments -r: dx contex-sensitive for local environments -s: stratified (prefix) -t: context-free for terms - -- second letter - -e: reserved for generic entrywise extension -i: irreducible form -n: normal form -p: reflexive parallel transformation -q: sequential transformation -r: reducible form -s: strongly normalizing form - -- third letter - -b: (q)rst-reduction -c: conversion -d: decomposed rt-reduction -e: decomposed rt-conversion -g: counted rt-transition (generic) -m: semi-counted rt-transition (mixed) -q: restricted reduction -r: reduction -s: substitution -u: supclosure -w: reserved for generic pointwise extension -x: uncounted rt-transition (extended) -y: rt-substitution - -- forth letter (if present) - -c: proper single step (general) (successor) -e: reflexive transitive closure to normal form (evaluation) -g: proper multiple step (general) (greater) -p: non-reflexive transitive closure (plus) -q: reflexive closure (question) -r: proper multiple step (restricted) (restricted) -s: reflexive transitive closure (star) -u: proper single step (restricted) (unit) +aaa_cpm_SO +aaa_csx +aaa_fsb +aaa_ind_csx +aaa_ind_csx_aux +aaa_ind_csx_cpxs +aaa_ind_csx_cpxs_aux +aaa_ind_fpb +aaa_ind_fpb_aux +aaa_ind_fpbg +aaa_ind_fpbg_aux +cnr +cnr_abbr_neg +cnr_abst +cnr_appl_simple +cnr_dec_teqx +cnr_gref +cnr_inv_abbr_neg +cnr_inv_abst +cnr_inv_appl +cnr_inv_cast +cnr_inv_lifts +cnr_inv_lref_abbr +cnr_lifts +cnr_lref_abst +cnr_lref_atom +cnr_lref_unit +cnr_sort +cnuw +cnuw_abbr_neg +cnuw_abst +cnuw_appl_simple +cnuw_atom_drops +cnuw_cpms_trans +cnuw_ctop +cnuw_dec +cnuw_dec_ex +cnuw_fwd_appl +cnuw_gref +cnuw_inv_abbr_pos +cnuw_inv_cast +cnuw_inv_lifts +cnuw_inv_zero_pair +cnuw_lifts +cnuw_lref +cnuw_sort +cnuw_unit_drops +cnuw_zero_unit +cnv +cnv_acle_omega +cnv_acle_one +cnv_acle_trans +cnv_appl +cnv_appl_cpes +cnv_appl_cpts +cnv_appl_ge +cnv_appl_ntas_ge +cnv_bind +cnv_cast +cnv_cast_cpes +cnv_cast_cpts +cnv_cpcs_dec +cnv_cpes_dec +cnv_cpm_conf_lpr_appl_appl_aux +cnv_cpm_conf_lpr_appl_beta_aux +cnv_cpm_conf_lpr_appl_theta_aux +cnv_cpm_conf_lpr_atom_atom_aux +cnv_cpm_conf_lpr_atom_delta_aux +cnv_cpm_conf_lpr_atom_ell_aux +cnv_cpm_conf_lpr_atom_ess_aux +cnv_cpm_conf_lpr_aux +cnv_cpm_conf_lpr_beta_beta_aux +cnv_cpm_conf_lpr_bind_bind_aux +cnv_cpm_conf_lpr_bind_zeta_aux +cnv_cpm_conf_lpr_cast_cast_aux +cnv_cpm_conf_lpr_cast_ee_aux +cnv_cpm_conf_lpr_cast_epsilon_aux +cnv_cpm_conf_lpr_delta_delta_aux +cnv_cpm_conf_lpr_delta_ell_aux +cnv_cpm_conf_lpr_ee_ee_aux +cnv_cpm_conf_lpr_epsilon_ee_aux +cnv_cpm_conf_lpr_epsilon_epsilon_aux +cnv_cpm_conf_lpr_sub +cnv_cpm_conf_lpr_theta_theta_aux +cnv_cpm_conf_lpr_zeta_zeta_aux +cnv_cpmre_cpms_conf +cnv_cpmre_mono +cnv_cpmre_trans +cnv_cpms_conf +cnv_cpms_conf_eq +cnv_cpms_conf_lpr +cnv_cpms_conf_lpr_aux +cnv_cpms_conf_lpr_refl_tneqx_sub +cnv_cpms_conf_lpr_step_tneqx_sub +cnv_cpms_conf_lpr_teqx_teqx_aux +cnv_cpms_conf_lpr_teqx_tneqx_aux +cnv_cpms_conf_lpr_tneqx_tneqx_aux +cnv_cpms_fwd_appl_sn_decompose +cnv_cpms_nta +cnv_cpms_ntas +cnv_cpms_strip_lpr_sub +cnv_cpms_teqx_conf_lpr_aux +cnv_cpms_teqx_strip_lpr_aux +cnv_cpms_trans +cnv_cpms_trans_lpr +cnv_cpms_trans_lpr_sub +cnv_cpm_teqx_conf_lpr +cnv_cpm_teqx_conf_lpr_appl_appl_aux +cnv_cpm_teqx_conf_lpr_atom_atom_aux +cnv_cpm_teqx_conf_lpr_atom_ess_aux +cnv_cpm_teqx_conf_lpr_aux +cnv_cpm_teqx_conf_lpr_bind_bind_aux +cnv_cpm_teqx_conf_lpr_cast_cast_aux +cnv_cpm_teqx_cpm_trans_aux +cnv_cpm_teqx_cpm_trans_sub +cnv_cpm_trans +cnv_cpm_trans_lpr +cnv_cpm_trans_lpr_aux +cnv_cpmuwe_mono +cnv_cpmuwe_trans +cnv_cpr_teqx_fwd_refl +cnv_dec +cnv_fpbg_refl_false +cnv_fqu_conf +cnv_fqup_conf +cnv_fquq_conf +cnv_fqus_conf +cnv_fwd_aaa +cnv_fwd_cpms_abst_dx_le +cnv_fwd_cpm_SO +cnv_fwd_cpms_total +cnv_fwd_csx +cnv_fwd_flat +cnv_fwd_fsb +cnv_fwd_pair_sn +cnv_ind_cpes +cnv_inv_appl +cnv_inv_appl_aux +cnv_inv_appl_cpes +cnv_inv_appl_cpts +cnv_inv_appl_ntas +cnv_inv_bind +cnv_inv_bind_aux +cnv_inv_cast +cnv_inv_cast_aux +cnv_inv_cast_cpes +cnv_inv_cast_cpts +cnv_inv_gref +cnv_inv_gref_aux +cnv_inv_lifts +cnv_inv_lref +cnv_inv_lref_atom +cnv_inv_lref_aux +cnv_inv_lref_drops +cnv_inv_lref_pair +cnv_inv_lref_unit +cnv_inv_zero +cnv_inv_zero_aux +cnv_lifts +cnv_lprs_trans +cnv_lpr_trans +cnv_lref +cnv_lref_drops +cnv_nta_sn +cnv_preserve +cnv_R_cpmuwe_dec +cnv_R_cpmuwe_total +cnv_sort +cnv_zero +cnx +cnx_abst +cnx_appl_simple +cnx_csx +cnx_inv_abbr_neg +cnx_inv_abbr_pos +cnx_inv_abst +cnx_inv_appl +cnx_inv_cast +cnx_inv_lifts +cnx_inv_lref_pair +cnx_lifts +cnx_lref_atom +cnx_lref_unit +cnx_sort +cnx_teqx_trans +cpc +cpc_conf +cpc_cpcs +cpc_fwd_cpr +cpc_refl +cpcs +cpcs_aaa_mono +cpcs_bind1 +cpcs_bind2 +cpcs_bind_dx +cpcs_bind_sn +cpcs_canc_dx +cpcs_canc_sn +cpcs_cpr_conf +cpcs_cpr_div +cpcs_cprs_conf +cpcs_cprs_div +cpcs_cprs_dx +cpcs_cprs_sn +cpcs_cprs_step_dx +cpcs_cprs_step_sn +cpcs_cpr_step_dx +cpcs_cpr_step_sn +cpcs_flat +cpcs_flat_dx_cpr_rev +cpcs_ind_dx +cpcs_ind_sn +cpcs_inv_abst_bi_dx +cpcs_inv_abst_bi_sn +cpcs_inv_abst_dx +cpcs_inv_abst_sn +cpcs_inv_cprs +cpcs_inv_lifts_bi +cpcs_inv_sort_abst +cpcs_inv_sort_bi +cpcs_lifts_bi +cpcs_refl +cpcs_step_dx +cpcs_step_sn +cpcs_strip +cpcs_sym +cpcs_trans +cpc_sym +cpes +cpes_aaa_mono +cpes_cpes_trans +cpes_cpms_div +cpes_cprs_trans +cpes_fwd_abst_bi +cpes_refl +cpes_refl_aaa +cpes_sym +cpg +cpg_appl +cpg_atom +cpg_beta +cpg_bind +cpg_cast +cpg_cpx +cpg_delta +cpg_delta_drops +cpg_ee +cpg_ell +cpg_ell_drops +cpg_eps +cpg_ess +cpg_fwd_bind1_minus +cpg_inv_abbr1 +cpg_inv_abst1 +cpg_inv_appl1 +cpg_inv_appl1_aux +cpg_inv_appl1_simple +cpg_inv_atom1 +cpg_inv_atom1_aux +cpg_inv_atom1_drops +cpg_inv_bind1 +cpg_inv_bind1_aux +cpg_inv_cast1 +cpg_inv_cast1_aux +cpg_inv_gref1 +cpg_inv_lifts_bi +cpg_inv_lifts_sn +cpg_inv_lref1 +cpg_inv_lref1_bind +cpg_inv_lref1_drops +cpg_inv_sort1 +cpg_inv_zero1 +cpg_inv_zero1_pair +cpg_lifts_bi +cpg_lifts_sn +cpg_lref +cpg_refl +cpg_theta +cpg_zeta +cpm +cpm_aaa_conf +cpm_appl +cpm_beta +cpm_bind +cpm_bind2 +cpm_bind_unit +cpm_cast +cpm_cpms +cpm_delta +cpm_delta_drops +cpm_ee +cpm_ell +cpm_ell_drops +cpm_eps +cpm_ess +cpm_fpb +cpm_fpbq +cpm_fsge_comp +cpm_fwd_bind1_minus +cpm_fwd_cpx +cpm_fwd_plus +cpm_fwd_plus_aux +cpm_ind +cpm_inv_abbr1 +cpm_inv_abst1 +cpm_inv_abst_bi +cpm_inv_appl1 +cpm_inv_appl1_simple +cpm_inv_atom1 +cpm_inv_atom1_drops +cpm_inv_bind1 +cpm_inv_cast1 +cpm_inv_gref1 +cpm_inv_lifts_bi +cpm_inv_lifts_sn +cpm_inv_lref1 +cpm_inv_lref1_ctop +cpm_inv_lref1_drops +cpm_inv_sort1 +cpm_inv_zero1 +cpm_inv_zero1_unit +cpm_lifts_bi +cpm_lifts_sn +cpm_lref +cpmre +cpmre_fwd_cpms +cpmre_intro +cpmre_total_aaa +cpm_rex_conf +cpms +cpms_aaa_conf +cpms_abst_dx_le_aaa +cpms_appl +cpms_appl_dx +cpms_beta +cpms_beta_dx +cpms_beta_rc +cpms_bind +cpms_bind2_dx +cpms_bind_alt +cpms_bind_dx +cpms_cast +cpms_cast_sn +cpms_cprre_trans +cpms_cprs_trans +cpms_delta +cpms_delta_drops +cpms_div +cpms_ee +cpms_ell +cpms_ell_drops +cpms_eps +cpms_fpbg_trans +cpms_fwd_cpxs +cpms_fwd_fpbs +cpms_ind_dx +cpms_ind_sn +cpms_inv_abbr_abst +cpms_inv_abbr_sn_dx +cpms_inv_abst_bi +cpms_inv_abst_sn +cpms_inv_abst_sn_cprs +cpms_inv_appl_sn +cpms_inv_cast1 +cpms_inv_delta_sn +cpms_inv_ell_sn +cpms_inv_gref1 +cpms_inv_lifts_bi +cpms_inv_lifts_sn +cpms_inv_lref1_ctop +cpms_inv_lref1_drops +cpms_inv_lref_sn +cpms_inv_plus +cpms_inv_sort1 +cpms_inv_succ_sn +cpms_inv_zero1_unit +cpms_lifts_bi +cpms_lifts_sn +cpms_lref +cpm_sort +cpms_reqx_conf_dx +cpms_reqx_conf_sn +cpms_sort +cpms_step_dx +cpms_step_sn +cpms_teqx_ind_sn +cpms_theta +cpms_theta_dx +cpms_theta_rc +cpms_tneqx_fwd_fpbg +cpms_tneqx_fwd_step_sn_aux +cpms_total_aaa +cpms_trans +cpms_trans_swap +cpms_zeta +cpms_zeta_dx +cpm_teqx_free +cpm_teqx_ind +cpm_teqx_inv_appl_sn +cpm_teqx_inv_atom_sn +cpm_teqx_inv_bind_dx +cpm_teqx_inv_bind_sn +cpm_teqx_inv_bind_sn_void +cpm_teqx_inv_cast_sn +cpm_teqx_inv_lref_sn +cpm_theta +cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg +cpm_tneqx_cpm_fpbg +cpmuwe +cpmuwe_abbr_neg +cpmuwe_abst +cpmuwe_ctop +cpmuwe_fwd_cpms +cpmuwe_gref +cpmuwe_intro +cpmuwe_sort +cpmuwe_total_csx +cpmuwe_zero_unit +cpm_zeta +cpr_abbr_pos_tneqx +cpr_conf +cpr_conf_lpr +cpr_conf_lpr_atom_atom +cpr_conf_lpr_atom_delta +cpr_conf_lpr_beta_beta +cpr_conf_lpr_bind_bind +cpr_conf_lpr_bind_zeta +cpr_conf_lpr_delta_delta +cpr_conf_lpr_eps_eps +cpr_conf_lpr_flat_beta +cpr_conf_lpr_flat_eps +cpr_conf_lpr_flat_flat +cpr_conf_lpr_flat_theta +cpr_conf_lpr_theta_theta +cpr_conf_lpr_zeta_zeta +cpr_cpcs_dx +cpr_cpcs_sn +cpr_cprs_conf_cpcs +cpr_cprs_div +cpr_div +cpr_ext +cpr_flat +cpr_ind +cpr_inv_atom1 +cpr_inv_atom1_drops +cpr_inv_cast1 +cpr_inv_flat1 +cpr_inv_gref1 +cpr_inv_lref1 +cpr_inv_lref1_drops +cpr_inv_sort1 +cpr_inv_zero1 +cpr_pair_sn +cprre_cprs_conf +cpr_refl +cprre_mono +cprre_total_csx +cprs_abbr_pos_twneq +cprs_conf +cprs_conf_cpcs +cprs_cpr_conf_cpcs +cprs_cpr_div +cprs_CTC +cprs_div +cprs_ext +cprs_flat +cprs_flat_dx +cprs_flat_sn +cprs_ind_dx +cprs_ind_sn +cprs_inv_appl_sn +cprs_inv_cast1 +cprs_inv_cnr_sn +cprs_inv_CTC +cprs_inv_lref1_drops +cprs_inv_sort1 +cprs_lpr_conf_dx +cprs_lpr_conf_sn +cprs_nta_trans +cprs_nta_trans_cnv +cprs_refl +cprs_step_dx +cprs_step_sn +cprs_strip +cprs_trans +cpr_subst +cpt +cpt_appl +cpt_bind +cpt_cast +cpt_cpts +cpt_delta +cpt_delta_drops +cpt_ee +cpt_ell +cpt_ell_drops +cpt_ess +cpt_fwd_cpm +cpt_fwd_plus +cpt_fwd_plus_aux +cpt_ind +cpt_inv_appl_sn +cpt_inv_atom_sn +cpt_inv_atom_sn_drops +cpt_inv_bind_sn +cpt_inv_cast_sn +cpt_inv_gref_sn +cpt_inv_lifts_bi +cpt_inv_lifts_sn +cpt_inv_lref_sn +cpt_inv_lref_sn_ctop +cpt_inv_lref_sn_drops +cpt_inv_sort_sn +cpt_inv_zero_sn +cpt_inv_zero_sn_unit +cpt_lifts_bi +cpt_lifts_sn +cpt_lref +cpt_refl +cpts +cpts_appl_dx +cpts_bind_dx +cpts_cast_sn +cpts_cpms_conf_eq +cpts_cprs_trans +cpts_delta +cpts_delta_drops +cpts_ee +cpts_ell +cpts_ell_drops +cpts_fwd_cpms +cpts_ind_dx +cpts_ind_sn +cpts_inv_cast_sn +cpts_inv_delta_sn +cpts_inv_ell_sn +cpts_inv_gref_sn +cpts_inv_lifts_bi +cpts_inv_lifts_sn +cpts_inv_lref_sn +cpts_inv_lref_sn_ctop +cpts_inv_lref_sn_drops +cpts_inv_sort_sn +cpts_inv_succ_sn +cpts_inv_zero_sn_unit +cpts_lifts_bi +cpts_lifts_sn +cpts_lref +cpt_sort +cpts_refl +cpts_sort +cpts_step_dx +cpts_step_sn +cpts_total_aaa +cpx +cpx_aaa_conf +cpx_aaa_conf_lpx +cpx_beta +cpx_bind +cpx_bind2 +cpx_bind_unit +cpx_cpxs +cpx_delta +cpx_delta_drops +cpx_ee +cpx_eps +cpx_ess +cpx_ext +cpx_flat +cpx_fsge_comp +cpx_fwd_bind1_minus +cpx_ind +cpx_inv_abbr1 +cpx_inv_abst1 +cpx_inv_appl1 +cpx_inv_appl1_simple +cpx_inv_atom1 +cpx_inv_atom1_drops +cpx_inv_bind1 +cpx_inv_cast1 +cpx_inv_flat1 +cpx_inv_gref1 +cpx_inv_lifts_bi +cpx_inv_lifts_sn +cpx_inv_lref1 +cpx_inv_lref1_bind +cpx_inv_lref1_drops +cpx_inv_sort1 +cpx_inv_zero1 +cpx_inv_zero1_pair +cpx_lifts_bi +cpx_lifts_sn +cpx_lref +cpx_pair_sn +cpx_refl +cpx_req_conf_sn +cpx_reqx_conf +cpx_reqx_conf_dx +cpx_reqx_conf_sn +cpx_rex_conf +cpxs +cpxs_aaa_conf +cpxs_beta +cpxs_beta_dx +cpxs_beta_rc +cpxs_bind +cpxs_bind2_dx +cpxs_bind_alt +cpxs_bind_dx +cpxs_cnx +cpxs_delta +cpxs_delta_drops +cpxs_ee +cpxs_eps +cpxs_ext +cpxs_flat +cpxs_flat_dx +cpxs_flat_sn +cpxs_fpbg_trans +cpxs_fpbs +cpxs_fpbs_trans +cpxs_fqup_fpbs +cpxs_fqus_fpbs +cpxs_fqus_lpxs_fpbs +cpxs_fwd_beta +cpxs_fwd_beta_vector +cpxs_fwd_cast +cpxs_fwd_cast_vector +cpxs_fwd_cnx +cpxs_fwd_cnx_vector +cpxs_fwd_delta_drops +cpxs_fwd_delta_drops_vector +cpxs_fwd_sort +cpxs_fwd_sort_vector +cpxs_fwd_theta +cpxs_fwd_theta_vector +cpxs_ind +cpxs_ind_dx +cpxs_inv_abbr1_dx +cpxs_inv_abst1 +cpxs_inv_appl1 +cpxs_inv_cast1 +cpxs_inv_cnx1 +cpxs_inv_lifts_bi +cpxs_inv_lifts_sn +cpxs_inv_lref1 +cpxs_inv_lref1_drops +cpxs_inv_sort1 +cpxs_inv_zero1 +cpxs_lifts_bi +cpxs_lifts_sn +cpxs_lref +cpxs_pair_sn +cpxs_refl +cpxs_reqx_conf +cpxs_reqx_conf_dx +cpxs_reqx_conf_sn +cpxs_sort +cpxs_strap1 +cpxs_strap2 +cpxs_teqx_fpbs +cpxs_teqx_fpbs_trans +cpxs_theta +cpxs_theta_dx +cpxs_theta_rc +cpxs_tneqx_fpbg +cpxs_tneqx_fwd_step_sn +cpxs_trans +cpx_subst +cpxs_zeta +cpxs_zeta_dx +cpx_teqx_conf +cpx_teqx_conf_rex +cpx_theta +cpx_zeta +csx +csx_abbr +csx_abst +csx_appl_beta +csx_appl_beta_aux +csx_appl_simple +csx_appl_simple_teqo +csx_appl_theta +csx_appl_theta_aux +csx_applv_beta +csx_applv_cast +csx_applv_cnx +csx_applv_delta_drops +csx_applv_sort +csx_applv_theta +csx_bind +csx_cast +csx_cpcs_dec +csx_cpxs_trans +csx_cpx_trans +csx_feqx_conf +csx_fpbq_conf +csx_fqu_conf +csx_fqup_conf +csx_fquq_conf +csx_fqus_conf +csx_fsb +csx_fsb_fpbs +csx_fwd_applv +csx_fwd_bind +csx_fwd_bind_dx +csx_fwd_bind_dx_aux +csx_fwd_bind_dx_unit +csx_fwd_bind_dx_unit_aux +csx_fwd_bind_unit +csx_fwd_flat +csx_fwd_flat_dx +csx_fwd_flat_dx_aux +csx_fwd_pair_sn +csx_fwd_pair_sn_aux +csx_gcp +csx_gcr +csx_ind +csx_ind_cpxs +csx_ind_cpxs_teqx +csx_ind_fpb +csx_ind_fpbg +csx_intro +csx_intro_cpxs +csx_inv_lifts +csx_inv_lref_drops +csx_inv_lref_pair_drops +csx_lifts +csx_lpx_conf +csx_lpxs_conf +csx_lref_pair_drops +csx_lsubr_conf +csx_reqx_conf +csx_reqx_trans +csx_rsx +csx_sort +csx_teqx_trans +csxv +csxv_inv_cons +drops_lprs_trans +drops_lpr_trans +drops_lpxs_trans +drops_lpx_trans +feqx_cpxs_trans +feqx_cpx_trans +feqx_fpbg_trans +feqx_fpbs +feqx_fpbs_trans +feqx_fpb_trans +feqx_lpxs_trans +fleq_rpx +fpb +fpb_cpx +fpb_fpbg +fpb_fpbg_trans +fpb_fpbq +fpb_fpbq_fneqx +fpb_fpbs +fpb_fqu +fpbg +fpbg_cpms_trans +fpbg_feqx_trans +fpbg_fpbq_trans +fpbg_fpbs_trans +fpbg_fqu_trans +fpbg_fwd_fpbs +fpbg_teqx_div +fpbg_trans +fpb_inv_feqx +fpb_lpx +fpbq +fpbq_aaa_conf +fpbq_cpx +fpbq_feqx +fpbq_fneqx_inv_fpb +fpbq_fpbg_trans +fpbq_fpbs +fpbq_fquq +fpbq_inv_fpb +fpbq_lpx +fpbq_refl +fpbs +fpbs_aaa_conf +fpbs_cpxs_teqx_fqup_lpx_trans +fpbs_cpxs_trans +fpbs_cpx_tneqx_trans +fpbs_csx_conf +fpbs_feqx_trans +fpbs_fpbg_trans +fpbs_fpb_trans +fpbs_fqup_trans +fpbs_fqus_trans +fpbs_ind +fpbs_ind_dx +fpbs_intro_star +fpbs_inv_fpbg +fpbs_inv_star +fpbs_lpxs_trans +fpbs_lpx_trans +fpbs_refl +fpbs_strap1 +fpbs_strap2 +fpbs_teqx_trans +fpbs_trans +fqu_cpr_trans_dx +fqu_cpr_trans_sn +fqu_cpxs_trans +fqu_cpxs_trans_tneqx +fqu_cpx_trans +fqu_cpx_trans_tneqx +fqu_lpr_trans +fqu_lpx_trans +fqup_cpms_fwd_fpbg +fqup_cpxs_trans +fqup_cpxs_trans_tneqx +fqup_cpx_trans +fqup_cpx_trans_tneqx +fqup_fpbg +fqup_fpbg_trans +fqup_fpbs +fqup_fpbs_trans +fquq_cpr_trans_dx +fquq_cpr_trans_sn +fquq_cpxs_trans +fquq_cpxs_trans_tneqx +fquq_cpx_trans +fquq_cpx_trans_tneqx +fquq_lpr_trans +fquq_lpx_trans +fqus_cpxs_trans +fqus_cpxs_trans_tneqx +fqus_cpx_trans +fqus_cpx_trans_tneqx +fqus_fpbs +fqus_fpbs_trans +fqus_lpxs_fpbs +fsb +fsb_feqx_trans +fsb_fpbg_refl_false +fsb_fpbs_trans +fsb_ind_alt +fsb_ind_fpbg +fsb_ind_fpbg_fpbs +fsb_intro +fsb_intro_fpbg +fsb_inv_csx +IH_cnv_cpm_conf_lpr +IH_cnv_cpms_conf_lpr +IH_cnv_cpms_strip_lpr +IH_cnv_cpms_trans_lpr +IH_cnv_cpm_teqx_conf_lpr +IH_cnv_cpm_teqx_cpm_trans +IH_cnv_cpm_trans_lpr +IH_cpr_conf_lpr +jsx +jsx_atom +jsx_bind +jsx_csx_conf +jsx_fwd_bind_sn +jsx_fwd_drops_atom_sn +jsx_fwd_drops_pair_sn +jsx_fwd_drops_unit_sn +jsx_fwd_lsubr +jsx_inv_atom_sn +jsx_inv_atom_sn_aux +jsx_inv_bind_sn +jsx_inv_bind_sn_aux +jsx_inv_pair_sn +jsx_inv_void_sn +jsx_pair +jsx_refl +jsx_trans +lfsx_atom +lpr +lpr_aaa_conf +lpr_bind +lpr_bind_refl_dx +lpr_conf +lpr_cpcs_conf +lpr_cpcs_trans +lpr_cpms_trans +lpr_cpm_trans +lpr_cpr_conf +lpr_cpr_conf_dx +lpr_cpr_conf_sn +lpr_cprs_conf +lpr_cprs_trans +lpr_cpr_trans +lpr_drops_conf +lpr_drops_trans +lpr_fpb +lpr_fpbq +lpr_fquq_trans +lpr_fqu_trans +lpr_fwd_length +lpr_fwd_lpx +lpr_inv_atom_dx +lpr_inv_atom_sn +lpr_inv_bind_dx +lpr_inv_bind_sn +lpr_inv_pair +lpr_inv_pair_dx +lpr_inv_pair_sn +lpr_inv_unit_dx +lpr_inv_unit_sn +lpr_lprs +lpr_pair +lpr_refl +lprs +lprs_aaa_conf +lprs_bind_refl_dx +lprs_conf +lprs_cpcs_trans +lprs_cpms_trans +lprs_cpm_trans +lprs_cpr_conf_dx +lprs_cpr_conf_sn +lprs_cprs_conf +lprs_cprs_conf_dx +lprs_cprs_conf_sn +lprs_CTC +lprs_drops_conf +lprs_drops_trans +lprs_fwd_length +lprs_fwd_lpxs +lprs_ind +lprs_ind_dx +lprs_ind_sn +lprs_inv_atom_dx +lprs_inv_atom_sn +lprs_inv_CTC +lprs_inv_pair_dx +lprs_inv_pair_sn +lprs_inv_TC +lprs_pair +lprs_pair_dx +lprs_refl +lprs_step_dx +lprs_step_sn +lprs_strip +lprs_TC +lprs_trans +lpx +lpx_aaa_conf +lpx_bind +lpx_bind_refl_dx +lpx_cpx_conf_fsge +lpx_cpxs_trans +lpx_cpx_trans +lpx_drops_conf +lpx_drops_trans +lpx_fqup_trans +lpx_fquq_trans +lpx_fqus_trans +lpx_fqu_trans +lpx_fsge_comp +lpx_fwd_length +lpx_inv_atom_dx +lpx_inv_atom_sn +lpx_inv_bind_dx +lpx_inv_bind_sn +lpx_inv_pair +lpx_inv_pair_dx +lpx_inv_pair_sn +lpx_inv_unit_dx +lpx_inv_unit_sn +lpx_lpxs +lpx_pair +lpx_refl +lpx_rpx +lpxs +lpxs_aaa_conf +lpxs_bind_refl_dx +lpxs_cpxs_trans +lpxs_cpx_trans +lpxs_drops_conf +lpxs_drops_trans +lpxs_feqx_fpbs +lpxs_fpbs +lpxs_fpbs_trans +lpxs_fwd_length +lpxs_ind +lpxs_ind_dx +lpxs_ind_sn +lpxs_inv_atom_dx +lpxs_inv_atom_sn +lpxs_inv_bind_sn +lpxs_inv_pair_dx +lpxs_inv_pair_sn +lpxs_pair +lpxs_pair_dx +lpxs_refl +lpxs_rneqx_fpbg +lpxs_rneqx_inv_step_sn +lpxs_step_dx +lpxs_step_sn +lpxs_trans +lsubr_cpcs_trans +lsubr_cpg_trans +lsubr_cpms_trans +lsubr_cpm_trans +lsubr_cpxs_trans +lsubr_cpx_trans +lsubsv_fwd_lsuba +lsubv +lsubv_atom +lsubv_beta +lsubv_bind +lsubv_cnv_trans +lsubv_cpcs_trans +lsubv_cpms_trans +lsubv_drops_conf_isuni +lsubv_drops_trans_isuni +lsubv_fwd_lsubr +lsubv_inv_abst_sn +lsubv_inv_atom_dx +lsubv_inv_atom_dx_aux +lsubv_inv_atom_sn +lsubv_inv_atom_sn_aux +lsubv_inv_bind_dx +lsubv_inv_bind_dx_aux +lsubv_inv_bind_sn +lsubv_inv_bind_sn_aux +lsubv_refl +lsubv_trans +nta +nta_abst_predicative +nta_abst_repellent +nta_appl +nta_appl_abst +nta_appl_ntas_pos +nta_appl_ntas_zero +nta_bind_cnv +nta_cast +nta_cast_old +nta_conv +nta_conv_cnv +nta_cpcs_bi +nta_cpcs_conf +nta_cpcs_conf_cnv +nta_cpr_conf +nta_cpr_conf_lpr +nta_cprs_conf +nta_cprs_trans +nta_fwd_aaa +nta_fwd_cnv_dx +nta_fwd_cnv_sn +nta_fwd_correct +nta_fwd_fsb +nta_ind_cnv +nta_ind_ext_cnv +nta_ind_ext_cnv_mixed +nta_ind_rest_cnv +nta_inference_dec +nta_inv_abst_bi_cnv +nta_inv_appl_sn +nta_inv_appl_sn_ntas +nta_inv_bind_sn_cnv +nta_inv_cast_sn +nta_inv_cast_sn_old +nta_inv_gref_sn +nta_inv_ldec_sn_cnv +nta_inv_ldef_sn +nta_inv_lifts_sn +nta_inv_lref_sn +nta_inv_lref_sn_drops_cnv +nta_inv_pure_sn_cnv +nta_inv_sort_sn +nta_ldec_cnv +nta_ldec_drops_cnv +nta_ldef +nta_ldef_drops +nta_lifts_bi +nta_lifts_sn +nta_lpr_conf +nta_lprs_conf +nta_lref +nta_mono +nta_ntas +nta_pure_cnv +ntas +ntas_bind_cnv +ntas_fwd_cnv_dx +ntas_fwd_cnv_sn +ntas_ind_bi_nta +ntas_intro +ntas_inv_appl_sn +ntas_inv_nta +ntas_inv_plus +ntas_inv_zero +nta_sort +ntas_refl +ntas_sort +ntas_step_dx +ntas_step_sn +ntas_trans +ntas_zero +nta_typecheck +nta_typecheck_dec +R_cpmuwe +R_cpmuwe_total_csx +req_cpx_trans +reqx_cpxs_trans +reqx_cpx_trans +reqx_fpb_trans +reqx_lpxs_trans +reqx_lpx_trans +reqx_rpx_trans +rpr_fsge_comp +rpx +rpx_atom +rpx_bind +rpx_bind_dx_split +rpx_bind_dx_split_void +rpx_bind_repl_dx +rpx_bind_void +rpx_cpx_conf +rpx_cpx_conf_fsge +rpx_cpx_conf_fsge_dx +rpx_flat +rpx_flat_dx_split +rpx_fsge_comp +rpx_fwd_bind_dx +rpx_fwd_bind_dx_void +rpx_fwd_flat_dx +rpx_fwd_length +rpx_fwd_pair_sn +rpx_gref +rpx_inv_atom_dx +rpx_inv_atom_sn +rpx_inv_bind +rpx_inv_bind_void +rpx_inv_flat +rpx_inv_gref +rpx_inv_gref_bind_dx +rpx_inv_gref_bind_sn +rpx_inv_lifts_bi +rpx_inv_lifts_dx +rpx_inv_lifts_sn +rpx_inv_lpx_req +rpx_inv_lref +rpx_inv_lref_bind_dx +rpx_inv_lref_bind_sn +rpx_inv_sort +rpx_inv_sort_bind_dx +rpx_inv_sort_bind_sn +rpx_inv_zero_length +rpx_inv_zero_pair_dx +rpx_inv_zero_pair_sn +rpx_lifts_sn +rpx_lref +rpx_pair +rpx_pair_refl +rpx_pair_sn_split +rpx_refl +rpx_reqx_conf +rpx_sort +rpx_teqx_conf +rpx_teqx_div +rsx +rsx_bind +rsx_bind_lpxs_aux +rsx_bind_lpxs_void_aux +rsx_bind_void +rsx_cpxs_trans +rsx_cpx_trans +rsx_cpx_trans_jsx +rsx_flat +rsx_flat_lpxs +rsx_fwd_bind_dx_void +rsx_fwd_flat_dx +rsx_fwd_lref_pair_csx +rsx_fwd_lref_pair_csx_aux +rsx_fwd_lref_pair_csx_drops +rsx_fwd_lref_pair_drops +rsx_fwd_pair +rsx_fwd_pair_aux +rsx_fwd_pair_sn +rsx_gref +rsx_ind +rsx_ind_lpxs +rsx_ind_lpxs_reqx +rsx_intro +rsx_intro_lpxs +rsx_inv_bind_void +rsx_inv_flat +rsx_inv_lifts +rsx_inv_lref_drops +rsx_inv_lref_pair +rsx_inv_lref_pair_drops +rsx_jsx_trans +rsx_lifts +rsx_lpxs_trans +rsx_lpx_trans +rsx_lref_atom_drops +rsx_lref_pair +rsx_lref_pair_drops +rsx_lref_pair_lpxs +rsx_lref_unit_drops +rsx_reqx_trans +rsx_sort +rsx_unit +teqx_cpxs_trans +teqx_cpx_trans +teqx_fpbs_trans +teqx_fpb_trans +teqx_reqx_lpx_fpbs diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma index bee160dd3..4e6732f13 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma @@ -32,7 +32,7 @@ lemma lprs_cpm_trans (h) (n) (G) (T1:term) (T2:term): /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-. (* Basic_2A1: includes cprs_bind2 *) -lemma cpms_bind_dx (h) (n) (G) (L): +lemma cpms_bind_alt (h) (n) (G) (L): ∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 → ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ➡*[h,n] T2 → ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma index 87f5bc330..d820662f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma @@ -19,16 +19,17 @@ include "basic_2/rt_computation/lpxs_lpx.ma". (* Properties with context-sensitive extended rt-computation for terms ******) (* Basic_2A1: was: cpxs_bind2 *) -lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 → - ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ⬈*[h] T2 → - ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈*[h] ⓑ[p,I]V2.T2. +lemma cpxs_bind_alt (h) (G): + ∀L,V1,V2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 → + ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ⬈*[h] T2 → + ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈*[h] ⓑ[p,I]V2.T2. /4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. (* Inversion lemmas with context-sensitive ext rt-computation for terms *****) -lemma cpxs_inv_abst1 (h) (G): ∀p,L,V1,T1,U2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ⬈*[h] U2 → - ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ⬈*[h] T2 & - U2 = ⓛ[p]V2.T2. +lemma cpxs_inv_abst1 (h) (G): + ∀p,L,V1,T1,U2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ⬈*[h] U2 → + ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ⬈*[h] T2 & U2 = ⓛ[p]V2.T2. #h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ #U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct @@ -38,10 +39,9 @@ qed-. (* Basic_2A1: was: cpxs_inv_abbr1 *) lemma cpxs_inv_abbr1_dx (h) (p) (G) (L): - ∀V1,T1,U2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ⬈*[h] U2 → - ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & - U2 = ⓓ[p]V2.T2 - | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ. + ∀V1,T1,U2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ⬈*[h] U2 → + ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & U2 = ⓓ[p]V2.T2 + | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ. #h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ #U0 #U2 #_ #HU02 * * diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma index aebf01f07..8d9c5ee40 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma @@ -55,8 +55,9 @@ lemma lpr_cpr_conf (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (* Advanced inversion lemmas ************************************************) (* Note: there must be a proof suitable for lfpr *) -lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 → - ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2. +lemma cpcs_inv_abst_bi_sn (h) (G) (L): + ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 → + ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2. #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H #T #H1 #H2 elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct @@ -66,8 +67,9 @@ lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT /4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ qed-. -lemma cpcs_inv_abst_dx (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 → - ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW2❫ ⊢ T1 ⬌*[h] T2 & p1 = p2. +lemma cpcs_inv_abst_bi_dx (h) (G) (L): + ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 → + ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW2❫ ⊢ T1 ⬌*[h] T2 & p1 = p2. #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 -#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ +#HT12 elim (cpcs_inv_abst_bi_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 9ea5a2521..686676a94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -61,7 +61,7 @@ lemma cpg_inv_lref1_drops: ∀Rt,c,h,G,i,L,T2. ❪G,L❫ ⊢ #i ⬈[Rt,c,h] T2 ] * #cV #L #W #W2 #HKL #HW2 #HWV2 #H destruct lapply (lifts_trans … HWV2 … HVT2 ??) -V2 [3,6: |*: // ] #H - lapply (lifts_uni … H) -H #H +(* lapply (lifts_uni … H) -H #H *) (**) /4 width=8 by drops_drop, ex4_4_intro, or3_intro2, or3_intro1/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2A/grammar/aarity.ma index b980bc16a..835d8f837 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/grammar/aarity.ma @@ -46,7 +46,7 @@ lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥. ] qed-. -lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥. +lemma discr_apair_xy_y: ∀B,A. ②B. A = A → ⊥. #B #A elim A -A [ #H destruct | #Y #X #_ #IHX #H elim (destruct_apair_apair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *) diff --git a/matita/matita/contribs/lambdadelta/basic_2A/names.txt b/matita/matita/contribs/lambdadelta/basic_2A/names.txt new file mode 100644 index 000000000..25e865b6f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2A/names.txt @@ -0,0 +1,1919 @@ +aaa +aaa_abbr +aaa_abst +aaa_appl +aaa_cast +aaa_csx +aaa_da +aaa_fqu_conf +aaa_fqup_conf +aaa_fquq_conf +aaa_fqus_conf +aaa_fsb +aaa_fsba +aaa_ind_csx +aaa_ind_csx_alt +aaa_ind_csx_alt_aux +aaa_ind_csx_aux +aaa_ind_fpb +aaa_ind_fpb_aux +aaa_ind_fpbg +aaa_ind_fpbg_aux +aaa_inv_abbr +aaa_inv_abbr_aux +aaa_inv_abst +aaa_inv_abst_aux +aaa_inv_appl +aaa_inv_appl_aux +aaa_inv_cast +aaa_inv_cast_aux +aaa_inv_gref +aaa_inv_gref_aux +aaa_inv_lift +aaa_inv_lref +aaa_inv_lref_aux +aaa_inv_sort +aaa_inv_sort_aux +aaa_lift +aaa_lifts +aaa_lleq_conf +aaa_lref +aaa_lstas +aaa_mono +aaa_sort +aarity +AAtom +Abbr +Abst +acr +acr_aaa +acr_aaa_csubc_lifts +acr_abst +acr_gcr +APair +append +append_assoc +append_atom_sn +append_inj_dx +append_inj_sn +append_inv_pair_dx +append_inv_refl_dx +append_length +Appl +ApplDelta +ApplDelta_lift +ApplOmega1 +ApplOmega2 +ApplOmega3 +applv +applv_simple +at +at_ge +at_inv_cons +at_inv_cons_aux +at_inv_cons_ge +at_inv_cons_lt +at_inv_nil +at_inv_nil_aux +at_lt +at_mono +at_nil +bind2 +Bind2 +candidate +Cast +ceq +cfun +cir +cir_appl +cir_cnr +cir_gref +cir_ib2 +cir_inv_appl +cir_inv_bind +cir_inv_delta +cir_inv_flat +cir_inv_ib2 +cir_inv_lift +cir_inv_ri2 +cir_lift +cir_sort +cix +cix_appl +cix_cnx +cix_gref +cix_ib2 +cix_inv_appl +cix_inv_bind +cix_inv_cir +cix_inv_delta +cix_inv_flat +cix_inv_ib2 +cix_inv_lift +cix_inv_ri2 +cix_inv_sort +cix_lift +cix_lref +cix_sort +cnr +cnr_abst +cnr_appl_simple +cnr_dec +cnr_inv_abbr +cnr_inv_abst +cnr_inv_appl +cnr_inv_cir +cnr_inv_crr +cnr_inv_delta +cnr_inv_eps +cnr_inv_lift +cnr_inv_zeta +cnr_lift +cnr_lref_abst +cnr_lref_atom +cnr_lref_free +cnr_sort +cnx +cnx_abst +cnx_appl_simple +cnx_csx +cnx_dec +cnx_fwd_cnr +cnx_inv_abbr +cnx_inv_abst +cnx_inv_appl +cnx_inv_cix +cnx_inv_crx +cnx_inv_delta +cnx_inv_eps +cnx_inv_lift +cnx_inv_sort +cnx_inv_zeta +cnx_lift +cnx_lref_atom +cnx_lref_free +cnx_sort +cnx_sort_iter +CP0 +CP1 +CP2 +CP3 +cpc +cpc_conf +cpc_cpcs +cpc_fwd_cpr +cpc_refl +cpcs +cpcs_aaa_mono +cpcs_bind1 +cpcs_bind2 +cpcs_bind_dx +cpcs_bind_sn +cpcs_canc_dx +cpcs_canc_sn +cpcs_cpr_conf +cpcs_cpr_div +cpcs_cprs_conf +cpcs_cprs_div +cpcs_cprs_dx +cpcs_cprs_sn +cpcs_cprs_strap1 +cpcs_cprs_strap2 +cpcs_cpr_strap1 +cpcs_cpr_strap2 +cpcs_flat +cpcs_flat_dx_cpr_rev +cpcs_ind +cpcs_ind_dx +cpcs_inv_abst1 +cpcs_inv_abst2 +cpcs_inv_abst_dx +cpcs_inv_abst_sn +cpcs_inv_cprs +cpcs_inv_lift +cpcs_inv_sort +cpcs_inv_sort_abst +cpcs_lift +cpcs_refl +cpcs_scpes +cpcs_strap1 +cpcs_strap2 +cpcs_strip +cpcs_sym +cpcs_trans +cpc_sym +cpr +cpr_aaa_conf +cpr_ApplOmega_12 +cpr_ApplOmega_23 +cpr_atom +cpr_beta +cpr_bind +cpr_bind2 +cpr_conf +cpr_conf_lpr +cpr_conf_lpr_atom_atom +cpr_conf_lpr_atom_delta +cpr_conf_lpr_beta_beta +cpr_conf_lpr_bind_bind +cpr_conf_lpr_bind_zeta +cpr_conf_lpr_delta_delta +cpr_conf_lpr_eps_eps +cpr_conf_lpr_flat_beta +cpr_conf_lpr_flat_eps +cpr_conf_lpr_flat_flat +cpr_conf_lpr_flat_theta +cpr_conf_lpr_theta_theta +cpr_conf_lpr_zeta_zeta +cpr_cpcs_dx +cpr_cpcs_sn +cpr_cprs +cpr_cprs_conf_cpcs +cpr_cprs_div +cpr_cpx +cpr_delift +cpr_delta +cpr_div +cpre +cpre_mono +cpr_eps +cpr_flat +cpr_fpb +cpr_fpbq +cpr_fwd_bind1_minus +cpr_fwd_cir +cpr_inv_abbr1 +cpr_inv_abst1 +cpr_inv_appl1 +cpr_inv_appl1_simple +cpr_inv_atom1 +cpr_inv_atom1_aux +cpr_inv_bind1 +cpr_inv_bind1_aux +cpr_inv_cast1 +cpr_inv_flat1 +cpr_inv_flat1_aux +cpr_inv_gref1 +cpr_inv_lift1 +cpr_inv_lref1 +cpr_inv_sort1 +cpr_lift +cpr_llpx_sn_conf +cpr_lpr_fpbs +cpr_lpr_sta_fpbs +cpr_Omega_12 +cpr_Omega_21 +cpr_pair_sn +cpr_refl +cprs +cprs_aaa_conf +cprs_beta +cprs_beta_dx +cprs_beta_rc +cprs_bind +cprs_bind2 +cprs_bind2_dx +cprs_bind_dx +cprs_conf +cprs_conf_cpcs +cprs_cpr_conf_cpcs +cprs_cpr_div +cprs_cpxs +cprs_delta +cprs_div +cprs_eps +cprs_flat +cprs_flat_dx +cprs_flat_sn +cprs_fpbs +cprs_ind +cprs_ind_dx +cprs_inv_abbr1 +cprs_inv_abst +cprs_inv_abst1 +cprs_inv_appl1 +cprs_inv_cast1 +cprs_inv_cnr1 +cprs_inv_lift1 +cprs_inv_lref1 +cprs_inv_sort1 +cprs_lift +cprs_lpr_conf_dx +cprs_lpr_conf_sn +cprs_refl +cprs_scpds_div +cprs_strap1 +cprs_strap2 +cprs_strip +cprs_theta +cprs_theta_dx +cprs_theta_rc +cprs_trans +cprs_zeta +cpr_theta +cpr_zeta +cpx +cpx_aaa_conf +cpx_atom +cpx_beta +cpx_bind +cpx_bind2 +cpx_cpxs +cpx_ct +cpx_delift +cpx_delta +cpxe +cpx_eps +cpx_flat +cpx_frees_trans +cpx_fwd_bind1_minus +cpx_fwd_cix +cpx_inv_abbr1 +cpx_inv_abst1 +cpx_inv_appl1 +cpx_inv_appl1_simple +cpx_inv_atom1 +cpx_inv_atom1_aux +cpx_inv_bind1 +cpx_inv_bind1_aux +cpx_inv_cast1 +cpx_inv_flat1 +cpx_inv_flat1_aux +cpx_inv_gref1 +cpx_inv_lift1 +cpx_inv_lref1 +cpx_inv_lref1_ge +cpx_inv_sort1 +cpx_lift +cpx_lleq_conf +cpx_lleq_conf_dx +cpx_lleq_conf_sn +cpx_llpx_sn_conf +cpx_lpx_aaa_conf +cpx_pair_sn +cpx_refl +cpxs +cpxs_aaa_conf +cpxs_ApplOmega_13 +cpxs_beta +cpxs_beta_dx +cpxs_beta_rc +cpxs_bind +cpxs_bind2 +cpxs_bind2_dx +cpxs_bind_dx +cpxs_ct +cpxs_delta +cpxs_eps +cpxs_flat +cpxs_flat_dx +cpxs_flat_sn +cpxs_fpbg +cpxs_fpbs +cpxs_fpbs_trans +cpxs_fqup_fpbs +cpxs_fqus_fpbs +cpxs_fqus_lpxs_fpbs +cpxs_fwd_beta +cpxs_fwd_beta_vector +cpxs_fwd_cast +cpxs_fwd_cast_vector +cpxs_fwd_cnx +cpxs_fwd_cnx_vector +cpxs_fwd_delta +cpxs_fwd_delta_vector +cpxs_fwd_sort +cpxs_fwd_sort_vector +cpxs_fwd_theta +cpxs_fwd_theta_vector +cpxs_ind +cpxs_ind_dx +cpxs_inv_abbr1 +cpxs_inv_abst1 +cpxs_inv_appl1 +cpxs_inv_cast1 +cpxs_inv_cnx1 +cpxs_inv_lift1 +cpxs_inv_lref1 +cpxs_inv_sort1 +cpxs_lift +cpxs_lleq_conf +cpxs_lleq_conf_dx +cpxs_lleq_conf_sn +cpxs_neq_inv_step_sn +cpxs_pair_sn +cpxs_refl +cpxs_sort +cpxs_strap1 +cpxs_strap2 +cpx_st +cpxs_theta +cpxs_theta_dx +cpxs_theta_rc +cpxs_trans +cpxs_zeta +cpx_theta +cpx_zeta +cpy +cpy_atom +cpy_bind +cpy_conf_eq +cpy_conf_neq +cpy_cpys +cpy_flat +cpy_full +cpy_fwd_nlift2_ge +cpy_fwd_tw +cpy_fwd_up +cpy_inv_atom1 +cpy_inv_atom1_aux +cpy_inv_bind1 +cpy_inv_bind1_aux +cpy_inv_flat1 +cpy_inv_flat1_aux +cpy_inv_gref1 +cpy_inv_lift1_be +cpy_inv_lift1_be_up +cpy_inv_lift1_eq +cpy_inv_lift1_ge +cpy_inv_lift1_ge_up +cpy_inv_lift1_le +cpy_inv_lift1_le_up +cpy_inv_lref1 +cpy_inv_refl_O2 +cpy_inv_refl_O2_aux +cpy_inv_sort1 +cpy_lift_be +cpy_lift_ge +cpy_lift_le +cpy_refl +cpys +cpysa +cpysa_atom +cpysa_bind +cpysa_cpy_trans +cpysa_flat +cpysa_inv_cpys +cpys_antisym_eq +cpysa_refl +cpysa_subst +cpys_bind +cpys_conf_eq +cpys_conf_neq +cpys_cpysa +cpys_flat +cpys_fwd_tw +cpys_fwd_up +cpys_ind +cpys_ind_alt +cpys_ind_dx +cpys_inv_atom1 +cpys_inv_bind1 +cpys_inv_flat1 +cpys_inv_gref1 +cpys_inv_lift1_be +cpys_inv_lift1_be_up +cpys_inv_lift1_eq +cpys_inv_lift1_ge +cpys_inv_lift1_ge_up +cpys_inv_lift1_le +cpys_inv_lift1_le_up +cpys_inv_lift1_subst +cpys_inv_lift1_up +cpys_inv_lref1 +cpys_inv_lref1_drop +cpys_inv_lref1_Y2 +cpys_inv_refl_O2 +cpys_inv_SO2 +cpys_inv_sort1 +cpys_lift_be +cpys_lift_ge +cpys_lift_le +cpy_split_down +cpy_split_up +cpys_refl +cpys_split_up +cpys_strap1 +cpys_strap1_down +cpys_strap2 +cpys_strap2_down +cpys_strip_eq +cpys_strip_neq +cpys_subst +cpys_subst_Y2 +cpys_trans_down +cpys_trans_eq +cpy_subst +cpys_weak +cpys_weak_full +cpys_weak_top +cpy_trans_down +cpy_trans_ge +cpy_weak +cpy_weak_full +cpy_weak_top +crr +crr_appl_dx +crr_appl_sn +crr_beta +crr_crx +crr_delta +crr_ib2_dx +crr_ib2_sn +crr_inv_appl +crr_inv_appl_aux +crr_inv_gref +crr_inv_gref_aux +crr_inv_ib2 +crr_inv_ib2_aux +crr_inv_lift +crr_inv_lref +crr_inv_lref_aux +crr_inv_sort +crr_inv_sort_aux +crr_lift +crr_ri2 +crr_theta +crx +crx_appl_dx +crx_appl_sn +crx_beta +crx_delta +crx_ib2_dx +crx_ib2_sn +crx_inv_appl +crx_inv_appl_aux +crx_inv_gref +crx_inv_gref_aux +crx_inv_ib2 +crx_inv_ib2_aux +crx_inv_lift +crx_inv_lref +crx_inv_lref_aux +crx_inv_sort +crx_inv_sort_aux +crx_lift +crx_ri2 +crx_sort +crx_theta +csx +csxa +csx_abbr +csx_abst +csxa_cpxs_trans +csxa_csx +csxa_ind +csxa_intro +csxa_intro_aux +csxa_intro_cpx +csx_appl_beta +csx_appl_beta_aux +csx_appl_simple +csx_appl_simple_tsts +csx_appl_theta +csx_appl_theta_aux +csx_applv_beta +csx_applv_cast +csx_applv_cnx +csx_applv_delta +csx_applv_sort +csx_applv_theta +csx_cast +csx_cpre +csx_cpxe +csx_cpxs_trans +csx_cpx_trans +csx_csxa +csx_fpb_conf +csx_fpbs_conf +csx_fqu_conf +csx_fqup_conf +csx_fquq_conf +csx_fqus_conf +csx_fsb +csx_fsb_fpbs +csx_fwd_applv +csx_fwd_bind +csx_fwd_bind_dx +csx_fwd_bind_dx_aux +csx_fwd_flat +csx_fwd_flat_dx +csx_fwd_flat_dx_aux +csx_fwd_pair_sn +csx_fwd_pair_sn_aux +csx_gcp +csx_gcr +csx_ind +csx_ind_alt +csx_ind_fpb +csx_ind_fpbg +csx_intro +csx_intro_cpxs +csx_inv_lift +csx_inv_lref_bind +csx_lift +csx_lleq_conf +csx_lleq_trans +csx_lpx_conf +csx_lpxs_conf +csx_lref_bind +csx_lsx +csx_sort +csxv +csxv_inv_cons +d1_liftable_liftables +d1_liftables_liftables_all +da +da_bind +da_cpr_lpr +da_cpr_lpr_aux +da_cprs_lpr +da_cprs_lpr_aux +da_flat +da_inv_bind +da_inv_bind_aux +da_inv_flat +da_inv_flat_aux +da_inv_gref +da_inv_gref_aux +da_inv_lift +da_inv_lref +da_inv_lref_aux +da_inv_sort +da_inv_sort_aux +da_ldec +da_ldef +da_lift +da_lstas +da_mono +d_appendable_sn +da_scpds_lpr_aux +da_scpes_aux +da_sort +d_deliftable_sn +d_deliftable_sn_llstar +d_deliftable_sn_LTC +dedropable_sn +dedropable_sn_TC +deg_inv_prec +deg_inv_pred +deg_iter +deg_next_SO +deg_O +deg_SO +deg_SO_gt +deg_SO_inv_pos +deg_SO_inv_pos_aux +deg_SO_pos +deg_SO_refl +deg_SO_zero +Delta +Delta_lift +destruct_apair_apair_aux +destruct_lpair_lpair_aux +destruct_sort_sort_aux +destruct_tatom_tatom_aux +destruct_tpair_tpair_aux +discr_apair_xy_x +discr_apair_xy_y +discr_lpair_x_xy +discr_tpair_xy_x +discr_tpair_xy_y +d_liftable +d_liftable1 +d_liftable_llstar +d_liftable_LTC +d_liftables1 +d_liftables1_all +drop +dropable_dx +dropable_dx_TC +dropable_sn +dropable_sn_TC +drop_atom +drop_conf_be +drop_conf_div +drop_conf_ge +drop_conf_le +drop_conf_lt +drop_drop +drop_drop_lt +drop_FT +drop_fwd_be +drop_fwd_drop2 +drop_fwd_length +drop_fwd_length_eq1 +drop_fwd_length_eq2 +drop_fwd_length_ge +drop_fwd_length_le2 +drop_fwd_length_le4 +drop_fwd_length_le_ge +drop_fwd_length_le_le +drop_fwd_length_lt2 +drop_fwd_length_lt4 +drop_fwd_length_minus2 +drop_fwd_length_minus4 +drop_fwd_lw +drop_fwd_lw_lt +drop_fwd_rfw +drop_gen +drop_inv_atom1 +drop_inv_atom1_aux +drop_inv_drop1 +drop_inv_drop1_lt +drop_inv_FT +drop_inv_FT_aux +drop_inv_gen +drop_inv_length_eq +drop_inv_O1_gt +drop_inv_O1_pair1 +drop_inv_O1_pair1_aux +drop_inv_O1_pair2 +drop_inv_O2 +drop_inv_O2_aux +drop_inv_pair1 +drop_inv_refl +drop_inv_skip1 +drop_inv_skip1_aux +drop_inv_skip2 +drop_inv_skip2_aux +drop_inv_T +drop_lprs_trans +drop_lpr_trans +drop_lpxs_trans +drop_lpx_trans +drop_lsubc_trans +drop_mono +drop_O1_append_sn_le +drop_O1_append_sn_le_aux +drop_O1_eq +drop_O1_ex +drop_O1_ge +drop_O1_inj +drop_O1_inv_append1_ge +drop_O1_inv_append1_le +drop_O1_le +drop_O1_lt +drop_O1_pair +drop_pair +drop_refl +drop_refl_atom_O2 +drops +drops_cons +drops_drop_trans +drops_inv_cons +drops_inv_cons_aux +drops_inv_nil +drops_inv_nil_aux +drops_inv_skip2 +drop_skip +drop_skip_lt +drops_lsubc_trans +drops_nil +drop_split +drops_skip +drops_trans +drop_T +drop_trans_ge +drop_trans_ge_comm +drop_trans_le +drop_trans_lt +eq_aarity_dec +eq_bind2_dec +eq_false_inv_tpair_dx +eq_false_inv_tpair_sn +eq_flat2_dec +eq_genv_dec +eq_item0_dec +eq_item2_dec +eq_lenv_dec +eq_term_dec +flat2 +Flat2 +fleq +fleq_canc_dx +fleq_canc_sn +fleq_fpbg_trans +fleq_fpbq +fleq_fpbs +fleq_fpb_trans +fleq_intro +fleq_inv_gen +fleq_refl +fleq_sym +fleq_trans +fpb +fpb_cpx +fpb_fpbg +fpb_fpbg_trans +fpb_fpbq +fpb_fpbq_alt +fpb_fpbs +fpb_fpbsa_trans +fpb_fqu +fpbg +fpbg_fleq_trans +fpbg_fpbq_trans +fpbg_fpbs_trans +fpbg_fwd_fpbs +fpbg_refl +fpbg_trans +fpb_inv_fleq +fpb_lpx +fpbq +fpbqa +fpbq_aaa_conf +fpbqa_inv_fpbq +fpbq_cpx +fpbq_fpbg_trans +fpbq_fpbqa +fpbq_fpbs +fpbq_fquq +fpbq_ind_alt +fpbq_inv_fpb_alt +fpbq_lleq +fpbq_lpx +fpbq_refl +fpbs +fpbsa +fpbs_aaa_conf +fpbsa_inv_fpbs +fpbs_cpxs_trans +fpbs_cpx_trans_neq +fpbs_fpbg +fpbs_fpbg_trans +fpbs_fpbsa +fpbs_fpb_trans +fpbs_fqup_trans +fpbs_fqus_trans +fpbs_ind +fpbs_ind_dx +fpbs_intro_alt +fpbs_inv_alt +fpbs_lleq_trans +fpbs_lpxs_trans +fpbs_refl +fpbs_strap1 +fpbs_strap2 +fpbs_trans +fqu +fqu_bind_dx +fqu_cpr_trans_dx +fqu_cpr_trans_sn +fqu_cpxs_trans +fqu_cpxs_trans_neq +fqu_cpx_trans +fqu_cpx_trans_neq +fqu_drop +fqu_drop_lt +fqu_flat_dx +fqu_fqup +fqu_fquq +fqu_fwd_fw +fqu_fwd_length_lref1 +fqu_fwd_length_lref1_aux +fqu_inv_eq +fqu_inv_eq_aux +fqu_lpr_trans +fqu_lpx_trans +fqu_lref_O +fqu_lref_S_lt +fqup +fqu_pair_sn +fqup_ApplOmega_13 +fqup_bind_dx +fqup_bind_dx_flat_dx +fqup_cpxs_trans +fqup_cpxs_trans_neq +fqup_cpx_trans +fqup_cpx_trans_neq +fqup_drop +fqup_flat_dx +fqup_flat_dx_bind_dx +fqup_flat_dx_pair_sn +fqup_fpbg +fqup_fpbs +fqup_fqus +fqup_fqus_trans +fqup_fwd_fw +fqup_ind +fqup_ind_dx +fqup_inv_step_sn +fqup_lref +fqup_pair_sn +fqup_strap1 +fqup_strap2 +fqup_trans +fqup_wf_ind +fqup_wf_ind_eq +fquq +fquqa +fquqa_drop +fquqa_inv_fquq +fquqa_refl +fquq_bind_dx +fquq_cpr_trans_dx +fquq_cpr_trans_sn +fquq_cpxs_trans +fquq_cpxs_trans_neq +fquq_cpx_trans +fquq_cpx_trans_neq +fquq_drop +fquq_flat_dx +fquq_fquqa +fquq_fqus +fquq_fwd_fw +fquq_fwd_length_lref1 +fquq_fwd_length_lref1_aux +fquq_inv_gen +fquq_lpr_trans +fquq_lpx_trans +fquq_lref_O +fquq_lstas_trans +fquq_pair_sn +fquq_refl +fquq_sta_trans +fqus +fqus_cpxs_trans +fqus_cpxs_trans_neq +fqus_cpx_trans +fqus_cpx_trans_neq +fqus_drop +fqus_fpbs +fqus_fpbs_trans +fqus_fqup_trans +fqus_fwd_fw +fqus_ind +fqus_ind_dx +fqus_inv_gen +fqus_lpxs_fpbs +fqus_lstas_trans +fqus_refl +fqus_strap1 +fqus_strap1_fqu +fqus_strap2 +fqus_strap2_fqu +fqu_sta_trans +fqus_trans +fqu_wf_ind +frees +frees_append +frees_be +frees_bind_dx +frees_bind_dx_O +frees_bind_sn +frees_dec +frees_eq +frees_flat_dx +frees_flat_sn +frees_inv +frees_inv_append +frees_inv_append_aux +frees_inv_bind +frees_inv_bind_O +frees_inv_flat +frees_inv_gref +frees_inv_lift_be +frees_inv_lift_ge +frees_inv_lref +frees_inv_lref_free +frees_inv_lref_ge +frees_inv_lref_lt +frees_inv_lref_skip +frees_inv_sort +frees_lift_ge +frees_lref_be +frees_lref_eq +frees_lreq_conf +frees_S +frees_trans +frees_weak +fsb +fsba +fsba_fpbs_trans +fsba_ind_alt +fsba_intro +fsba_inv_fsb +fsb_fpbs_trans +fsb_fsba +fsb_ind_alt +fsb_ind_fpbg +fsb_intro +fsb_inv_csx +fw +fw_lpair_sn +fw_shift +fw_tpair_dx +fw_tpair_sn +gcp +gcp0_lifts +gcp2_lifts +gcp2_lifts_all +gcr +gcr_aaa +gcr_lift +gcr_lifts +genv +gget +gget_dec +gget_eq +gget_gt +gget_inv_eq +gget_inv_gt +gget_inv_lt +gget_inv_lt_aux +gget_lt +gget_mono +gget_total +GRef +ib2 +IH_da_cpr_lpr +IH_lstas_cpr_lpr +IH_snv_cpr_lpr +IH_snv_lstas +is_lift_dec +item0 +item2 +LAtom +lcosx +lcosx_drop_trans_lt +lcosx_inv_pair +lcosx_inv_succ +lcosx_inv_succ_aux +lcosx_O +lcosx_pair +lcosx_skip +lcosx_sort +length +length_inv_pos_dx +length_inv_pos_dx_ltail +length_inv_pos_sn +length_inv_pos_sn_ltail +length_inv_zero_dx +length_inv_zero_sn +lenv +lenv_ind_alt +lift +lift_bind +lift_conf_be +lift_conf_O1 +lift_div_be +lift_div_le +lift_flat +lift_fwd_pair1 +lift_fwd_pair2 +lift_fwd_tw +lift_gref +lift_inj +lift_inv_bind1 +lift_inv_bind1_aux +lift_inv_bind2 +lift_inv_bind2_aux +lift_inv_flat1 +lift_inv_flat1_aux +lift_inv_flat2 +lift_inv_flat2_aux +lift_inv_gref1 +lift_inv_gref1_aux +lift_inv_gref2 +lift_inv_gref2_aux +lift_inv_lref1 +lift_inv_lref1_aux +lift_inv_lref1_ge +lift_inv_lref1_lt +lift_inv_lref2 +lift_inv_lref2_aux +lift_inv_lref2_be +lift_inv_lref2_ge +lift_inv_lref2_lt +lift_inv_O2 +lift_inv_O2_aux +lift_inv_pair_xy_x +lift_inv_pair_xy_y +lift_inv_sort1 +lift_inv_sort1_aux +lift_inv_sort2 +lift_inv_sort2_aux +lift_lref_ge +lift_lref_ge_minus +lift_lref_ge_minus_eq +lift_lref_lt +lift_mono +lift_refl +lifts +lifts_applv +lifts_bind +lifts_cons +lifts_flat +lift_simple_dx +lift_simple_sn +lifts_inv_applv1 +lifts_inv_bind1 +lifts_inv_cons +lifts_inv_cons_aux +lifts_inv_flat1 +lifts_inv_gref1 +lifts_inv_lref1 +lifts_inv_nil +lifts_inv_nil_aux +lifts_inv_sort1 +lifts_lift_trans +lifts_lift_trans_le +lifts_nil +lift_sort +lift_split +lifts_simple_dx +lifts_simple_sn +lifts_total +lifts_trans +liftsv +liftsv_cons +liftsv_liftv_trans_le +liftsv_nil +lift_total +lift_trans_be +lift_trans_ge +lift_trans_le +liftv +liftv_cons +liftv_inv_cons1 +liftv_inv_cons1_aux +liftv_inv_nil1 +liftv_inv_nil1_aux +liftv_mono +liftv_nil +liftv_total +lleq +lleq_aaa_trans +lleq_bind +lleq_bind_O +lleq_bind_repl_O +lleq_bind_repl_SO +lleq_canc_dx +lleq_canc_sn +lleq_cpxs_trans +lleq_cpx_trans +lleq_dec +lleq_flat +lleq_fpbs +lleq_fpbs_trans +lleq_fpb_trans +lleq_fqup_trans +lleq_fquq_trans +lleq_fqus_trans +lleq_fqu_trans +lleq_free +lleq_fwd_bind_dx +lleq_fwd_bind_O_dx +lleq_fwd_bind_sn +lleq_fwd_drop_dx +lleq_fwd_drop_sn +lleq_fwd_flat_dx +lleq_fwd_flat_sn +lleq_fwd_length +lleq_fwd_lref +lleq_fwd_lref_dx +lleq_fwd_lref_sn +lleq_ge +lleq_ge_up +lleq_gref +lleq_ind +lleq_ind_alt_r +lleq_intro_alt +lleq_intro_alt_r +lleq_inv_alt +lleq_inv_alt_r +lleq_inv_bind +lleq_inv_bind_O +lleq_inv_flat +lleq_inv_lift_be +lleq_inv_lift_ge +lleq_inv_lift_le +lleq_inv_lref_ge +lleq_inv_lref_ge_bi +lleq_inv_lref_ge_dx +lleq_inv_lref_ge_sn +lleq_inv_S +lleq_lift_ge +lleq_lift_le +lleq_llpx_sn_conf +lleq_llpx_sn_trans +lleq_lpxs_trans +lleq_lpx_trans +lleq_lref +lleq_lreq_repl +lleq_lreq_trans +lleq_nlleq_trans +lleq_refl +lleq_skip +lleq_sort +lleq_sym +lleq_trans +lleq_transitive +lleq_Y +llor +llor_atom +llor_skip +llor_tail_cofrees +llor_tail_frees +llor_total +llpx_sn +llpx_sn_alt +llpx_sn_alt_inv_llpx_sn +llpx_sn_alt_r +llpx_sn_alt_r_bind +llpx_sn_alt_r_flat +llpx_sn_alt_r_free +llpx_sn_alt_r_fwd_length +llpx_sn_alt_r_fwd_lref +llpx_sn_alt_r_gref +llpx_sn_alt_r_ind_alt +llpx_sn_alt_r_intro +llpx_sn_alt_r_intro_alt +llpx_sn_alt_r_inv_alt +llpx_sn_alt_r_inv_bind +llpx_sn_alt_r_inv_flat +llpx_sn_alt_r_inv_lpx_sn +llpx_sn_alt_r_lref +llpx_sn_alt_r_skip +llpx_sn_alt_r_sort +llpx_sn_bind +llpx_sn_bind_O +llpx_sn_bind_repl_O +llpx_sn_bind_repl_SO +llpx_sn_co +llpx_sn_dec +llpx_sn_drop_conf_O +llpx_sn_drop_trans_O +llpx_sn_flat +llpx_sn_free +llpx_sn_frees_trans +llpx_sn_frees_trans_aux +llpx_sn_fwd_bind_dx +llpx_sn_fwd_bind_O_dx +llpx_sn_fwd_bind_sn +llpx_sn_fwd_drop_dx +llpx_sn_fwd_drop_sn +llpx_sn_fwd_flat_dx +llpx_sn_fwd_flat_sn +llpx_sn_fwd_length +llpx_sn_fwd_lref +llpx_sn_fwd_lref_aux +llpx_sn_fwd_lref_dx +llpx_sn_fwd_lref_sn +llpx_sn_fwd_pair_sn +llpx_sn_ge +llpx_sn_ge_up +llpx_sn_gref +llpx_sn_ind_alt_r +llpx_sn_intro_alt_r +llpx_sn_inv_alt_r +llpx_sn_inv_bind +llpx_sn_inv_bind_aux +llpx_sn_inv_bind_O +llpx_sn_inv_flat +llpx_sn_inv_flat_aux +llpx_sn_inv_lift_be +llpx_sn_inv_lift_ge +llpx_sn_inv_lift_le +llpx_sn_inv_lift_O +llpx_sn_inv_lref_ge_bi +llpx_sn_inv_lref_ge_dx +llpx_sn_inv_lref_ge_sn +llpx_sn_inv_S +llpx_sn_inv_S_aux +llpx_sn_lift_ge +llpx_sn_lift_le +llpx_sn_llor_dx +llpx_sn_llor_dx_sym +llpx_sn_llor_fwd_sn +llpx_sn_llpx_sn_alt +llpx_sn_lpx_sn_alt_r +llpx_sn_lref +llpx_sn_lrefl +llpx_sn_lreq_repl +llpx_sn_lreq_trans +llpx_sn_refl +llpx_sn_skip +llpx_sn_sort +llpx_sn_TC_pair_dx +llpx_sn_Y +LPair +lpair_ltail +lpr +lpr_aaa_conf +lpr_conf +lpr_cpcs_conf +lpr_cpcs_trans +lpr_cpr_conf +lpr_cpr_conf_dx +lpr_cpr_conf_sn +lpr_cprs_conf +lpr_cprs_trans +lpr_cpr_trans +lpr_drop_conf +lpr_drop_trans_O1 +lpr_fpb +lpr_fpbq +lpr_fwd_length +lpr_inv_atom1 +lpr_inv_atom2 +lpr_inv_pair1 +lpr_inv_pair2 +lpr_lprs +lpr_lpx +lpr_pair +lpr_refl +lprs +lprs_aaa_conf +lprs_conf +lprs_cpcs_trans +lprs_cpr_conf_dx +lprs_cpr_conf_sn +lprs_cprs_conf +lprs_cprs_conf_dx +lprs_cprs_conf_sn +lprs_cprs_trans +lprs_cpr_trans +lprs_drop_conf +lprs_drop_trans_O1 +lprs_fpbs +lprs_fwd_length +lprs_ind +lprs_ind_alt +lprs_ind_dx +lprs_inv_atom1 +lprs_inv_atom2 +lprs_inv_pair1 +lprs_inv_pair2 +lprs_lpxs +lprs_pair +lprs_pair2 +lprs_pair_refl +lprs_refl +lprs_strap1 +lprs_strap2 +lprs_strip +lprs_trans +lpx +lpx_aaa_conf +lpx_cpx_frees_trans +lpx_cpxs_trans +lpx_cpx_trans +lpx_drop_conf +lpx_drop_trans_O1 +lpx_fqup_trans +lpx_fquq_trans +lpx_fqus_trans +lpx_fqu_trans +lpx_frees_trans +lpx_fwd_length +lpx_inv_atom1 +lpx_inv_atom2 +lpx_inv_pair +lpx_inv_pair1 +lpx_inv_pair2 +lpx_lleq_fqup_trans +lpx_lleq_fquq_trans +lpx_lleq_fqus_trans +lpx_lleq_fqu_trans +lpx_lpxs +lpx_pair +lpx_refl +lpxs +lpxs_aaa_conf +lpxs_cpxs_trans +lpxs_cpx_trans +lpxs_drop_conf +lpxs_drop_trans_O1 +lpxs_fpbg +lpxs_fpbs +lpxs_fpbs_trans +lpxs_fqup_trans +lpxs_fquq_trans +lpxs_fqus_trans +lpxs_fwd_length +lpxs_ind +lpxs_ind_alt +lpxs_ind_dx +lpxs_inv_atom1 +lpxs_inv_atom2 +lpxs_inv_pair1 +lpxs_inv_pair2 +lpxs_lleq_fpbs +lpxs_lleq_fqup_trans +lpxs_lleq_fquq_trans +lpxs_lleq_fqus_trans +lpxs_lleq_fqu_trans +lpx_sn +lpx_sn_alt +lpx_sn_alt_atom +lpx_sn_alt_fwd_length +lpx_sn_alt_inv_atom1 +lpx_sn_alt_inv_atom2 +lpx_sn_alt_inv_lpx_sn +lpx_sn_alt_inv_pair1 +lpx_sn_alt_inv_pair2 +lpx_sn_alt_pair +lpx_sn_atom +lpx_sn_conf +lpx_sn_confluent +lpx_sn_deliftable_dropable +lpx_sn_dropable +lpx_sn_dropable_aux +lpx_sn_drop_conf +lpx_sn_drop_trans +lpx_sn_fwd_length +lpx_sn_intro_alt +lpx_sn_inv_alt +lpx_sn_inv_atom1 +lpx_sn_inv_atom1_aux +lpx_sn_inv_atom2 +lpx_sn_inv_atom2_aux +lpx_sn_inv_pair +lpx_sn_inv_pair1 +lpx_sn_inv_pair1_aux +lpx_sn_inv_pair2 +lpx_sn_inv_pair2_aux +lpx_sn_liftable_dedropable +lpxs_nlleq_inv_step_sn +lpx_sn_llpx_sn +lpx_sn_lpx_sn_alt +lpx_sn_LTC_TC_lpx_sn +lpx_sn_pair +lpx_sn_refl +lpx_sn_trans +lpx_sn_transitive +lpxs_pair +lpxs_pair2 +lpxs_pair_refl +lpxs_refl +lpxs_strap1 +lpxs_strap2 +lpxs_trans +LRef +lreq +lreq_atom +lreq_canc_dx +lreq_canc_sn +lreq_cpxs_trans +lreq_cpx_trans +lreq_drop_conf_be +lreq_drop_trans_be +lreq_frees_trans +lreq_fwd_length +lreq_inv_atom1 +lreq_inv_atom1_aux +lreq_inv_atom2 +lreq_inv_O_Y +lreq_inv_O_Y_aux +lreq_inv_pair +lreq_inv_pair1 +lreq_inv_pair1_aux +lreq_inv_pair2 +lreq_inv_succ +lreq_inv_succ1 +lreq_inv_succ1_aux +lreq_inv_succ2 +lreq_inv_zero1 +lreq_inv_zero1_aux +lreq_inv_zero2 +lreq_join +lreq_lleq_trans +lreq_llpx_sn_trans +lreq_lpxs_trans_lleq +lreq_lpxs_trans_lleq_aux +lreq_lpx_trans_lleq +lreq_lpx_trans_lleq_aux +lreq_O2 +lreq_pair +lreq_pair_lt +lreq_pair_O_Y +lreq_refl +lreq_succ +lreq_succ_lt +lreq_sym +lreq_trans +lreq_zero +lstas +lstas_aaa_conf +lstas_appl +lstas_bind +lstas_cast +lstas_conf +lstas_conf_le +lstas_correct +lstas_cpcs_lpr +lstas_cpr +lstas_cpr_aux +lstas_cpr_lpr +lstas_cpr_lpr_aux +lstas_cprs_lpr +lstas_cprs_lpr_aux +lstas_cpxs +lstas_da_conf +lstas_fpbg +lstas_fpbs +lstas_inv_appl1 +lstas_inv_appl1_aux +lstas_inv_bind1 +lstas_inv_bind1_aux +lstas_inv_cast1 +lstas_inv_cast1_aux +lstas_inv_da +lstas_inv_da_ge +lstas_inv_gref1 +lstas_inv_gref1_aux +lstas_inv_lift1 +lstas_inv_lref1 +lstas_inv_lref1_aux +lstas_inv_lref1_O +lstas_inv_lref1_S +lstas_inv_refl_pos +lstas_inv_sort1 +lstas_inv_sort1_aux +lstas_ldef +lstas_lift +lstas_llpx_sn_conf +lstas_lstas +lstas_mono +lstas_scpds +lstas_scpds_aux +lstas_scpds_trans +lstas_scpes_trans +lstas_sort +lstas_split +lstas_split_aux +lstas_succ +lstas_trans +lstas_zero +lsuba +lsuba_aaa_conf +lsuba_aaa_trans +lsuba_atom +lsuba_beta +lsuba_drop_O1_conf +lsuba_drop_O1_trans +lsuba_fwd_lsubr +lsuba_inv_atom1 +lsuba_inv_atom1_aux +lsuba_inv_atom2 +lsuba_inv_atom2_aux +lsuba_inv_pair1 +lsuba_inv_pair1_aux +lsuba_inv_pair2 +lsuba_inv_pair2_aux +lsuba_lsubc +lsuba_pair +lsuba_refl +lsuba_trans +lsubc +lsubc_atom +lsubc_beta +lsubc_drop_O1_trans +lsubc_fwd_lsubr +lsubc_inv_atom1 +lsubc_inv_atom1_aux +lsubc_inv_atom2 +lsubc_inv_atom2_aux +lsubc_inv_pair1 +lsubc_inv_pair1_aux +lsubc_inv_pair2 +lsubc_inv_pair2_aux +lsubc_pair +lsubc_refl +lsubd +lsubd_atom +lsubd_beta +lsubd_da_conf +lsubd_da_trans +lsubd_drop_O1_conf +lsubd_drop_O1_trans +lsubd_fwd_lsubr +lsubd_inv_atom1 +lsubd_inv_atom1_aux +lsubd_inv_atom2 +lsubd_inv_atom2_aux +lsubd_inv_pair1 +lsubd_inv_pair1_aux +lsubd_inv_pair2 +lsubd_inv_pair2_aux +lsubd_pair +lsubd_refl +lsubd_trans +lsubr +lsubr_atom +lsubr_beta +lsubr_cpcs_trans +lsubr_cprs_trans +lsubr_cpr_trans +lsubr_cpxs_trans +lsubr_cpx_trans +lsubr_fwd_drop2_abbr +lsubr_fwd_drop2_pair +lsubr_fwd_length +lsubr_inv_abbr2 +lsubr_inv_abbr2_aux +lsubr_inv_abst1 +lsubr_inv_abst1_aux +lsubr_inv_atom1 +lsubr_inv_atom1_aux +lsubr_inv_pair1 +lsubr_inv_pair1_aux +lsubr_pair +lsubr_refl +lsubr_trans +lsubsv +lsubsv_atom +lsubsv_beta +lsubsv_cpcs_trans +lsubsv_cprs_trans +lsubsv_drop_O1_conf +lsubsv_drop_O1_trans +lsubsv_fwd_lsuba +lsubsv_fwd_lsubd +lsubsv_fwd_lsubr +lsubsv_inv_atom1 +lsubsv_inv_atom1_aux +lsubsv_inv_atom2 +lsubsv_inv_atom2_aux +lsubsv_inv_pair1 +lsubsv_inv_pair1_aux +lsubsv_inv_pair2 +lsubsv_inv_pair2_aux +lsubsv_lstas_trans +lsubsv_pair +lsubsv_refl +lsubsv_scpds_trans +lsubsv_snv_trans +lsubsv_sta_trans +lsuby +lsuby_atom +lsuby_cpysa_trans +lsuby_cpys_trans +lsuby_cpy_trans +lsuby_drop_trans_be +lsuby_fwd_length +lsuby_inv_atom1 +lsuby_inv_atom1_aux +lsuby_inv_pair1 +lsuby_inv_pair1_aux +lsuby_inv_pair2 +lsuby_inv_pair2_aux +lsuby_inv_succ1 +lsuby_inv_succ1_aux +lsuby_inv_succ2 +lsuby_inv_succ2_aux +lsuby_inv_zero1 +lsuby_inv_zero1_aux +lsuby_inv_zero2 +lsuby_inv_zero2_aux +lsuby_O2 +lsuby_pair +lsuby_pair_lt +lsuby_pair_O_Y +lsuby_refl +lsuby_succ +lsuby_succ_lt +lsuby_sym +lsuby_trans +lsuby_zero +lsx +lsxa +lsxa_ind +lsxa_intro +lsxa_intro_aux +lsxa_intro_lpx +lsxa_inv_lsx +lsxa_lleq_trans +lsxa_lpxs_trans +lsx_atom +lsx_bind +lsx_bind_lpxs_aux +lsx_cpx_trans_lcosx +lsx_cpx_trans_O +lsx_flat +lsx_flat_lpxs +lsx_fwd_bind_dx +lsx_fwd_bind_sn +lsx_fwd_flat_dx +lsx_fwd_flat_sn +lsx_fwd_lref_be +lsx_fwd_pair_sn +lsx_ge +lsx_ge_up +lsx_gref +lsx_ind +lsx_ind_alt +lsx_intro +lsx_intro_alt +lsx_inv_bind +lsx_inv_flat +lsx_inv_lift_be +lsx_inv_lift_ge +lsx_inv_lift_le +lsx_lift_ge +lsx_lift_le +lsx_lleq_trans +lsx_lpxs_trans +lsx_lpx_trans +lsx_lref_be +lsx_lref_be_lpxs +lsx_lref_free +lsx_lref_skip +lsx_lreq_conf +lsx_lsxa +lsx_sort +ltail_length +lw +lw_pair +minuss +minuss_ge +minuss_inv_cons1 +minuss_inv_cons1_aux +minuss_inv_cons1_ge +minuss_inv_cons1_lt +minuss_inv_nil1 +minuss_inv_nil1_aux +minuss_lt +minuss_nil +mk_gcp +mk_gcr +mk_sd +mk_sh +nexts_dec +nexts_inj +nexts_le +nexts_lt +nf +nlift_bind_dx +nlift_bind_sn +nlift_flat_dx +nlift_flat_sn +nlift_inv_bind +nlift_inv_flat +nlift_inv_lref_be_SO +nlift_lref_be_SO +nlleq_inv_bind +nlleq_inv_bind_O +nlleq_inv_flat +nlleq_lleq_div +nllpx_sn_inv_bind +nllpx_sn_inv_bind_O +nllpx_sn_inv_flat +Omega1 +Omega2 +pluss +pluss_inv_cons2 +pluss_inv_nil2 +rfw +rfw_lpair_dx +rfw_lpair_sn +rfw_shift +rfw_tpair_dx +rfw_tpair_sn +ri2 +S1 +S2 +S3 +S4 +S5 +S6 +S7 +scpds +scpds_aaa_conf +scpds_conf_eq +scpds_cpr_lpr_aux +scpds_cprs_trans +scpds_div +scpds_fwd_cprs +scpds_fwd_cpxs +scpds_inv_abbr_abst +scpds_inv_abst1 +scpds_inv_lift1 +scpds_inv_lstas_eq +scpds_lift +scpds_strap1 +scpds_strap2 +scpes +scpes_aaa_mono +scpes_canc_dx +scpes_canc_sn +scpes_cpr_lpr_aux +scpes_inv_abst2 +scpes_inv_lstas_eq +scpes_le_aux +scpes_refl +scpes_sym +scpes_trans +sd +sd_d +sd_d_correct +sd_d_SS +sd_O +sd_SO +sh +sh_N +shnv +shnv_cast +shnv_inv_cast +shnv_inv_cast_aux +shnv_inv_snv +simple +simple_atom +simple_flat +simple_inv_bind +simple_inv_bind_aux +simple_inv_pair +simple_tsts_repl_dx +simple_tsts_repl_sn +snv +snv_appl +snv_bind +snv_cast +snv_cast_scpes +snv_cpr_lpr +snv_cpr_lpr_aux +snv_cprs_lpr +snv_cprs_lpr_aux +snv_extended +snv_fqu_conf +snv_fqup_conf +snv_fquq_conf +snv_fqus_conf +snv_fwd_aaa +snv_fwd_da +snv_fwd_fsb +snv_fwd_lstas +snv_inv_appl +snv_inv_appl_aux +snv_inv_bind +snv_inv_bind_aux +snv_inv_cast +snv_inv_cast_aux +snv_inv_gref +snv_inv_gref_aux +snv_inv_lift +snv_inv_lref +snv_inv_lref_aux +snv_lift +snv_lref +snv_lstas +snv_lstas_aux +snv_preserve +snv_restricted +snv_shnv_cast +snv_sort +Sort +sta_cprs_scpds +sta_cpx +sta_cpx_aux +sta_fpb +sta_fpbg +sta_fpbq +sta_fpbs +sta_ldec +TAtom +TC_lpx_sn_fwd_length +TC_lpx_sn_ind +TC_lpx_sn_inv_atom1 +TC_lpx_sn_inv_atom2 +TC_lpx_sn_inv_lpx_sn_LTC +TC_lpx_sn_inv_pair1 +TC_lpx_sn_inv_pair1_aux +TC_lpx_sn_inv_pair2 +TC_lpx_sn_pair +TC_lpx_sn_pair_refl +term +tir_atom +tix_lref +TPair +tpr_cpr +tprs_cprs +trr_inv_atom +trx_inv_atom +tsts +tsts_atom +tsts_canc_dx +tsts_canc_sn +tsts_dec +tsts_inv_atom1 +tsts_inv_atom1_aux +tsts_inv_atom2 +tsts_inv_atom2_aux +tsts_inv_bind_applv_simple +tsts_inv_pair1 +tsts_inv_pair1_aux +tsts_inv_pair2 +tsts_inv_pair2_aux +tsts_pair +tsts_refl +tsts_sym +tsts_trans +tw +tw_pos +unfold +unfold_bind +unfold_flat +unfold_lref +unfold_sort diff --git a/matita/matita/contribs/lambdadelta/basic_2A/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2A/static/lsuba.ma index c22a725d1..36f3c6f17 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/static/lsuba.ma @@ -67,7 +67,7 @@ fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L2 = ⋆ → L1 = ] qed-. -lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆. +lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆. /2 width=4 by lsuba_inv_atom2_aux/ qed-. fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → diff --git a/matita/matita/contribs/lambdadelta/names.txt b/matita/matita/contribs/lambdadelta/names.txt new file mode 100644 index 000000000..0448c5ad8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/names.txt @@ -0,0 +1,105 @@ +NAMING CONVENTIONS FOR METAVARIABLES + +A,B : arity +C : candidate of reducibility +D,E : RTM environment +F,G : global environment +H : reserved: transient premise +IH : reserved: inductive premise +I,J : item +K,L : local environment +M,N : reserved: future use +O : +P : relocation environment +Q : elimination predicate +R : generic predicate/relation +S : RTM stack +T,U,V,W: term +X,Y,Z : reserved: transient objet denoted by a capital letter + +a : applicability condition (true = restricted, false = general) +b : local dropping kind parameter (true = restricted, false = general) +c : rt-reduction count parameter +d : term degree +e : reserved: future use (\lambda\delta 3) +f,g : local reference transforming map +h : sort hierarchy parameter +i,j : local reference depth (de Bruijn's) +k,l : global reference level +m,n : iterations +o : sort degree parameter (origin) +p,q : binder polarity +r : +s : sort index +t,u : +v,w : local reference position level (de Bruijn's) (RTM) +x,y,z : reserved: transient objet denoted by a small letter + +NAMING CONVENTIONS FOR CONSTRUCTORS + +0: atomic +2: binary + +A: application to vector +E: empty list +F: boolean false +T: boolean true + +a: application +b: generic binder with one argument +d: abbreviation +f: generic flat with one argument +i: generic binder for local environments +l: typed abstraction +n: native type annotation +u: generic binder with zero argument +x: exclusion + +NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS + +- prefix and first letter + +b: bi contex-sensitive for local environments +c: contex-sensitive for terms +f: context-freee for closures +l: sn contex-sensitive for local environments +r: dx contex-sensitive for local environments +s: stratified (prefix) +t: context-free for terms + +- second letter + +e: reserved for generic entrywise extension +i: irreducible form +n: normal form +p: reflexive parallel transformation +q: sequential transformation +r: reducible form +s: strongly normalizing form + +- third letter + +b: (q)rst-reduction +c: conversion +d: decomposed rt-reduction +e: decomposed rt-conversion +g: counted rt-transition (generic) +m: semi-counted rt-transition (mixed) +q: restricted reduction +r: reduction +s: substitution +u: supclosure +w: reserved for generic pointwise extension +x: uncounted rt-transition (extended) +y: rt-substitution + +- forth letter (if present) + +c: proper single step (general) (successor) +e: reflexive transitive closure to normal form (evaluation) +g: proper multiple step (general) (greater) +p: non-reflexive transitive closure (plus) +q: reflexive closure (question) +r: proper multiple step (restricted) (restricted) +s: reflexive transitive closure (star) +u: proper single step (restricted) (unit) diff --git a/matita/matita/contribs/lambdadelta/static_2/names.txt b/matita/matita/contribs/lambdadelta/static_2/names.txt new file mode 100644 index 000000000..6af48b1ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/names.txt @@ -0,0 +1,1276 @@ +aaa +aaa_aaa_inv_appl +aaa_aaa_inv_cast +aaa_abbr +aaa_abst +aaa_appl +aaa_cast +aaa_dec +aaa_feqx_conf +aaa_fqu_conf +aaa_fqup_conf +aaa_fquq_conf +aaa_fqus_conf +aaa_inv_abbr +aaa_inv_abbr_aux +aaa_inv_abst +aaa_inv_abst_aux +aaa_inv_appl +aaa_inv_appl_aux +aaa_inv_cast +aaa_inv_cast_aux +aaa_inv_gref +aaa_inv_gref_aux +aaa_inv_lifts +aaa_inv_lref +aaa_inv_lref_aux +aaa_inv_lref_drops +aaa_inv_sort +aaa_inv_sort_aux +aaa_inv_zero +aaa_inv_zero_aux +aaa_lifts +aaa_lref +aaa_lref_drops +aaa_mono +aaa_pair_inv_lref +aaa_sort +aaa_teqx_conf_reqx +aaa_zero +aarity +AAtom +Abbr +Abst +abst_dec +ac +ac_eq +ac_eq_props +ac_le +acle +acle_eq_le +acle_eq_monotonic_le +acle_le_eq +acle_le_monotonic_le +acle_omega +acle_one +ac_le_props +acle_refl +acle_trans +ac_props +acr +acr_aaa +acr_aaa_csubc_lifts +acr_abst +acr_gcr +acr_lifts +ac_top +ac_top_props +APair +append +append_assoc +append_atom +append_atom_sn +append_bind +append_inj_dx +append_inj_length_dx +append_inj_length_sn +append_inj_sn +append_inv_atom3_sn +append_inv_bind3_sn +append_inv_pair_dx +append_inv_refl_dx +append_length +append_shift +Appl +applv +applv_cons +applv_nil +applv_simple +apply_top +bind +bind1 +bind2 +Bind2 +BPair +BUnit +bw +bw_pos +candidate +Cast +cdeq +cdeq_ext +ceq +ceq_ext +ceq_ext_inv_eq +ceq_ext_refl +ceq_ext_trans +ceq_inv_lift_sn +ceq_lift_sn +cext2 +cext2_co +cext2_d_liftable2_sn +cext2_sym +cfull +cfull_dec +cfull_lift_sn +cfun +co_dedropable_sn +co_dedropable_sn_CTC +co_dedropable_sn_ltc +co_dropable_dx +co_dropable_dx_CTC +co_dropable_dx_ltc +co_dropable_sn +co_dropable_sn_CTC +co_dropable_sn_ltc +CP0 +CP1 +CP2 +CP3 +d1_liftable_liftable_all +d2_deliftable_sn_CTC +d2_deliftable_sn_ltc +d2_liftable_sn_CTC +d2_liftable_sn_ltc +d_appendable_sn +d_deliftable1 +d_deliftable1_isuni +d_deliftable2_bi +d_deliftable2_sn +d_deliftable2_sn_bi +dedropable_sn +dedropable_sn_CTC +deg_inv_prec +deg_inv_pred +deg_iter +deg_next_SO +deg_O +deg_SO +deg_SO_gt +deg_SO_inv_succ +deg_SO_inv_succ_aux +deg_SO_refl +deg_SO_succ +deg_SO_zero +deliftable2_bi +deliftable2_dx +deliftable2_sn +deliftable2_sn_bi +deliftable2_sn_dx +destruct_apair_apair_aux +destruct_lbind_lbind_aux +destruct_sort_sort_aux +destruct_tatom_tatom_aux +destruct_tpair_tpair_aux +discr_apair_xy_x +discr_apair_xy_y +discr_lbind_x_xy +discr_lbind_xy_x +discr_tpair_xy_x +discr_tpair_xy_y +d_liftable1 +d_liftable1_all +d_liftable1_isuni +d_liftable2_bi +d_liftable2_sn +d_liftable2_sn_bi +dropable_dx +dropable_dx_CTC +dropable_sn +dropable_sn_CTC +drops +drops_after_fwd_drop2 +drops_atom +drops_atom2_sex_conf +drops_atom_F +drops_bind2_fwd_rfw +drops_conf +drops_conf_div +drops_conf_div_bind_isuni +drops_conf_div_fcla +drops_conf_div_isuni +drops_conf_skip1 +drops_drop +drops_eq_repl_back +drops_eq_repl_fwd +drops_F +drops_fcla_fwd +drops_fcla_fwd_le2 +drops_fcla_fwd_lt2 +drops_fcla_fwd_lt4 +drops_F_uni +drops_fwd_drop2 +drops_fwd_drop2_aux +drops_fwd_fcla +drops_fwd_fcla_le2 +drops_fwd_fcla_lt2 +drops_fwd_isfin +drops_fwd_isid +drops_fwd_length_eq1 +drops_fwd_length_eq2 +drops_fwd_length_le4 +drops_fwd_lw +drops_fwd_lw_lt +drops_gen +drops_inv_atom1 +drops_inv_atom1_aux +drops_inv_atom2 +drops_inv_bind1_isuni +drops_inv_bind2_isuni +drops_inv_bind2_isuni_next +drops_inv_drop1 +drops_inv_drop1_aux +drops_inv_F +drops_inv_gen +drops_inv_isuni +drops_inv_length_eq +drops_inv_skip1 +drops_inv_skip1_aux +drops_inv_skip2 +drops_inv_skip2_aux +drops_inv_succ +drops_inv_TF +drops_inv_TF_aux +drops_inv_uni +drops_inv_x_bind_xy +drops_isuni_ex +drops_isuni_fwd_drop2 +drops_ldec_dec +drops_lsubc_trans +drops_mono +drops_refl +drops_seq_trans_next +drops_sex_trans_next +drops_sex_trans_push +drops_skip +drops_split_div +drops_split_trans +drops_split_trans_bind2 +drops_TF +drops_tls_at +drops_trans +drops_trans_skip2 +eq_aarity_dec +eq_bind1_dec +eq_bind2_dec +eq_bind_dec +eq_false_inv_tpair_dx +eq_false_inv_tpair_sn +eq_flat2_dec +eq_genv_dec +eq_item0_dec +eq_item2_dec +eq_lenv_dec +eq_term_dec +ext2 +ext2_dec +ext2_inv_pair +ext2_inv_pair_dx +ext2_inv_pair_dx_aux +ext2_inv_pair_sn +ext2_inv_pair_sn_aux +ext2_inv_tc +ext2_inv_unit +ext2_inv_unit_dx +ext2_inv_unit_dx_aux +ext2_inv_unit_sn +ext2_inv_unit_sn_aux +ext2_pair +ext2_refl +ext2_sym +ext2_tc +ext2_tc_inj +ext2_tc_pair +ext2_tc_step +ext2_trans +ext2_unit +f_dedropable_sn +f_dropable_dx +f_dropable_sn +feqx +feqx_canc_dx +feqx_canc_sn +feqx_fqus_trans +feqx_intro_dx +feqx_intro_sn +feqx_inv_gen_dx +feqx_inv_gen_sn +feqx_refl +feqx_sym +feqx_tneqx_repl_dx +feqx_trans +flat2 +Flat2 +fold +fold_atom +fold_pair +fold_unit +fqu +fqu_bind_dx +fqu_clear +fqu_drop +fqu_flat_dx +fqu_fqup +fqu_fquq +fqu_fwd_fw +fqu_fwd_length_lref1 +fqu_fwd_length_lref1_aux +fqu_gref +fqu_inv_atom1 +fqu_inv_bind1 +fqu_inv_bind1_aux +fqu_inv_bind1_true +fqu_inv_flat1 +fqu_inv_flat1_aux +fqu_inv_gref1 +fqu_inv_gref1_aux +fqu_inv_gref1_bind +fqu_inv_lref1 +fqu_inv_lref1_aux +fqu_inv_lref1_bind +fqu_inv_sort1 +fqu_inv_sort1_aux +fqu_inv_sort1_bind +fqu_inv_teqx +fqu_inv_teqx_aux +fqu_inv_zero1_pair +fqu_lref_O +fqu_lref_S +fqup +fqu_pair_sn +fqup_bind_dx +fqup_bind_dx_flat_dx +fqup_clear +fqup_drops_strap1 +fqup_drops_succ +fqup_flat_dx +fqup_flat_dx_bind_dx +fqup_flat_dx_pair_sn +fqup_fqus +fqup_fqus_trans +fqup_fwd_fw +fqup_ind +fqup_ind_dx +fqup_inv_step_sn +fqup_lref +fqup_pair_sn +fqup_strap1 +fqup_strap2 +fqup_trans +fqup_wf_ind +fqup_wf_ind_eq +fqup_zeta +fquq +fquq_fqus +fquq_fwd_fw +fquq_fwd_length_lref1 +fquq_refl +fqus +fqus_drops +fqus_fqup_trans +fqus_fwd_fw +fqus_ind +fqus_ind_dx +fqus_inv_atom1 +fqus_inv_bind1 +fqus_inv_bind1_true +fqus_inv_flat1 +fqus_inv_fqup +fqus_inv_fqu_sn +fqus_inv_gref1 +fqus_inv_gref1_bind +fqus_inv_lref1 +fqus_inv_lref1_bind +fqus_inv_refl_atom3 +fqus_inv_sort1 +fqus_inv_sort1_bind +fqus_inv_zero1_pair +fqu_sort +fqus_refl +fqus_strap1 +fqus_strap1_fqu +fqus_strap2 +fqus_strap2_fqu +fqus_trans +fqu_teqx_conf +fqu_wf_ind +frees +frees_append_void +frees_atom +frees_atom_drops +frees_bind +frees_bind_void +frees_eq_repl_back +frees_eq_repl_fwd +frees_flat +frees_fwd_coafter +frees_fwd_isfin +frees_gref +frees_ind_void +frees_inv_append_void +frees_inv_append_void_aux +frees_inv_atom +frees_inv_atom_aux +frees_inv_bind +frees_inv_bind_aux +frees_inv_bind_void +frees_inv_drops_next +frees_inv_flat +frees_inv_flat_aux +frees_inv_gref +frees_inv_gref_aux +frees_inv_lifts +frees_inv_lifts_ex +frees_inv_lifts_SO +frees_inv_lref +frees_inv_lref_aux +frees_inv_lref_drops +frees_inv_pair +frees_inv_pair_aux +frees_inv_sort +frees_inv_sort_aux +frees_inv_unit +frees_inv_unit_aux +frees_lifts +frees_lifts_SO +frees_lref +frees_lref_push +frees_lref_pushs +frees_mono +frees_pair +frees_pair_drops +frees_req_conf +frees_reqx_conf +frees_sex_conf +frees_sort +frees_teqx_conf +frees_teqx_conf_reqx +frees_total +frees_unit +frees_unit_drops +fsge_rex_trans +fsle +fsle_bind +fsle_bind_dx_dx +fsle_bind_dx_sn +fsle_bind_eq +fsle_bind_sn_ge +fsle_flat +fsle_flat_dx_dx +fsle_flat_dx_sn +fsle_flat_sn +fsle_frees_trans +fsle_frees_trans_eq +fsle_fwd_pair_sn +fsle_gref +fsle_gref_bi +fsle_inv_frees_eq +fsle_inv_lifts_sn +fsle_lifts_dx +fsle_lifts_sn +fsle_lifts_SO +fsle_lifts_SO_sn +fsle_pair_bi +fsle_refl +fsle_shift +fsle_sort +fsle_sort_bi +fsle_trans_dx +fsle_trans_rc +fsle_trans_sn +fsle_unit_bi +f_transitive_next +fw +fw_clear +fw_lpair_sn +fw_shift +fw_tpair_dx +fw_tpair_sn +GAtom +gcp +gcp2_all +gcr +gcr_aaa +genv +glength +GPair +GRef +gw +gw_pair +is_apear_dec +is_lifts_dec +item0 +item2 +LAtom +LBind +length +length_atom +length_bind +length_inv_succ_dx +length_inv_succ_dx_ltail +length_inv_succ_sn +length_inv_succ_sn_ltail +length_inv_zero_dx +length_inv_zero_sn +lenv +lenv_case_tail +lenv_ind_tail +lex +lex_atom +lex_bind +lex_bind_refl_dx +lex_co +lex_conf +lex_confluent +lex_CTC +lex_CTC_ind_dx +lex_CTC_ind_sn +lex_CTC_inj +lex_CTC_step_dx +lex_CTC_step_sn +lex_dropable_dx +lex_dropable_sn +lex_drops_conf_pair +lex_drops_trans_pair +lex_fwd_length +lex_ind +lex_inv_atom_dx +lex_inv_atom_sn +lex_inv_bind_dx +lex_inv_bind_sn +lex_inv_CTC +lex_inv_pair +lex_inv_pair_dx +lex_inv_pair_sn +lex_inv_unit_dx +lex_inv_unit_sn +lex_liftable_dedropable_sn +lex_pair +lex_refl +lex_trans +lex_transitive +lex_unit +liftable2_bi +liftable2_dx +liftable2_sn +liftable2_sn_bi +liftable2_sn_dx +lifts +lifts_applv +liftsb +liftsb_conf +liftsb_div3 +liftsb_eq_repl_back +liftsb_fwd_bw +liftsb_fwd_isid +lifts_bind +liftsb_inj +liftsb_inv_pair_dx +liftsb_inv_pair_sn +liftsb_inv_unit_dx +liftsb_inv_unit_sn +liftsb_mono +liftsb_refl +liftsb_split_trans +liftsb_total +liftsb_trans +lifts_conf +lifts_div3 +lifts_div4 +lifts_div4_one +lifts_eq_repl_back +lifts_eq_repl_fwd +lifts_flat +lifts_fwd_isid +lifts_fwd_pair1 +lifts_fwd_pair2 +lifts_fwd_tw +lifts_gref +lifts_inj +lifts_inv_applv1 +lifts_inv_applv2 +lifts_inv_atom1 +lifts_inv_atom2 +lifts_inv_bind1 +lifts_inv_bind1_aux +lifts_inv_bind2 +lifts_inv_bind2_aux +lifts_inv_flat1 +lifts_inv_flat1_aux +lifts_inv_flat2 +lifts_inv_flat2_aux +lifts_inv_gref1 +lifts_inv_gref1_aux +lifts_inv_gref2 +lifts_inv_gref2_aux +lifts_inv_lref1 +lifts_inv_lref1_aux +lifts_inv_lref1_uni +lifts_inv_lref2 +lifts_inv_lref2_aux +lifts_inv_lref2_uni +lifts_inv_lref2_uni_ge +lifts_inv_lref2_uni_lt +lifts_inv_pair_xy_x +lifts_inv_pair_xy_y +lifts_inv_push_succ_sn +lifts_inv_push_zero_sn +lifts_inv_sort1 +lifts_inv_sort1_aux +lifts_inv_sort2 +lifts_inv_sort2_aux +lifts_lref +lifts_lref_ge +lifts_lref_ge_minus +lifts_lref_lt +lifts_lref_uni +lifts_mono +lifts_push_lref +lifts_push_zero +lifts_refl +lifts_simple_dx +lifts_simple_sn +lifts_sort +lifts_split_div +lifts_split_trans +lifts_total +lifts_trans +lifts_trans4_one +lifts_trans_uni +lifts_uni +liftsv +liftsv_cons +liftsv_inj +liftsv_inv_cons1 +liftsv_inv_cons1_aux +liftsv_inv_cons2 +liftsv_inv_cons2_aux +liftsv_inv_nil1 +liftsv_inv_nil1_aux +liftsv_inv_nil2 +liftsv_inv_nil2_aux +liftsv_mono +liftsv_nil +liftsv_split_trans +liftsv_total +liftsv_trans +LRef +lsuba +lsuba_aaa_conf +lsuba_aaa_trans +lsuba_atom +lsuba_beta +lsuba_bind +lsuba_drops_conf_isuni +lsuba_drops_trans_isuni +lsuba_fwd_lsubr +lsuba_inv_atom1 +lsuba_inv_atom1_aux +lsuba_inv_atom2 +lsuba_inv_atom2_aux +lsuba_inv_bind1 +lsuba_inv_bind1_aux +lsuba_inv_bind2 +lsuba_inv_bind2_aux +lsuba_lsubc +lsuba_refl +lsuba_trans +lsubc +lsubc_atom +lsubc_beta +lsubc_bind +lsubc_drops_trans_isuni +lsubc_fwd_lsubr +lsubc_inv_atom1 +lsubc_inv_atom1_aux +lsubc_inv_atom2 +lsubc_inv_atom2_aux +lsubc_inv_bind1 +lsubc_inv_bind1_aux +lsubc_inv_bind2 +lsubc_inv_bind2_aux +lsubc_refl +lsubf +lsubf_atom +lsubf_beta +lsubf_beta_tl_dx +lsubf_bind +lsubf_bind_tl_dx +lsubf_eq_repl_back1 +lsubf_eq_repl_back2 +lsubf_eq_repl_fwd1 +lsubf_eq_repl_fwd2 +lsubf_frees_trans +lsubf_fwd_bind_tl +lsubf_fwd_isid_dx +lsubf_fwd_isid_sn +lsubf_fwd_lsubr_isdiv +lsubf_fwd_sle +lsubf_inv_atom +lsubf_inv_atom1 +lsubf_inv_atom1_aux +lsubf_inv_atom2 +lsubf_inv_atom2_aux +lsubf_inv_beta_sn +lsubf_inv_bind_sn +lsubf_inv_pair1 +lsubf_inv_pair1_aux +lsubf_inv_pair2 +lsubf_inv_pair2_aux +lsubf_inv_push1 +lsubf_inv_push1_aux +lsubf_inv_push2 +lsubf_inv_push2_aux +lsubf_inv_push_sn +lsubf_inv_refl +lsubf_inv_sor_dx +lsubf_inv_unit1 +lsubf_inv_unit1_aux +lsubf_inv_unit2 +lsubf_inv_unit2_aux +lsubf_inv_unit_sn +lsubf_push +lsubf_refl +lsubf_refl_eq +lsubf_sor +lsubf_unit +lsubr +lsubr_atom +lsubr_beta +lsubr_bind +lsubr_fwd_bind1 +lsubr_fwd_bind2 +lsubr_fwd_drops2_abbr +lsubr_fwd_drops2_bind +lsubr_fwd_length +lsubr_inv_abbr2 +lsubr_inv_abst1 +lsubr_inv_abst2 +lsubr_inv_atom1 +lsubr_inv_atom1_aux +lsubr_inv_atom2 +lsubr_inv_atom2_aux +lsubr_inv_bind1 +lsubr_inv_bind1_aux +lsubr_inv_bind2 +lsubr_inv_bind2_aux +lsubr_inv_pair2 +lsubr_inv_unit1 +lsubr_inv_unit2 +lsubr_lsubf +lsubr_lsubf_isid +lsubr_refl +lsubr_trans +lsubr_unit +ltail_length +lveq +lveq_atom +lveq_bind +lveq_fwd_abst_bind_length_le +lveq_fwd_bind_abst_length_le +lveq_fwd_gen +lveq_fwd_length +lveq_fwd_length_eq +lveq_fwd_length_le_dx +lveq_fwd_length_le_sn +lveq_fwd_length_minus +lveq_fwd_length_plus +lveq_fwd_pair_dx +lveq_fwd_pair_sn +lveq_inj +lveq_inj_length +lveq_inj_void_dx_le +lveq_inj_void_sn_ge +lveq_inv_atom_atom +lveq_inv_atom_bind +lveq_inv_bind +lveq_inv_bind_atom +lveq_inv_bind_O +lveq_inv_pair_pair +lveq_inv_succ +lveq_inv_succ_aux +lveq_inv_succ_dx +lveq_inv_succ_sn +lveq_inv_succ_sn_aux +lveq_inv_void_dx_length +lveq_inv_void_sn_length +lveq_inv_void_succ_dx +lveq_inv_void_succ_sn +lveq_inv_zero +lveq_inv_zero_aux +lveq_length_eq +lveq_length_fwd_dx +lveq_length_fwd_sn +lveq_refl +lveq_sym +lveq_void_dx +lveq_void_sn +lw +lw_bind +mk_ac +mk_ac_props +mk_gcp +mk_gcr +mk_sd +mk_sd_props +mk_sh +mk_sh_acyclic +mk_sh_decidable +mk_sh_lt +nexts_le +nexts_lt +nf +R_confluent2_rex +req +req_feqx_trans +req_fsle_comp +req_fwd_rex +req_inv_bind +req_inv_flat +req_inv_lifts_bi +req_inv_lref_bind_dx +req_inv_lref_bind_sn +req_inv_zero_pair_dx +req_inv_zero_pair_sn +req_refl +req_reqx +req_reqx_trans +req_rex_trans +req_transitive +reqx +reqx_atom +reqx_bind +reqx_bind_repl_dx +reqx_bind_void +reqx_canc_dx +reqx_canc_sn +reqx_dec +reqx_flat +reqx_fqup_trans +reqx_fquq_trans +reqx_fqus_trans +reqx_fqu_trans +reqx_fsge_comp +reqx_fwd_bind_dx +reqx_fwd_bind_dx_void +reqx_fwd_dx +reqx_fwd_flat_dx +reqx_fwd_length +reqx_fwd_pair_sn +reqx_fwd_zero_pair +reqx_gref +reqx_gref_length +reqx_inv_atom_dx +reqx_inv_atom_sn +reqx_inv_bind +reqx_inv_bind_void +reqx_inv_flat +reqx_inv_lifts_bi +reqx_inv_lifts_dx +reqx_inv_lifts_sn +reqx_inv_lref +reqx_inv_lref_bind_dx +reqx_inv_lref_bind_sn +reqx_inv_lref_pair_bi +reqx_inv_lref_pair_dx +reqx_inv_lref_pair_sn +reqx_inv_zero +reqx_inv_zero_pair_dx +reqx_inv_zero_pair_sn +reqx_lifts_bi +reqx_lifts_sn +reqx_lref +reqx_pair +reqx_pair_refl +reqx_refl +reqx_repl +reqx_rneqx_trans +reqx_sort +reqx_sort_length +reqx_sym +reqx_trans +reqx_unit +reqx_unit_length +rex +rex_atom +rex_bind +rex_bind_dx_split +rex_bind_dx_split_void +rex_bind_repl_dx +rex_bind_void +rex_co +rex_conf +rex_confluent +rex_dec +rex_dropable_dx +rex_dropable_sn +rex_flat +rex_flat_dx_split +rex_fsge_compatible +rex_fsle_compatible +rex_fwd_bind_dx +rex_fwd_bind_dx_void +rex_fwd_dx +rex_fwd_flat_dx +rex_fwd_length +rex_fwd_pair_sn +rex_fwd_zero_pair +rex_gref +rex_gref_length +rex_inv_atom_dx +rex_inv_atom_sn +rex_inv_bind +rex_inv_bind_void +rex_inv_flat +rex_inv_frees +rex_inv_gref +rex_inv_gref_bind_dx +rex_inv_gref_bind_sn +rex_inv_lex_req +rex_inv_lifts_bi +rex_inv_lref +rex_inv_lref_bind_dx +rex_inv_lref_bind_sn +rex_inv_lref_pair_bi +rex_inv_lref_pair_dx +rex_inv_lref_pair_sn +rex_inv_lref_unit_dx +rex_inv_lref_unit_sn +rex_inv_sort +rex_inv_sort_bind_dx +rex_inv_sort_bind_sn +rex_inv_zero +rex_inv_zero_length +rex_inv_zero_pair_dx +rex_inv_zero_pair_sn +rex_inv_zero_unit_dx +rex_inv_zero_unit_sn +rex_isid +rex_lex +rex_liftable_dedropable_sn +rex_lifts_bi +rex_lref +rex_pair +rex_pair_refl +rex_pair_sn_split +rex_refl +rexs +rexs_atom +rexs_co +rexs_fwd_bind_dx +rexs_fwd_bind_dx_void +rexs_fwd_flat_dx +rexs_fwd_length +rexs_fwd_pair_sn +rexs_gref +rexs_ind_dx +rexs_ind_sn +rexs_inv_atom_dx +rexs_inv_atom_sn +rexs_inv_bind +rexs_inv_bind_void +rexs_inv_flat +rexs_inv_gref +rexs_inv_gref_bind_dx +rexs_inv_gref_bind_sn +rexs_inv_lex_req +rexs_inv_sort +rexs_inv_sort_bind_dx +rexs_inv_sort_bind_sn +rexs_lex +rexs_lex_req +rexs_lref +rex_sort +rex_sort_length +rexs_pair +rexs_pair_refl +rexs_refl +rexs_sort +rexs_step_dx +rexs_step_sn +rexs_sym +rexs_tc +rexs_trans +rexs_unit +rex_sym +rex_trans_fsle +rex_transitive +rex_trans_next +rex_unit +rex_unit_length +rex_unit_sn +R_fsge_compatible +rfw +rfw_clear +rfw_lpair_dx +rfw_lpair_sn +rfw_shift +rfw_tpair_dx +rfw_tpair_sn +rneqx_inv_bind +rneqx_inv_bind_void +rneqx_inv_flat +rneqx_reqx_canc_dx +rneqx_reqx_div +rnex_inv_bind +rnex_inv_bind_void +rnex_inv_flat +R_pw_confluent2_sex +S1 +S2 +S3 +S5 +S6 +S7 +sd +sd_d +sd_d_correct +sd_d_props +sd_d_SS +sd_O +sd_O_props +sd_props +sd_SO +sd_SO_props +seq +seq_canc_dx +seq_canc_sn +seq_co_dedropable_sn +seq_co_dropable_dx +seq_co_dropable_sn +seq_drops_conf_next +seq_drops_trans_next +seq_eq_repl_back +seq_eq_repl_fwd +seq_fwd_length +seq_inv_atom1 +seq_inv_atom2 +seq_inv_next +seq_inv_next1 +seq_inv_next2 +seq_inv_push +seq_inv_push1 +seq_inv_push2 +seq_inv_tl +seq_join +seq_meet +seq_refl +seq_sym +seq_trans +sex +sex_atom +sex_canc_dx +sex_canc_sn +sex_co +sex_co_dropable_dx +sex_co_dropable_sn +sex_co_isid +sex_conf +sex_dec +sex_dropable_dx_aux +sex_drops_conf_next +sex_drops_conf_push +sex_drops_trans_next +sex_drops_trans_push +sex_eq_repl_back +sex_eq_repl_fwd +sex_fwd_bind +sex_fwd_length +sex_inv_atom1 +sex_inv_atom1_aux +sex_inv_atom2 +sex_inv_atom2_aux +sex_inv_next +sex_inv_next1 +sex_inv_next1_aux +sex_inv_next2 +sex_inv_next2_aux +sex_inv_push +sex_inv_push1 +sex_inv_push1_aux +sex_inv_push2 +sex_inv_push2_aux +sex_inv_tc_dx +sex_inv_tc_sn +sex_inv_tl +sex_join +sex_length_cfull +sex_length_isid +sex_liftable_co_dedropable_bi +sex_liftable_co_dedropable_sn +sex_meet +sex_next +sex_pair_repl +sex_push +sex_refl +sex_sdj +sex_sdj_split +sex_sle_split +sex_sym +sex_tc_dx +sex_tc_inj_dx +sex_tc_inj_sn +sex_tc_next +sex_tc_next_dx +sex_tc_next_sn +sex_tc_push +sex_tc_push_dx +sex_tc_push_sn +sex_tc_refl +sex_tc_step_dx +sex_trans +sex_trans_gen +sex_trans_id_cfull +sex_transitive +sh +sh_acyclic +sh_decidable +sh_lt +sh_lt_acyclic +sh_lt_dec +sh_lt_nexts_inv_lt +simple +simple_atom +simple_dec_ex +simple_flat +simple_inv_bind +simple_inv_bind_aux +simple_inv_pair +simple_teqo_repl_dx +simple_teqo_repl_sn +sle_seq_trans +sle_sex_conf +sle_sex_trans +Sort +s_rs_transitive_isid +s_rs_transitive_lex_inv_isid +TAtom +tc_f_dedropable_sn +tc_f_dropable_dx +tc_f_dropable_sn +teqo +teqo_canc_dx +teqo_canc_sn +teqo_dec +teqo_gref +teqo_inv_applv_bind_simple +teqo_inv_gref1 +teqo_inv_gref1_aux +teqo_inv_lifts_bi +teqo_inv_lref1 +teqo_inv_lref1_aux +teqo_inv_pair +teqo_inv_pair1 +teqo_inv_pair1_aux +teqo_inv_pair2 +teqo_inv_pair2_aux +teqo_inv_sort1 +teqo_inv_sort1_aux +teqo_lifts_bi +teqo_lifts_dx +teqo_lifts_sn +teqo_lref +teqo_pair +teqo_refl +teqo_sort +teqo_sym +teqo_trans +teqx +teqx_canc_dx +teqx_canc_sn +teqx_dec +teqx_ext +teqx_feqx +teqx_fqup_trans +teqx_fquq_trans +teqx_fqus_trans +teqx_fqu_trans +teqx_fwd_atom1 +teqx_gref +teqx_inv_gref1 +teqx_inv_gref1_aux +teqx_inv_lifts_bi +teqx_inv_lifts_dx +teqx_inv_lifts_sn +teqx_inv_lref1 +teqx_inv_lref1_aux +teqx_inv_pair +teqx_inv_pair1 +teqx_inv_pair1_aux +teqx_inv_pair2 +teqx_inv_pair_xy_x +teqx_inv_pair_xy_y +teqx_inv_sort1 +teqx_inv_sort1_aux +teqx_inv_sort2 +teqx_lifts_bi +teqx_lifts_dx +teqx_lifts_inv_pair_sn +teqx_lifts_sn +teqx_lref +teqx_pair +teqx_refl +teqx_repl +teqx_reqx_conf +teqx_reqx_div +teqx_rex_conf +teqx_rex_div +teqx_sort +teqx_sym +teqx_teqo +teqx_tneqx_trans +teqx_trans +teqx_tweq +term +tneqx_inv_pair +tneqx_teqx_canc_dx +TPair +tw +tweq +tweq_abbr +tweq_abbr_neg +tweq_abbr_pos +tweq_abst +tweq_appl +tweq_canc_dx +tweq_canc_sn +tweq_cast +tweq_dec +tweq_fwd_pair_bi +tweq_fwd_pair_sn +tweq_gref +tweq_inv_abbr_neg_sn +tweq_inv_abbr_pos_bi +tweq_inv_abbr_pos_sn +tweq_inv_abbr_pos_x_lifts_y_y +tweq_inv_abbr_sn +tweq_inv_abbr_sn_aux +tweq_inv_abst_sn +tweq_inv_abst_sn_aux +tweq_inv_appl_bi +tweq_inv_appl_sn +tweq_inv_appl_sn_aux +tweq_inv_cast_bi +tweq_inv_cast_sn +tweq_inv_cast_sn_aux +tweq_inv_cast_xy_y +tweq_inv_gref_sn +tweq_inv_gref_sn_aux +tweq_inv_lifts_bi +tweq_inv_lref_sn +tweq_inv_lref_sn_aux +tweq_inv_sort_sn +tweq_inv_sort_sn_aux +tweq_lifts_bi +tweq_lifts_dx +tweq_lifts_sn +tweq_lref +tweq_refl +tweq_repl +tweq_simple_trans +tweq_sort +tweq_sym +tweq_trans +tw_le_pair_dx +tw_pos +Void diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma index ee9394a5b..dd8ee277c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma @@ -59,8 +59,9 @@ theorem drops_trans: ∀b1,f1,L1,L. ⇩*[b1,f1] L1 ≘ L → ] qed-. -theorem drops_conf_div: ∀f1,L,K. ⇩*[Ⓣ,f1] L ≘ K → ∀f2. ⇩*[Ⓣ,f2] L ≘ K → - 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2. +theorem drops_conf_div_isuni: + ∀f1,L,K. ⇩*[Ⓣ,f1] L ≘ K → ∀f2. ⇩*[Ⓣ,f2] L ≘ K → + 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2. #f1 #L #K #H elim H -f1 -L -K [ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2 /3 width=1 by isid_inv_eq_repl/ @@ -127,13 +128,14 @@ lapply (drops_trans … H1 … H2 … Hf) -L -Hf qed-. (* Basic_2A1: includes: drops_conf_div *) -lemma drops_conf_div_bind: ∀f1,f2,I1,I2,L,K. - ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] → - 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2. +lemma drops_conf_div_bind_isuni: + ∀f1,f2,I1,I2,L,K. + ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] → + 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2. #f1 #f2 #I1 #I2 #L #K #Hf1 #Hf2 #HU1 #HU2 lapply (drops_isuni_fwd_drop2 … Hf1) // #H1 lapply (drops_isuni_fwd_drop2 … Hf2) // #H2 -lapply (drops_conf_div … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H +lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12 lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0 lapply (drops_mono … H0 … Hf2) -L #H diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma index 196d0654c..466275aad 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma @@ -19,7 +19,7 @@ include "static_2/static/feqx.ma". (* Properties with syntactic equivalence on referred entries ****************) -lemma req_reqx_trans: ∀L1,L,T1. L1 ≡[T1] L → +lemma req_feqx_trans: ∀L1,L,T1. L1 ≡[T1] L → ∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. #L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma index 34267b7d6..242c3d52c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma @@ -31,7 +31,7 @@ lemma fsle_shift: ∀L1,L2. |L1| = |L2| → #L1 #L2 #H1L #I #T1 #T2 #V * #n #m #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct -lapply (lveq_inv_bind … H2L) -H2L #HL +lapply (lveq_inv_bind_O … H2L) -H2L #HL elim (frees_total L2 V) #g1 #Hg1 elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ lapply (sor_inv_sle_dx … Hg) #H0g diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma index fd30febbf..54b6aa1cb 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma @@ -67,7 +67,7 @@ fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L2 = ⋆ → L1 = ] qed-. -lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆. +lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆. /2 width=4 by lsuba_inv_atom2_aux/ qed-. fact lsuba_inv_bind2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2. L2 = K2.ⓘ[I] → diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma index 776affc1c..e8d0343a7 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma @@ -96,7 +96,7 @@ lemma lveq_inv_succ: ∀L1,L2,n1,n2. L1 ≋ⓧ*[↑n1,↑n2] L2 → ⊥. (* Advanced inversion lemmas ************************************************) -lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2. +lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2. #I1 #I2 #K1 #K2 #H elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct // qed-. -- 2.39.2