| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (646 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (312 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (102 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
Global Index
A
Acc_ind_dep [lemma, in Undecidability.MarkovPost]All [constructor, in Undecidability.FOL]
AllE [constructor, in Undecidability.Deduction]
AllI [constructor, in Undecidability.Deduction]
and_dec [instance, in Undecidability.Prelim]
appCtx [lemma, in Undecidability.BPCP_CND]
app_equi_proper [instance, in Undecidability.Prelim]
app_incl_proper [instance, in Undecidability.Prelim]
app_incl_R [lemma, in Undecidability.Prelim]
app_incl_l [lemma, in Undecidability.Prelim]
app_sub [lemma, in Undecidability.Semantics]
app1 [lemma, in Undecidability.BPCP_CND]
app2 [lemma, in Undecidability.BPCP_CND]
app3 [lemma, in Undecidability.BPCP_CND]
B
bool_eq_dec [instance, in Undecidability.Prelim]bool_dec [instance, in Undecidability.Prelim]
bool_Prop_false [lemma, in Undecidability.Prelim]
bool_Prop_true [lemma, in Undecidability.Prelim]
BPCP [inductive, in Undecidability.PCP]
BPCP_ksatis [lemma, in Undecidability.BPCP_IFOL]
BPCP_kvalid [lemma, in Undecidability.BPCP_IFOL]
BPCP_kprv [lemma, in Undecidability.BPCP_IFOL]
BPCP_derivable [lemma, in Undecidability.PCP]
BPCP_satis [lemma, in Undecidability.BPCP_FOL]
BPCP_prv [lemma, in Undecidability.BPCP_FOL]
BPCP_prv' [lemma, in Undecidability.BPCP_FOL]
BPCP_valid [lemma, in Undecidability.BPCP_FOL]
BPCP_CND [lemma, in Undecidability.BPCP_CND]
BPCP_to_CND [lemma, in Undecidability.BPCP_CND]
BPCP_CND.R [variable, in Undecidability.BPCP_CND]
BPCP_CND [section, in Undecidability.BPCP_CND]
BPCP_FOL [library]
BPCP_CND [library]
BPCP_IFOL [library]
BSRS [definition, in Undecidability.PCP]
C
card [definition, in Undecidability.PCP]cast [definition, in Undecidability.Deduction]
cBPCP [constructor, in Undecidability.PCP]
cfind [lemma, in Undecidability.Prelim]
class [constructor, in Undecidability.Deduction]
CND_BPCP [lemma, in Undecidability.BPCP_CND]
cnd_XM [lemma, in Undecidability.BPCP_CND]
compl [definition, in Undecidability.DecidableEnumerable]
const [abbreviation, in Undecidability.Semantics]
consts [definition, in Undecidability.Semantics]
consts_trans [lemma, in Undecidability.BPCP_CND]
consts_lifts [lemma, in Undecidability.Deduction]
consts_l [definition, in Undecidability.Semantics]
consts_t [definition, in Undecidability.Semantics]
cons_equi_proper [instance, in Undecidability.Prelim]
cons_incl_proper [instance, in Undecidability.Prelim]
cons_incl [lemma, in Undecidability.Prelim]
count_nat [lemma, in Undecidability.DecidableEnumerable]
count_bool [lemma, in Undecidability.DecidableEnumerable]
count_enum' [lemma, in Undecidability.DecidableEnumerable]
cprv [definition, in Undecidability.BPCP_CND]
cprv_unenum [lemma, in Undecidability.BPCP_CND]
cprv_undec [lemma, in Undecidability.BPCP_CND]
cprv_red [lemma, in Undecidability.BPCP_CND]
Ctx [constructor, in Undecidability.Deduction]
ctx_S [definition, in Undecidability.BPCP_FOL]
cumulative [definition, in Undecidability.DecidableEnumerable]
cum_T [projection, in Undecidability.DecidableEnumerable]
cum_ge' [lemma, in Undecidability.DecidableEnumerable]
cum_ge [lemma, in Undecidability.DecidableEnumerable]
C_longenough [lemma, in Undecidability.DecidableEnumerable]
C_exhaustive [lemma, in Undecidability.DecidableEnumerable]
D
Dec [definition, in Undecidability.Prelim]dec [definition, in Undecidability.Prelim]
Decb [abbreviation, in Undecidability.Prelim]
decidable [definition, in Undecidability.DecidableEnumerable]
DecidableEnumerable [library]
decidable_iff [lemma, in Undecidability.DecidableEnumerable]
decMP_to_eMP [lemma, in Undecidability.MarkovPost]
dec_red [lemma, in Undecidability.Reductions]
dec_transfer [lemma, in Undecidability.Prelim]
dec_DM_impl [lemma, in Undecidability.Prelim]
dec_DM_and [lemma, in Undecidability.Prelim]
dec_DN [lemma, in Undecidability.Prelim]
Dec_false [lemma, in Undecidability.Prelim]
Dec_true [lemma, in Undecidability.Prelim]
Dec_auto_not [lemma, in Undecidability.Prelim]
Dec_auto [lemma, in Undecidability.Prelim]
Dec_reflect_eq [lemma, in Undecidability.Prelim]
Dec_reflect [lemma, in Undecidability.Prelim]
dec_fresh [lemma, in Undecidability.Deduction]
dec_form [lemma, in Undecidability.FOL]
dec_logic [instance, in Undecidability.FOL]
dec_term [instance, in Undecidability.FOL]
dec_count_enum' [lemma, in Undecidability.DecidableEnumerable]
dec_count_enum [lemma, in Undecidability.DecidableEnumerable]
dec_disj [lemma, in Undecidability.DecidableEnumerable]
dec_conj [lemma, in Undecidability.DecidableEnumerable]
dec_compl [lemma, in Undecidability.DecidableEnumerable]
dec_decidable' [lemma, in Undecidability.DecidableEnumerable]
Deduction [library]
derivable [inductive, in Undecidability.PCP]
derivable_BPCP [lemma, in Undecidability.PCP]
derivable' [definition, in Undecidability.BPCP_FOL]
der_cons [constructor, in Undecidability.PCP]
der_sing [constructor, in Undecidability.PCP]
discrete [definition, in Undecidability.DecidableEnumerable]
discrete_list [lemma, in Undecidability.DecidableEnumerable]
discrete_option [lemma, in Undecidability.DecidableEnumerable]
discrete_sum [lemma, in Undecidability.DecidableEnumerable]
discrete_prod [lemma, in Undecidability.DecidableEnumerable]
discrete_nat_nat [lemma, in Undecidability.DecidableEnumerable]
discrete_nat [lemma, in Undecidability.DecidableEnumerable]
discrete_bool [lemma, in Undecidability.DecidableEnumerable]
discrete_iff [lemma, in Undecidability.DecidableEnumerable]
disjoint [definition, in Undecidability.Prelim]
disjoint_app [lemma, in Undecidability.Prelim]
disjoint_cons [lemma, in Undecidability.Prelim]
disjoint_nil' [lemma, in Undecidability.Prelim]
disjoint_nil [lemma, in Undecidability.Prelim]
disjoint_incl [lemma, in Undecidability.Prelim]
disjoint_symm [lemma, in Undecidability.Prelim]
disjoint_forall [lemma, in Undecidability.Prelim]
DN [constructor, in Undecidability.Deduction]
dnQ [definition, in Undecidability.BPCP_CND]
Double [lemma, in Undecidability.BPCP_CND]
Double' [lemma, in Undecidability.BPCP_CND]
drv_prv [lemma, in Undecidability.BPCP_FOL]
drv_val [lemma, in Undecidability.BPCP_FOL]
dummy [definition, in Undecidability.Infinite]
E
el_pos [lemma, in Undecidability.Prelim]el_dec [instance, in Undecidability.Infinite]
el_T [projection, in Undecidability.DecidableEnumerable]
embedding [record, in Undecidability.Kripke]
emb_trans [definition, in Undecidability.Kripke]
emb_refl [lemma, in Undecidability.Kripke]
Empty_set_eq_dec [instance, in Undecidability.Prelim]
eMP_to_MP [lemma, in Undecidability.MarkovPost]
enc [definition, in Undecidability.BPCP_FOL]
enc_vars [lemma, in Undecidability.BPCP_FOL]
enum [definition, in Undecidability.DecidableEnumerable]
enumerable [definition, in Undecidability.DecidableEnumerable]
enumerable_red [lemma, in Undecidability.Reductions]
enumerable_PCP [lemma, in Undecidability.PCP]
enumerable_derivable [lemma, in Undecidability.PCP]
enumerable_class_prv [lemma, in Undecidability.Deduction]
enumerable_intu_prv [lemma, in Undecidability.Deduction]
enumerable_min_prv [lemma, in Undecidability.Deduction]
enumerable_conj [lemma, in Undecidability.DecidableEnumerable]
enumerable_disj [lemma, in Undecidability.DecidableEnumerable]
enumerable__T_list [lemma, in Undecidability.DecidableEnumerable]
enumerable_list [instance, in Undecidability.DecidableEnumerable]
enumerable_list.fixL.LX [variable, in Undecidability.DecidableEnumerable]
enumerable_list.fixL [section, in Undecidability.DecidableEnumerable]
enumerable_list.X [variable, in Undecidability.DecidableEnumerable]
enumerable_list [section, in Undecidability.DecidableEnumerable]
enumerable__T_option [lemma, in Undecidability.DecidableEnumerable]
enumerable__T_sum [lemma, in Undecidability.DecidableEnumerable]
enumerable__T_prod [lemma, in Undecidability.DecidableEnumerable]
enumerable_enum [lemma, in Undecidability.DecidableEnumerable]
enumerable_nat_nat [lemma, in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs.L_Y [variable, in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs.L_X [variable, in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs [section, in Undecidability.DecidableEnumerable]
enumerable_prod.Y [variable, in Undecidability.DecidableEnumerable]
enumerable_prod.X [variable, in Undecidability.DecidableEnumerable]
enumerable_prod [section, in Undecidability.DecidableEnumerable]
enumerable_enum.e [variable, in Undecidability.DecidableEnumerable]
enumerable_enum.p [variable, in Undecidability.DecidableEnumerable]
enumerable_enum.X [variable, in Undecidability.DecidableEnumerable]
enumerable_enum [section, in Undecidability.DecidableEnumerable]
enumerable_enumerable_T [lemma, in Undecidability.DecidableEnumerable]
enumerable__T [definition, in Undecidability.DecidableEnumerable]
enumT [record, in Undecidability.DecidableEnumerable]
enumT_form [instance, in Undecidability.FOL]
enumT_term [instance, in Undecidability.FOL]
enumT_nat [instance, in Undecidability.DecidableEnumerable]
enum_red [lemma, in Undecidability.Reductions]
enum_red.d [variable, in Undecidability.Reductions]
enum_red.x0 [variable, in Undecidability.Reductions]
enum_red.qe [variable, in Undecidability.Reductions]
enum_red.Lq [variable, in Undecidability.Reductions]
enum_red.Hf [variable, in Undecidability.Reductions]
enum_red.f [variable, in Undecidability.Reductions]
enum_red.q [variable, in Undecidability.Reductions]
enum_red.p [variable, in Undecidability.Reductions]
enum_red.Y [variable, in Undecidability.Reductions]
enum_red.X [variable, in Undecidability.Reductions]
enum_red [section, in Undecidability.Reductions]
enum_PCP' [lemma, in Undecidability.PCP]
enum_prv [lemma, in Undecidability.Deduction]
enum_enumT [lemma, in Undecidability.DecidableEnumerable]
enum_count [lemma, in Undecidability.DecidableEnumerable]
enum_enumerable [section, in Undecidability.DecidableEnumerable]
enum_bool [instance, in Undecidability.DecidableEnumerable]
enum_to_cumulative [lemma, in Undecidability.DecidableEnumerable]
env [definition, in Undecidability.Semantics]
eqType [record, in Undecidability.Prelim]
EqType [constructor, in Undecidability.Prelim]
eqType_dec [projection, in Undecidability.Prelim]
eqType_X [projection, in Undecidability.Prelim]
Equi [section, in Undecidability.Prelim]
equi [definition, in Undecidability.Prelim]
equi_rotate [lemma, in Undecidability.Prelim]
equi_shift [lemma, in Undecidability.Prelim]
equi_swap [lemma, in Undecidability.Prelim]
equi_dup [lemma, in Undecidability.Prelim]
equi_push [lemma, in Undecidability.Prelim]
equi_Equivalence [instance, in Undecidability.Prelim]
Equi.X [variable, in Undecidability.Prelim]
eq_dec_form [instance, in Undecidability.FOL]
eval [definition, in Undecidability.Semantics]
eval_empty [lemma, in Undecidability.Deduction]
eval_ext [lemma, in Undecidability.Deduction]
eval_ext_p [lemma, in Undecidability.Deduction]
eval_invar [lemma, in Undecidability.Kripke]
Exp [constructor, in Undecidability.Deduction]
F
F [definition, in Undecidability.BPCP_FOL]F [definition, in Undecidability.Infinite]
f [definition, in Undecidability.Infinite]
Fal [constructor, in Undecidability.FOL]
False_eq_dec [instance, in Undecidability.Prelim]
False_dec [instance, in Undecidability.Prelim]
FG [lemma, in Undecidability.Infinite]
filter [definition, in Undecidability.Prelim]
Filter [section, in Undecidability.Prelim]
filter_comm [lemma, in Undecidability.Prelim]
filter_and [lemma, in Undecidability.Prelim]
filter_pq_eq [lemma, in Undecidability.Prelim]
filter_pq_mono [lemma, in Undecidability.Prelim]
filter_fst' [lemma, in Undecidability.Prelim]
filter_fst [lemma, in Undecidability.Prelim]
filter_app [lemma, in Undecidability.Prelim]
filter_id [lemma, in Undecidability.Prelim]
filter_mono [lemma, in Undecidability.Prelim]
filter_incl [lemma, in Undecidability.Prelim]
Filter.X [variable, in Undecidability.Prelim]
FOL [library]
form [inductive, in Undecidability.FOL]
form_discrete [lemma, in Undecidability.BPCP_FOL]
form_logic_ind_subst [lemma, in Undecidability.Deduction]
form_ind_subst [lemma, in Undecidability.Deduction]
form_frag_ind [lemma, in Undecidability.FOL]
frag [constructor, in Undecidability.FOL]
fresh [definition, in Undecidability.Semantics]
full [constructor, in Undecidability.FOL]
fullsatis [definition, in Undecidability.Semantics]
fun_comp [definition, in Undecidability.Weakening]
F_stack [definition, in Undecidability.Infinite]
F_sur [lemma, in Undecidability.Infinite]
F_inj [lemma, in Undecidability.Infinite]
F_inj' [lemma, in Undecidability.Infinite]
F_lt [lemma, in Undecidability.Infinite]
F_el [lemma, in Undecidability.Infinite]
F_nel [lemma, in Undecidability.Infinite]
f_sur [lemma, in Undecidability.Infinite]
F1 [definition, in Undecidability.BPCP_FOL]
F2 [definition, in Undecidability.BPCP_FOL]
F3 [definition, in Undecidability.BPCP_FOL]
G
G [definition, in Undecidability.Infinite]gen [lemma, in Undecidability.Infinite]
generating [definition, in Undecidability.Infinite]
gen_le_f [lemma, in Undecidability.Infinite]
gen_spec [lemma, in Undecidability.Infinite]
gen_weakening [lemma, in Undecidability.Weakening]
gen' [definition, in Undecidability.Infinite]
Gen2Inf [section, in Undecidability.Infinite]
Gen2Inf.f' [variable, in Undecidability.Infinite]
Gen2Inf.Hf' [variable, in Undecidability.Infinite]
Gen2Inf.Hg [variable, in Undecidability.Infinite]
Gen2Inf.HX [variable, in Undecidability.Infinite]
Gen2Inf.X [variable, in Undecidability.Infinite]
GF [lemma, in Undecidability.Infinite]
H
He [projection, in Undecidability.Kripke]Hf [projection, in Undecidability.Kripke]
HP [projection, in Undecidability.Kripke]
HQ [projection, in Undecidability.Kripke]
I
IB [instance, in Undecidability.BPCP_FOL]IB_F [lemma, in Undecidability.BPCP_FOL]
IB_F3 [lemma, in Undecidability.BPCP_FOL]
IB_F2 [lemma, in Undecidability.BPCP_FOL]
IB_F1 [lemma, in Undecidability.BPCP_FOL]
IB_stable [lemma, in Undecidability.BPCP_FOL]
IB_drv [lemma, in Undecidability.BPCP_FOL]
IB_enc [lemma, in Undecidability.BPCP_FOL]
IB_prep [lemma, in Undecidability.BPCP_FOL]
iff_dec [instance, in Undecidability.Prelim]
ImpE [constructor, in Undecidability.Deduction]
ImpI [constructor, in Undecidability.Deduction]
impl [definition, in Undecidability.FOL]
Impl [constructor, in Undecidability.FOL]
impl_prv [lemma, in Undecidability.BPCP_FOL]
impl_dec [instance, in Undecidability.Prelim]
impl_trans [lemma, in Undecidability.BPCP_CND]
impl_sat' [lemma, in Undecidability.Semantics]
impl_sat [lemma, in Undecidability.Semantics]
impl_ksat' [lemma, in Undecidability.Kripke]
impl_ksat [lemma, in Undecidability.Kripke]
inclp [definition, in Undecidability.Prelim]
Inclusion [section, in Undecidability.Prelim]
Inclusion.X [variable, in Undecidability.Prelim]
incl_equi_proper [instance, in Undecidability.Prelim]
incl_preorder [instance, in Undecidability.Prelim]
incl_app_left [lemma, in Undecidability.Prelim]
incl_lrcons [lemma, in Undecidability.Prelim]
incl_rcons [lemma, in Undecidability.Prelim]
incl_lcons [lemma, in Undecidability.Prelim]
incl_shift [lemma, in Undecidability.Prelim]
incl_nil_eq [lemma, in Undecidability.Prelim]
incl_map [lemma, in Undecidability.Prelim]
incl_sing [lemma, in Undecidability.Prelim]
incl_nil [lemma, in Undecidability.Prelim]
incl_dec [lemma, in Undecidability.Deduction]
infinite [definition, in Undecidability.Infinite]
Infinite [library]
inf_quasi_nat [lemma, in Undecidability.Infinite]
inf_form [lemma, in Undecidability.FOL]
inf_term [lemma, in Undecidability.FOL]
Inf2Gen [section, in Undecidability.Infinite]
Inf2Gen.f [variable, in Undecidability.Infinite]
Inf2Gen.f' [variable, in Undecidability.Infinite]
Inf2Gen.Hf [variable, in Undecidability.Infinite]
Inf2Gen.Hf' [variable, in Undecidability.Infinite]
Inf2Gen.HX [variable, in Undecidability.Infinite]
Inf2Gen.X [variable, in Undecidability.Infinite]
injective [definition, in Undecidability.Infinite]
interp [record, in Undecidability.Semantics]
interp_kripke [instance, in Undecidability.Kripke]
intu [constructor, in Undecidability.Deduction]
in_rem_iff [lemma, in Undecidability.Prelim]
in_filter_iff [lemma, in Undecidability.Prelim]
in_concat_iff [lemma, in Undecidability.Prelim]
in_equi_proper [instance, in Undecidability.Prelim]
in_incl_proper [instance, in Undecidability.Prelim]
in_cons_neq [lemma, in Undecidability.Prelim]
in_sing [lemma, in Undecidability.Prelim]
in_omap_iff [lemma, in Undecidability.Prelim]
iprep [definition, in Undecidability.BPCP_FOL]
iprep_app [lemma, in Undecidability.BPCP_FOL]
iprep_eval [lemma, in Undecidability.BPCP_FOL]
iUnit [instance, in Undecidability.BPCP_CND]
i_Q [projection, in Undecidability.Semantics]
i_P [projection, in Undecidability.Semantics]
i_e [projection, in Undecidability.Semantics]
i_f [projection, in Undecidability.Semantics]
K
kcast [definition, in Undecidability.Kripke]kmodel [record, in Undecidability.Kripke]
kprv_unenum [lemma, in Undecidability.BPCP_IFOL]
kprv_undec [lemma, in Undecidability.BPCP_IFOL]
kprv_red [lemma, in Undecidability.BPCP_IFOL]
Kripke [section, in Undecidability.Kripke]
Kripke [library]
kripke_tarski [lemma, in Undecidability.Kripke]
Kripke.eta [variable, in Undecidability.Kripke]
Kripke.M [variable, in Undecidability.Kripke]
_ ⊫( _ ) _ [notation, in Undecidability.Kripke]
_ ⊨( _ ) _ [notation, in Undecidability.Kripke]
ksat [definition, in Undecidability.Kripke]
ksatis [definition, in Undecidability.Kripke]
ksatis_enum [lemma, in Undecidability.BPCP_IFOL]
ksatis_undec [lemma, in Undecidability.BPCP_IFOL]
ksatis_red [lemma, in Undecidability.BPCP_IFOL]
ksatis_satis [lemma, in Undecidability.Kripke]
ksat_ext [lemma, in Undecidability.Kripke]
ksat_ext_p [lemma, in Undecidability.Kripke]
ksat_iff [lemma, in Undecidability.Kripke]
ksat_mon [lemma, in Undecidability.Kripke]
ksoundness [lemma, in Undecidability.Kripke]
ksoundness' [lemma, in Undecidability.Kripke]
kvalid [definition, in Undecidability.Kripke]
kvalidity [section, in Undecidability.BPCP_IFOL]
kvalidity.R [variable, in Undecidability.BPCP_IFOL]
kvalid_unenum [lemma, in Undecidability.BPCP_IFOL]
kvalid_undec [lemma, in Undecidability.BPCP_IFOL]
kvalid_red [lemma, in Undecidability.BPCP_IFOL]
kvalid_valid [lemma, in Undecidability.Kripke]
L
L [definition, in Undecidability.Reductions]ldecidable [definition, in Undecidability.MarkovPost]
le_f [definition, in Undecidability.Infinite]
lift [definition, in Undecidability.Deduction]
list_cc [lemma, in Undecidability.Prelim]
list_exists_not_incl [lemma, in Undecidability.Prelim]
list_exists_DM [lemma, in Undecidability.Prelim]
list_exists_dec [instance, in Undecidability.Prelim]
list_forall_dec [instance, in Undecidability.Prelim]
list_in_dec [instance, in Undecidability.Prelim]
list_cycle [lemma, in Undecidability.Prelim]
list_eq_dec [instance, in Undecidability.Prelim]
list_ind_ne [lemma, in Undecidability.Prelim]
LL [definition, in Undecidability.Infinite]
LL_F [lemma, in Undecidability.Infinite]
LL_f [lemma, in Undecidability.Infinite]
LL_cum [lemma, in Undecidability.Infinite]
logic [inductive, in Undecidability.FOL]
lt_acc [lemma, in Undecidability.Infinite]
LX [definition, in Undecidability.Infinite]
LX_NoDup [lemma, in Undecidability.Infinite]
LX_el [lemma, in Undecidability.Infinite]
LX_len [lemma, in Undecidability.Infinite]
L_PCP [definition, in Undecidability.PCP]
L_ded [definition, in Undecidability.Deduction]
L_form [definition, in Undecidability.FOL]
L_term [definition, in Undecidability.FOL]
L_T [projection, in Undecidability.DecidableEnumerable]
M
make_fresh [lemma, in Undecidability.Semantics]MarkovPost [library]
Membership [section, in Undecidability.Prelim]
Membership.X [variable, in Undecidability.Prelim]
mkfresh [definition, in Undecidability.Semantics]
mkfresh_spec [lemma, in Undecidability.Semantics]
MND_CND [lemma, in Undecidability.BPCP_CND]
MND_IND [lemma, in Undecidability.Deduction]
MP [definition, in Undecidability.MarkovPost]
MP_Post [lemma, in Undecidability.MarkovPost]
MP_enum_stable [lemma, in Undecidability.MarkovPost]
MP_to_decMP [lemma, in Undecidability.MarkovPost]
mu [definition, in Undecidability.MarkovPost]
mu_least [lemma, in Undecidability.MarkovPost]
mu' [abbreviation, in Undecidability.MarkovPost]
M_stable [lemma, in Undecidability.BPCP_FOL]
N
nat_eq_dec [instance, in Undecidability.Prelim]nd [inductive, in Undecidability.Deduction]
ND_CND [lemma, in Undecidability.Weakening]
neList [section, in Undecidability.Prelim]
neList.B [variable, in Undecidability.Prelim]
neList.P [variable, in Undecidability.Prelim]
neList.S [variable, in Undecidability.Prelim]
neList.X [variable, in Undecidability.Prelim]
nodes [projection, in Undecidability.Kripke]
NonStan [module, in Undecidability.BPCP_FOL]
NonStan.IB [instance, in Undecidability.BPCP_FOL]
NonStan.IB_nonstandard [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_F [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_F2 [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_F1 [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_deriv' [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_deriv [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_enc [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_eval_None [lemma, in Undecidability.BPCP_FOL]
NonStan.IB_eval_Some [lemma, in Undecidability.BPCP_FOL]
NonStan.Nonstan [section, in Undecidability.BPCP_FOL]
NonStan.Nonstan.R [variable, in Undecidability.BPCP_FOL]
not_coenumerable [lemma, in Undecidability.Reductions]
not_decidable [lemma, in Undecidability.Reductions]
not_in_cons [lemma, in Undecidability.Prelim]
not_dec [instance, in Undecidability.Prelim]
nthe [abbreviation, in Undecidability.Prelim]
nthe [abbreviation, in Undecidability.Prelim]
nthe_app_l [lemma, in Undecidability.Prelim]
nthe_length [lemma, in Undecidability.Prelim]
O
ofNat [definition, in Undecidability.DecidableEnumerable]omap [definition, in Undecidability.Prelim]
option_eq_dec [instance, in Undecidability.Prelim]
or_dec [instance, in Undecidability.Prelim]
P
P [constructor, in Undecidability.FOL]pairs_retract [lemma, in Undecidability.DecidableEnumerable]
par [abbreviation, in Undecidability.FOL]
PCP [definition, in Undecidability.PCP]
PCP [library]
pos [definition, in Undecidability.Prelim]
Positions [section, in Undecidability.Prelim]
Positions.d [variable, in Undecidability.Prelim]
Positions.X [variable, in Undecidability.Prelim]
POST [definition, in Undecidability.MarkovPost]
Post_MP [lemma, in Undecidability.MarkovPost]
Post_to' [lemma, in Undecidability.MarkovPost]
POST' [definition, in Undecidability.MarkovPost]
pos_length [lemma, in Undecidability.Prelim]
pos_nth [lemma, in Undecidability.Prelim]
pos_nthe [lemma, in Undecidability.Prelim]
Pr [constructor, in Undecidability.FOL]
Prelim [library]
prep [definition, in Undecidability.BPCP_FOL]
prep_vars [lemma, in Undecidability.BPCP_FOL]
prep_subst [lemma, in Undecidability.BPCP_FOL]
prod_eq_dec [instance, in Undecidability.Prelim]
prod_enumerable [instance, in Undecidability.DecidableEnumerable]
projection [lemma, in Undecidability.DecidableEnumerable]
projection' [lemma, in Undecidability.DecidableEnumerable]
prv [inductive, in Undecidability.Deduction]
prv_unenum [lemma, in Undecidability.BPCP_FOL]
prv_undec [lemma, in Undecidability.BPCP_FOL]
prv_red [lemma, in Undecidability.BPCP_FOL]
prv_ind_min [lemma, in Undecidability.Deduction]
prv_intu [definition, in Undecidability.Deduction]
prv_class [definition, in Undecidability.Deduction]
prv_min [definition, in Undecidability.Deduction]
Q
Q [constructor, in Undecidability.FOL]quasi_nat [definition, in Undecidability.Infinite]
R
R [abbreviation, in Undecidability.MarkovPost]reachable [projection, in Undecidability.Kripke]
reach_tran [projection, in Undecidability.Kripke]
reach_refl [projection, in Undecidability.Kripke]
reduces [definition, in Undecidability.Reductions]
reduces_transitive [lemma, in Undecidability.Reductions]
Reductions [library]
red_comp [lemma, in Undecidability.Reductions]
rem [definition, in Undecidability.Prelim]
Removal [section, in Undecidability.Prelim]
Removal.X [variable, in Undecidability.Prelim]
rem_inclr [lemma, in Undecidability.Prelim]
rem_reorder [lemma, in Undecidability.Prelim]
rem_id [lemma, in Undecidability.Prelim]
rem_fst' [lemma, in Undecidability.Prelim]
rem_fst [lemma, in Undecidability.Prelim]
rem_comm [lemma, in Undecidability.Prelim]
rem_equi [lemma, in Undecidability.Prelim]
rem_app' [lemma, in Undecidability.Prelim]
rem_app [lemma, in Undecidability.Prelim]
rem_neq [lemma, in Undecidability.Prelim]
rem_in [lemma, in Undecidability.Prelim]
rem_cons' [lemma, in Undecidability.Prelim]
rem_cons [lemma, in Undecidability.Prelim]
rem_mono [lemma, in Undecidability.Prelim]
rem_incl [lemma, in Undecidability.Prelim]
rem_not_in [lemma, in Undecidability.Prelim]
ren [definition, in Undecidability.Weakening]
ren_swap_ctx [lemma, in Undecidability.Weakening]
ren_subst [lemma, in Undecidability.Weakening]
ren_subst_t [lemma, in Undecidability.Weakening]
ren_ext_ctx [lemma, in Undecidability.Weakening]
ren_ext [lemma, in Undecidability.Weakening]
ren_ext_t [lemma, in Undecidability.Weakening]
ren_comp_ctx [lemma, in Undecidability.Weakening]
ren_comp [lemma, in Undecidability.Weakening]
ren_comp_t [lemma, in Undecidability.Weakening]
ren_ctx_id [lemma, in Undecidability.Weakening]
ren_id [lemma, in Undecidability.Weakening]
ren_id_t [lemma, in Undecidability.Weakening]
ren_ctx [definition, in Undecidability.Weakening]
ren_t [definition, in Undecidability.Weakening]
R_nat_nat [definition, in Undecidability.DecidableEnumerable]
S
sat [definition, in Undecidability.Semantics]satis [definition, in Undecidability.Semantics]
satis_enum [lemma, in Undecidability.BPCP_FOL]
satis_undec [lemma, in Undecidability.BPCP_FOL]
satis_red [lemma, in Undecidability.BPCP_FOL]
sat_ext_p_list [lemma, in Undecidability.Deduction]
sat_ext [lemma, in Undecidability.Deduction]
sat_ext_p [lemma, in Undecidability.Deduction]
Semantics [section, in Undecidability.Semantics]
Semantics [library]
Semantics.domain [variable, in Undecidability.Semantics]
Semantics.eta [variable, in Undecidability.Semantics]
_ ⊨ _ [notation, in Undecidability.Semantics]
_ ⊫ _ [notation, in Undecidability.Semantics]
_ [[ _ := _ ]] [notation, in Undecidability.Semantics]
sem_imp [abbreviation, in Undecidability.Kripke]
singles [definition, in Undecidability.Weakening]
size [definition, in Undecidability.Deduction]
size_induction_dep [lemma, in Undecidability.Prelim]
size_induction [lemma, in Undecidability.Prelim]
size_subst [lemma, in Undecidability.Deduction]
soundness [lemma, in Undecidability.Deduction]
soundness' [lemma, in Undecidability.Deduction]
SRS [definition, in Undecidability.PCP]
stable [definition, in Undecidability.MarkovPost]
stable_red [lemma, in Undecidability.MarkovPost]
stack [definition, in Undecidability.PCP]
stack_enum [lemma, in Undecidability.PCP]
stack_discrete [lemma, in Undecidability.PCP]
stack_quasi_nat [lemma, in Undecidability.Infinite]
stack_infinite [lemma, in Undecidability.Infinite]
string [definition, in Undecidability.PCP]
subst [definition, in Undecidability.Semantics]
substconst_sat [lemma, in Undecidability.Deduction]
substconst_ksat [lemma, in Undecidability.Kripke]
subst_sat [lemma, in Undecidability.Deduction]
subst_eval [lemma, in Undecidability.Deduction]
subst_lift [lemma, in Undecidability.Deduction]
subst_t [definition, in Undecidability.Semantics]
subst_ksat [lemma, in Undecidability.Kripke]
sub_dec [lemma, in Undecidability.Infinite]
sum_eq_dec [instance, in Undecidability.Prelim]
surjective [definition, in Undecidability.Infinite]
symbol [definition, in Undecidability.PCP]
T
tau1 [definition, in Undecidability.PCP]tau2 [definition, in Undecidability.PCP]
term [inductive, in Undecidability.FOL]
TM [instance, in Undecidability.Semantics]
TM [section, in Undecidability.Semantics]
TM_sat [lemma, in Undecidability.Semantics]
to_dec [lemma, in Undecidability.Prelim]
trans [definition, in Undecidability.BPCP_CND]
trans_trans [lemma, in Undecidability.BPCP_CND]
trans_subst [lemma, in Undecidability.BPCP_CND]
True_eq_dec [instance, in Undecidability.Prelim]
True_dec [instance, in Undecidability.Prelim]
t_e [constructor, in Undecidability.FOL]
t_f [constructor, in Undecidability.FOL]
T_list_el [lemma, in Undecidability.DecidableEnumerable]
T_list_cum [lemma, in Undecidability.DecidableEnumerable]
T_list [definition, in Undecidability.DecidableEnumerable]
T_prod_el [lemma, in Undecidability.DecidableEnumerable]
T_prod_cum [lemma, in Undecidability.DecidableEnumerable]
T_prod [definition, in Undecidability.DecidableEnumerable]
T_nat_length [lemma, in Undecidability.DecidableEnumerable]
T_nat_in [lemma, in Undecidability.DecidableEnumerable]
T_ [definition, in Undecidability.DecidableEnumerable]
U
u [abbreviation, in Undecidability.BPCP_FOL]UA [definition, in Undecidability.BPCP_FOL]
unit_eq_dec [instance, in Undecidability.Prelim]
update [definition, in Undecidability.Semantics]
V
v [abbreviation, in Undecidability.BPCP_FOL]V [constructor, in Undecidability.FOL]
valid [definition, in Undecidability.Semantics]
validity [section, in Undecidability.BPCP_FOL]
validity.R [variable, in Undecidability.BPCP_FOL]
valid_unenum [lemma, in Undecidability.BPCP_FOL]
valid_undec [lemma, in Undecidability.BPCP_FOL]
valid_red [lemma, in Undecidability.BPCP_FOL]
valid_satis [lemma, in Undecidability.BPCP_FOL]
valid_L [definition, in Undecidability.Semantics]
var [abbreviation, in Undecidability.FOL]
vars_t_ren [lemma, in Undecidability.Weakening]
vars_t [definition, in Undecidability.Semantics]
W
Weak [lemma, in Undecidability.Weakening]Weakening [library]
weakPost [lemma, in Undecidability.MarkovPost]
world [projection, in Undecidability.Kripke]
world_f [projection, in Undecidability.Kripke]
X
X_gen [lemma, in Undecidability.Infinite]other
_ ⪯ _ [notation, in Undecidability.Reductions]_ / _ [notation, in Undecidability.PCP]
_ === _ [notation, in Undecidability.Prelim]
_ <<= _ [notation, in Undecidability.Prelim]
_ el _ [notation, in Undecidability.Prelim]
_ <<= _ [notation, in Undecidability.Prelim]
_ el _ [notation, in Undecidability.Prelim]
_ ⊢C _ [notation, in Undecidability.Deduction]
_ ⊢I _ [notation, in Undecidability.Deduction]
_ ⊢M _ [notation, in Undecidability.Deduction]
_ ⊢ _ [notation, in Undecidability.Deduction]
_ ==> _ [notation, in Undecidability.FOL]
_ --> _ [notation, in Undecidability.FOL]
_ ∘ _ [notation, in Undecidability.Weakening]
_ :-> _ [notation, in Undecidability.Weakening]
_ ⊨ _ [notation, in Undecidability.Semantics]
_ ⊫ _ [notation, in Undecidability.Semantics]
_ [[ _ := _ ]] [notation, in Undecidability.Semantics]
_ ⊩( _ , _ , _ ) _ [notation, in Undecidability.Kripke]
eq_dec _ [notation, in Undecidability.Prelim]
! _ [notation, in Undecidability.Kripke]
( _ × _ × .. × _ ) [notation, in Undecidability.Prelim]
[ _ | _ ∈ _ ] [notation, in Undecidability.Prelim]
[ _ | _ ∈ _ , _ ] [notation, in Undecidability.Prelim]
| _ | [notation, in Undecidability.Prelim]
| _ | [notation, in Undecidability.Prelim]
∀ _ ; _ [notation, in Undecidability.FOL]
⊥ [notation, in Undecidability.FOL]
¬ _ [notation, in Undecidability.FOL]
Notation Index
K
_ ⊫( _ ) _ [in Undecidability.Kripke]_ ⊨( _ ) _ [in Undecidability.Kripke]
S
_ ⊨ _ [in Undecidability.Semantics]_ ⊫ _ [in Undecidability.Semantics]
_ [[ _ := _ ]] [in Undecidability.Semantics]
other
_ ⪯ _ [in Undecidability.Reductions]_ / _ [in Undecidability.PCP]
_ === _ [in Undecidability.Prelim]
_ <<= _ [in Undecidability.Prelim]
_ el _ [in Undecidability.Prelim]
_ <<= _ [in Undecidability.Prelim]
_ el _ [in Undecidability.Prelim]
_ ⊢C _ [in Undecidability.Deduction]
_ ⊢I _ [in Undecidability.Deduction]
_ ⊢M _ [in Undecidability.Deduction]
_ ⊢ _ [in Undecidability.Deduction]
_ ==> _ [in Undecidability.FOL]
_ --> _ [in Undecidability.FOL]
_ ∘ _ [in Undecidability.Weakening]
_ :-> _ [in Undecidability.Weakening]
_ ⊨ _ [in Undecidability.Semantics]
_ ⊫ _ [in Undecidability.Semantics]
_ [[ _ := _ ]] [in Undecidability.Semantics]
_ ⊩( _ , _ , _ ) _ [in Undecidability.Kripke]
eq_dec _ [in Undecidability.Prelim]
! _ [in Undecidability.Kripke]
( _ × _ × .. × _ ) [in Undecidability.Prelim]
[ _ | _ ∈ _ ] [in Undecidability.Prelim]
[ _ | _ ∈ _ , _ ] [in Undecidability.Prelim]
| _ | [in Undecidability.Prelim]
| _ | [in Undecidability.Prelim]
∀ _ ; _ [in Undecidability.FOL]
⊥ [in Undecidability.FOL]
¬ _ [in Undecidability.FOL]
Module Index
N
NonStan [in Undecidability.BPCP_FOL]Variable Index
B
BPCP_CND.R [in Undecidability.BPCP_CND]E
enumerable_list.fixL.LX [in Undecidability.DecidableEnumerable]enumerable_list.X [in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs.L_Y [in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs.L_X [in Undecidability.DecidableEnumerable]
enumerable_prod.Y [in Undecidability.DecidableEnumerable]
enumerable_prod.X [in Undecidability.DecidableEnumerable]
enumerable_enum.e [in Undecidability.DecidableEnumerable]
enumerable_enum.p [in Undecidability.DecidableEnumerable]
enumerable_enum.X [in Undecidability.DecidableEnumerable]
enum_red.d [in Undecidability.Reductions]
enum_red.x0 [in Undecidability.Reductions]
enum_red.qe [in Undecidability.Reductions]
enum_red.Lq [in Undecidability.Reductions]
enum_red.Hf [in Undecidability.Reductions]
enum_red.f [in Undecidability.Reductions]
enum_red.q [in Undecidability.Reductions]
enum_red.p [in Undecidability.Reductions]
enum_red.Y [in Undecidability.Reductions]
enum_red.X [in Undecidability.Reductions]
Equi.X [in Undecidability.Prelim]
F
Filter.X [in Undecidability.Prelim]G
Gen2Inf.f' [in Undecidability.Infinite]Gen2Inf.Hf' [in Undecidability.Infinite]
Gen2Inf.Hg [in Undecidability.Infinite]
Gen2Inf.HX [in Undecidability.Infinite]
Gen2Inf.X [in Undecidability.Infinite]
I
Inclusion.X [in Undecidability.Prelim]Inf2Gen.f [in Undecidability.Infinite]
Inf2Gen.f' [in Undecidability.Infinite]
Inf2Gen.Hf [in Undecidability.Infinite]
Inf2Gen.Hf' [in Undecidability.Infinite]
Inf2Gen.HX [in Undecidability.Infinite]
Inf2Gen.X [in Undecidability.Infinite]
K
Kripke.eta [in Undecidability.Kripke]Kripke.M [in Undecidability.Kripke]
kvalidity.R [in Undecidability.BPCP_IFOL]
M
Membership.X [in Undecidability.Prelim]N
neList.B [in Undecidability.Prelim]neList.P [in Undecidability.Prelim]
neList.S [in Undecidability.Prelim]
neList.X [in Undecidability.Prelim]
NonStan.Nonstan.R [in Undecidability.BPCP_FOL]
P
Positions.d [in Undecidability.Prelim]Positions.X [in Undecidability.Prelim]
R
Removal.X [in Undecidability.Prelim]S
Semantics.domain [in Undecidability.Semantics]Semantics.eta [in Undecidability.Semantics]
V
validity.R [in Undecidability.BPCP_FOL]Library Index
B
BPCP_FOLBPCP_CND
BPCP_IFOL
D
DecidableEnumerableDeduction
F
FOLI
InfiniteK
KripkeM
MarkovPostP
PCPPrelim
R
ReductionsS
SemanticsW
WeakeningLemma Index
A
Acc_ind_dep [in Undecidability.MarkovPost]appCtx [in Undecidability.BPCP_CND]
app_incl_R [in Undecidability.Prelim]
app_incl_l [in Undecidability.Prelim]
app_sub [in Undecidability.Semantics]
app1 [in Undecidability.BPCP_CND]
app2 [in Undecidability.BPCP_CND]
app3 [in Undecidability.BPCP_CND]
B
bool_Prop_false [in Undecidability.Prelim]bool_Prop_true [in Undecidability.Prelim]
BPCP_ksatis [in Undecidability.BPCP_IFOL]
BPCP_kvalid [in Undecidability.BPCP_IFOL]
BPCP_kprv [in Undecidability.BPCP_IFOL]
BPCP_derivable [in Undecidability.PCP]
BPCP_satis [in Undecidability.BPCP_FOL]
BPCP_prv [in Undecidability.BPCP_FOL]
BPCP_prv' [in Undecidability.BPCP_FOL]
BPCP_valid [in Undecidability.BPCP_FOL]
BPCP_CND [in Undecidability.BPCP_CND]
BPCP_to_CND [in Undecidability.BPCP_CND]
C
cfind [in Undecidability.Prelim]CND_BPCP [in Undecidability.BPCP_CND]
cnd_XM [in Undecidability.BPCP_CND]
consts_trans [in Undecidability.BPCP_CND]
consts_lifts [in Undecidability.Deduction]
cons_incl [in Undecidability.Prelim]
count_nat [in Undecidability.DecidableEnumerable]
count_bool [in Undecidability.DecidableEnumerable]
count_enum' [in Undecidability.DecidableEnumerable]
cprv_unenum [in Undecidability.BPCP_CND]
cprv_undec [in Undecidability.BPCP_CND]
cprv_red [in Undecidability.BPCP_CND]
cum_ge' [in Undecidability.DecidableEnumerable]
cum_ge [in Undecidability.DecidableEnumerable]
C_longenough [in Undecidability.DecidableEnumerable]
C_exhaustive [in Undecidability.DecidableEnumerable]
D
decidable_iff [in Undecidability.DecidableEnumerable]decMP_to_eMP [in Undecidability.MarkovPost]
dec_red [in Undecidability.Reductions]
dec_transfer [in Undecidability.Prelim]
dec_DM_impl [in Undecidability.Prelim]
dec_DM_and [in Undecidability.Prelim]
dec_DN [in Undecidability.Prelim]
Dec_false [in Undecidability.Prelim]
Dec_true [in Undecidability.Prelim]
Dec_auto_not [in Undecidability.Prelim]
Dec_auto [in Undecidability.Prelim]
Dec_reflect_eq [in Undecidability.Prelim]
Dec_reflect [in Undecidability.Prelim]
dec_fresh [in Undecidability.Deduction]
dec_form [in Undecidability.FOL]
dec_count_enum' [in Undecidability.DecidableEnumerable]
dec_count_enum [in Undecidability.DecidableEnumerable]
dec_disj [in Undecidability.DecidableEnumerable]
dec_conj [in Undecidability.DecidableEnumerable]
dec_compl [in Undecidability.DecidableEnumerable]
dec_decidable' [in Undecidability.DecidableEnumerable]
derivable_BPCP [in Undecidability.PCP]
discrete_list [in Undecidability.DecidableEnumerable]
discrete_option [in Undecidability.DecidableEnumerable]
discrete_sum [in Undecidability.DecidableEnumerable]
discrete_prod [in Undecidability.DecidableEnumerable]
discrete_nat_nat [in Undecidability.DecidableEnumerable]
discrete_nat [in Undecidability.DecidableEnumerable]
discrete_bool [in Undecidability.DecidableEnumerable]
discrete_iff [in Undecidability.DecidableEnumerable]
disjoint_app [in Undecidability.Prelim]
disjoint_cons [in Undecidability.Prelim]
disjoint_nil' [in Undecidability.Prelim]
disjoint_nil [in Undecidability.Prelim]
disjoint_incl [in Undecidability.Prelim]
disjoint_symm [in Undecidability.Prelim]
disjoint_forall [in Undecidability.Prelim]
Double [in Undecidability.BPCP_CND]
Double' [in Undecidability.BPCP_CND]
drv_prv [in Undecidability.BPCP_FOL]
drv_val [in Undecidability.BPCP_FOL]
E
el_pos [in Undecidability.Prelim]emb_refl [in Undecidability.Kripke]
eMP_to_MP [in Undecidability.MarkovPost]
enc_vars [in Undecidability.BPCP_FOL]
enumerable_red [in Undecidability.Reductions]
enumerable_PCP [in Undecidability.PCP]
enumerable_derivable [in Undecidability.PCP]
enumerable_class_prv [in Undecidability.Deduction]
enumerable_intu_prv [in Undecidability.Deduction]
enumerable_min_prv [in Undecidability.Deduction]
enumerable_conj [in Undecidability.DecidableEnumerable]
enumerable_disj [in Undecidability.DecidableEnumerable]
enumerable__T_list [in Undecidability.DecidableEnumerable]
enumerable__T_option [in Undecidability.DecidableEnumerable]
enumerable__T_sum [in Undecidability.DecidableEnumerable]
enumerable__T_prod [in Undecidability.DecidableEnumerable]
enumerable_enum [in Undecidability.DecidableEnumerable]
enumerable_nat_nat [in Undecidability.DecidableEnumerable]
enumerable_enumerable_T [in Undecidability.DecidableEnumerable]
enum_red [in Undecidability.Reductions]
enum_PCP' [in Undecidability.PCP]
enum_prv [in Undecidability.Deduction]
enum_enumT [in Undecidability.DecidableEnumerable]
enum_count [in Undecidability.DecidableEnumerable]
enum_to_cumulative [in Undecidability.DecidableEnumerable]
equi_rotate [in Undecidability.Prelim]
equi_shift [in Undecidability.Prelim]
equi_swap [in Undecidability.Prelim]
equi_dup [in Undecidability.Prelim]
equi_push [in Undecidability.Prelim]
eval_empty [in Undecidability.Deduction]
eval_ext [in Undecidability.Deduction]
eval_ext_p [in Undecidability.Deduction]
eval_invar [in Undecidability.Kripke]
F
FG [in Undecidability.Infinite]filter_comm [in Undecidability.Prelim]
filter_and [in Undecidability.Prelim]
filter_pq_eq [in Undecidability.Prelim]
filter_pq_mono [in Undecidability.Prelim]
filter_fst' [in Undecidability.Prelim]
filter_fst [in Undecidability.Prelim]
filter_app [in Undecidability.Prelim]
filter_id [in Undecidability.Prelim]
filter_mono [in Undecidability.Prelim]
filter_incl [in Undecidability.Prelim]
form_discrete [in Undecidability.BPCP_FOL]
form_logic_ind_subst [in Undecidability.Deduction]
form_ind_subst [in Undecidability.Deduction]
form_frag_ind [in Undecidability.FOL]
F_sur [in Undecidability.Infinite]
F_inj [in Undecidability.Infinite]
F_inj' [in Undecidability.Infinite]
F_lt [in Undecidability.Infinite]
F_el [in Undecidability.Infinite]
F_nel [in Undecidability.Infinite]
f_sur [in Undecidability.Infinite]
G
gen [in Undecidability.Infinite]gen_le_f [in Undecidability.Infinite]
gen_spec [in Undecidability.Infinite]
gen_weakening [in Undecidability.Weakening]
GF [in Undecidability.Infinite]
I
IB_F [in Undecidability.BPCP_FOL]IB_F3 [in Undecidability.BPCP_FOL]
IB_F2 [in Undecidability.BPCP_FOL]
IB_F1 [in Undecidability.BPCP_FOL]
IB_stable [in Undecidability.BPCP_FOL]
IB_drv [in Undecidability.BPCP_FOL]
IB_enc [in Undecidability.BPCP_FOL]
IB_prep [in Undecidability.BPCP_FOL]
impl_prv [in Undecidability.BPCP_FOL]
impl_trans [in Undecidability.BPCP_CND]
impl_sat' [in Undecidability.Semantics]
impl_sat [in Undecidability.Semantics]
impl_ksat' [in Undecidability.Kripke]
impl_ksat [in Undecidability.Kripke]
incl_app_left [in Undecidability.Prelim]
incl_lrcons [in Undecidability.Prelim]
incl_rcons [in Undecidability.Prelim]
incl_lcons [in Undecidability.Prelim]
incl_shift [in Undecidability.Prelim]
incl_nil_eq [in Undecidability.Prelim]
incl_map [in Undecidability.Prelim]
incl_sing [in Undecidability.Prelim]
incl_nil [in Undecidability.Prelim]
incl_dec [in Undecidability.Deduction]
inf_quasi_nat [in Undecidability.Infinite]
inf_form [in Undecidability.FOL]
inf_term [in Undecidability.FOL]
in_rem_iff [in Undecidability.Prelim]
in_filter_iff [in Undecidability.Prelim]
in_concat_iff [in Undecidability.Prelim]
in_cons_neq [in Undecidability.Prelim]
in_sing [in Undecidability.Prelim]
in_omap_iff [in Undecidability.Prelim]
iprep_app [in Undecidability.BPCP_FOL]
iprep_eval [in Undecidability.BPCP_FOL]
K
kprv_unenum [in Undecidability.BPCP_IFOL]kprv_undec [in Undecidability.BPCP_IFOL]
kprv_red [in Undecidability.BPCP_IFOL]
kripke_tarski [in Undecidability.Kripke]
ksatis_enum [in Undecidability.BPCP_IFOL]
ksatis_undec [in Undecidability.BPCP_IFOL]
ksatis_red [in Undecidability.BPCP_IFOL]
ksatis_satis [in Undecidability.Kripke]
ksat_ext [in Undecidability.Kripke]
ksat_ext_p [in Undecidability.Kripke]
ksat_iff [in Undecidability.Kripke]
ksat_mon [in Undecidability.Kripke]
ksoundness [in Undecidability.Kripke]
ksoundness' [in Undecidability.Kripke]
kvalid_unenum [in Undecidability.BPCP_IFOL]
kvalid_undec [in Undecidability.BPCP_IFOL]
kvalid_red [in Undecidability.BPCP_IFOL]
kvalid_valid [in Undecidability.Kripke]
L
list_cc [in Undecidability.Prelim]list_exists_not_incl [in Undecidability.Prelim]
list_exists_DM [in Undecidability.Prelim]
list_cycle [in Undecidability.Prelim]
list_ind_ne [in Undecidability.Prelim]
LL_F [in Undecidability.Infinite]
LL_f [in Undecidability.Infinite]
LL_cum [in Undecidability.Infinite]
lt_acc [in Undecidability.Infinite]
LX_NoDup [in Undecidability.Infinite]
LX_el [in Undecidability.Infinite]
LX_len [in Undecidability.Infinite]
M
make_fresh [in Undecidability.Semantics]mkfresh_spec [in Undecidability.Semantics]
MND_CND [in Undecidability.BPCP_CND]
MND_IND [in Undecidability.Deduction]
MP_Post [in Undecidability.MarkovPost]
MP_enum_stable [in Undecidability.MarkovPost]
MP_to_decMP [in Undecidability.MarkovPost]
mu_least [in Undecidability.MarkovPost]
M_stable [in Undecidability.BPCP_FOL]
N
ND_CND [in Undecidability.Weakening]NonStan.IB_nonstandard [in Undecidability.BPCP_FOL]
NonStan.IB_F [in Undecidability.BPCP_FOL]
NonStan.IB_F2 [in Undecidability.BPCP_FOL]
NonStan.IB_F1 [in Undecidability.BPCP_FOL]
NonStan.IB_deriv' [in Undecidability.BPCP_FOL]
NonStan.IB_deriv [in Undecidability.BPCP_FOL]
NonStan.IB_enc [in Undecidability.BPCP_FOL]
NonStan.IB_eval_None [in Undecidability.BPCP_FOL]
NonStan.IB_eval_Some [in Undecidability.BPCP_FOL]
not_coenumerable [in Undecidability.Reductions]
not_decidable [in Undecidability.Reductions]
not_in_cons [in Undecidability.Prelim]
nthe_app_l [in Undecidability.Prelim]
nthe_length [in Undecidability.Prelim]
P
pairs_retract [in Undecidability.DecidableEnumerable]Post_MP [in Undecidability.MarkovPost]
Post_to' [in Undecidability.MarkovPost]
pos_length [in Undecidability.Prelim]
pos_nth [in Undecidability.Prelim]
pos_nthe [in Undecidability.Prelim]
prep_vars [in Undecidability.BPCP_FOL]
prep_subst [in Undecidability.BPCP_FOL]
projection [in Undecidability.DecidableEnumerable]
projection' [in Undecidability.DecidableEnumerable]
prv_unenum [in Undecidability.BPCP_FOL]
prv_undec [in Undecidability.BPCP_FOL]
prv_red [in Undecidability.BPCP_FOL]
prv_ind_min [in Undecidability.Deduction]
R
reduces_transitive [in Undecidability.Reductions]red_comp [in Undecidability.Reductions]
rem_inclr [in Undecidability.Prelim]
rem_reorder [in Undecidability.Prelim]
rem_id [in Undecidability.Prelim]
rem_fst' [in Undecidability.Prelim]
rem_fst [in Undecidability.Prelim]
rem_comm [in Undecidability.Prelim]
rem_equi [in Undecidability.Prelim]
rem_app' [in Undecidability.Prelim]
rem_app [in Undecidability.Prelim]
rem_neq [in Undecidability.Prelim]
rem_in [in Undecidability.Prelim]
rem_cons' [in Undecidability.Prelim]
rem_cons [in Undecidability.Prelim]
rem_mono [in Undecidability.Prelim]
rem_incl [in Undecidability.Prelim]
rem_not_in [in Undecidability.Prelim]
ren_swap_ctx [in Undecidability.Weakening]
ren_subst [in Undecidability.Weakening]
ren_subst_t [in Undecidability.Weakening]
ren_ext_ctx [in Undecidability.Weakening]
ren_ext [in Undecidability.Weakening]
ren_ext_t [in Undecidability.Weakening]
ren_comp_ctx [in Undecidability.Weakening]
ren_comp [in Undecidability.Weakening]
ren_comp_t [in Undecidability.Weakening]
ren_ctx_id [in Undecidability.Weakening]
ren_id [in Undecidability.Weakening]
ren_id_t [in Undecidability.Weakening]
S
satis_enum [in Undecidability.BPCP_FOL]satis_undec [in Undecidability.BPCP_FOL]
satis_red [in Undecidability.BPCP_FOL]
sat_ext_p_list [in Undecidability.Deduction]
sat_ext [in Undecidability.Deduction]
sat_ext_p [in Undecidability.Deduction]
size_induction_dep [in Undecidability.Prelim]
size_induction [in Undecidability.Prelim]
size_subst [in Undecidability.Deduction]
soundness [in Undecidability.Deduction]
soundness' [in Undecidability.Deduction]
stable_red [in Undecidability.MarkovPost]
stack_enum [in Undecidability.PCP]
stack_discrete [in Undecidability.PCP]
stack_quasi_nat [in Undecidability.Infinite]
stack_infinite [in Undecidability.Infinite]
substconst_sat [in Undecidability.Deduction]
substconst_ksat [in Undecidability.Kripke]
subst_sat [in Undecidability.Deduction]
subst_eval [in Undecidability.Deduction]
subst_lift [in Undecidability.Deduction]
subst_ksat [in Undecidability.Kripke]
sub_dec [in Undecidability.Infinite]
T
TM_sat [in Undecidability.Semantics]to_dec [in Undecidability.Prelim]
trans_trans [in Undecidability.BPCP_CND]
trans_subst [in Undecidability.BPCP_CND]
T_list_el [in Undecidability.DecidableEnumerable]
T_list_cum [in Undecidability.DecidableEnumerable]
T_prod_el [in Undecidability.DecidableEnumerable]
T_prod_cum [in Undecidability.DecidableEnumerable]
T_nat_length [in Undecidability.DecidableEnumerable]
T_nat_in [in Undecidability.DecidableEnumerable]
V
valid_unenum [in Undecidability.BPCP_FOL]valid_undec [in Undecidability.BPCP_FOL]
valid_red [in Undecidability.BPCP_FOL]
valid_satis [in Undecidability.BPCP_FOL]
vars_t_ren [in Undecidability.Weakening]
W
Weak [in Undecidability.Weakening]weakPost [in Undecidability.MarkovPost]
X
X_gen [in Undecidability.Infinite]Constructor Index
A
All [in Undecidability.FOL]AllE [in Undecidability.Deduction]
AllI [in Undecidability.Deduction]
C
cBPCP [in Undecidability.PCP]class [in Undecidability.Deduction]
Ctx [in Undecidability.Deduction]
D
der_cons [in Undecidability.PCP]der_sing [in Undecidability.PCP]
DN [in Undecidability.Deduction]
E
EqType [in Undecidability.Prelim]Exp [in Undecidability.Deduction]
F
Fal [in Undecidability.FOL]frag [in Undecidability.FOL]
full [in Undecidability.FOL]
I
ImpE [in Undecidability.Deduction]ImpI [in Undecidability.Deduction]
Impl [in Undecidability.FOL]
intu [in Undecidability.Deduction]
P
P [in Undecidability.FOL]Pr [in Undecidability.FOL]
Q
Q [in Undecidability.FOL]T
t_e [in Undecidability.FOL]t_f [in Undecidability.FOL]
V
V [in Undecidability.FOL]Inductive Index
B
BPCP [in Undecidability.PCP]D
derivable [in Undecidability.PCP]F
form [in Undecidability.FOL]L
logic [in Undecidability.FOL]N
nd [in Undecidability.Deduction]P
prv [in Undecidability.Deduction]T
term [in Undecidability.FOL]Projection Index
C
cum_T [in Undecidability.DecidableEnumerable]E
el_T [in Undecidability.DecidableEnumerable]eqType_dec [in Undecidability.Prelim]
eqType_X [in Undecidability.Prelim]
H
He [in Undecidability.Kripke]Hf [in Undecidability.Kripke]
HP [in Undecidability.Kripke]
HQ [in Undecidability.Kripke]
I
i_Q [in Undecidability.Semantics]i_P [in Undecidability.Semantics]
i_e [in Undecidability.Semantics]
i_f [in Undecidability.Semantics]
L
L_T [in Undecidability.DecidableEnumerable]N
nodes [in Undecidability.Kripke]R
reachable [in Undecidability.Kripke]reach_tran [in Undecidability.Kripke]
reach_refl [in Undecidability.Kripke]
W
world [in Undecidability.Kripke]world_f [in Undecidability.Kripke]
Section Index
B
BPCP_CND [in Undecidability.BPCP_CND]E
enumerable_list.fixL [in Undecidability.DecidableEnumerable]enumerable_list [in Undecidability.DecidableEnumerable]
enumerable_prod.fixLs [in Undecidability.DecidableEnumerable]
enumerable_prod [in Undecidability.DecidableEnumerable]
enumerable_enum [in Undecidability.DecidableEnumerable]
enum_red [in Undecidability.Reductions]
enum_enumerable [in Undecidability.DecidableEnumerable]
Equi [in Undecidability.Prelim]
F
Filter [in Undecidability.Prelim]G
Gen2Inf [in Undecidability.Infinite]I
Inclusion [in Undecidability.Prelim]Inf2Gen [in Undecidability.Infinite]
K
Kripke [in Undecidability.Kripke]kvalidity [in Undecidability.BPCP_IFOL]
M
Membership [in Undecidability.Prelim]N
neList [in Undecidability.Prelim]NonStan.Nonstan [in Undecidability.BPCP_FOL]
P
Positions [in Undecidability.Prelim]R
Removal [in Undecidability.Prelim]S
Semantics [in Undecidability.Semantics]T
TM [in Undecidability.Semantics]V
validity [in Undecidability.BPCP_FOL]Instance Index
A
and_dec [in Undecidability.Prelim]app_equi_proper [in Undecidability.Prelim]
app_incl_proper [in Undecidability.Prelim]
B
bool_eq_dec [in Undecidability.Prelim]bool_dec [in Undecidability.Prelim]
C
cons_equi_proper [in Undecidability.Prelim]cons_incl_proper [in Undecidability.Prelim]
D
dec_logic [in Undecidability.FOL]dec_term [in Undecidability.FOL]
E
el_dec [in Undecidability.Infinite]Empty_set_eq_dec [in Undecidability.Prelim]
enumerable_list [in Undecidability.DecidableEnumerable]
enumT_form [in Undecidability.FOL]
enumT_term [in Undecidability.FOL]
enumT_nat [in Undecidability.DecidableEnumerable]
enum_bool [in Undecidability.DecidableEnumerable]
equi_Equivalence [in Undecidability.Prelim]
eq_dec_form [in Undecidability.FOL]
F
False_eq_dec [in Undecidability.Prelim]False_dec [in Undecidability.Prelim]
I
IB [in Undecidability.BPCP_FOL]iff_dec [in Undecidability.Prelim]
impl_dec [in Undecidability.Prelim]
incl_equi_proper [in Undecidability.Prelim]
incl_preorder [in Undecidability.Prelim]
interp_kripke [in Undecidability.Kripke]
in_equi_proper [in Undecidability.Prelim]
in_incl_proper [in Undecidability.Prelim]
iUnit [in Undecidability.BPCP_CND]
L
list_exists_dec [in Undecidability.Prelim]list_forall_dec [in Undecidability.Prelim]
list_in_dec [in Undecidability.Prelim]
list_eq_dec [in Undecidability.Prelim]
N
nat_eq_dec [in Undecidability.Prelim]NonStan.IB [in Undecidability.BPCP_FOL]
not_dec [in Undecidability.Prelim]
O
option_eq_dec [in Undecidability.Prelim]or_dec [in Undecidability.Prelim]
P
prod_eq_dec [in Undecidability.Prelim]prod_enumerable [in Undecidability.DecidableEnumerable]
S
sum_eq_dec [in Undecidability.Prelim]T
TM [in Undecidability.Semantics]True_eq_dec [in Undecidability.Prelim]
True_dec [in Undecidability.Prelim]
U
unit_eq_dec [in Undecidability.Prelim]Abbreviation Index
C
const [in Undecidability.Semantics]D
Decb [in Undecidability.Prelim]M
mu' [in Undecidability.MarkovPost]N
nthe [in Undecidability.Prelim]nthe [in Undecidability.Prelim]
P
par [in Undecidability.FOL]R
R [in Undecidability.MarkovPost]S
sem_imp [in Undecidability.Kripke]U
u [in Undecidability.BPCP_FOL]V
v [in Undecidability.BPCP_FOL]var [in Undecidability.FOL]
Definition Index
B
BSRS [in Undecidability.PCP]C
card [in Undecidability.PCP]cast [in Undecidability.Deduction]
compl [in Undecidability.DecidableEnumerable]
consts [in Undecidability.Semantics]
consts_l [in Undecidability.Semantics]
consts_t [in Undecidability.Semantics]
cprv [in Undecidability.BPCP_CND]
ctx_S [in Undecidability.BPCP_FOL]
cumulative [in Undecidability.DecidableEnumerable]
D
Dec [in Undecidability.Prelim]dec [in Undecidability.Prelim]
decidable [in Undecidability.DecidableEnumerable]
derivable' [in Undecidability.BPCP_FOL]
discrete [in Undecidability.DecidableEnumerable]
disjoint [in Undecidability.Prelim]
dnQ [in Undecidability.BPCP_CND]
dummy [in Undecidability.Infinite]
E
emb_trans [in Undecidability.Kripke]enc [in Undecidability.BPCP_FOL]
enum [in Undecidability.DecidableEnumerable]
enumerable [in Undecidability.DecidableEnumerable]
enumerable__T [in Undecidability.DecidableEnumerable]
env [in Undecidability.Semantics]
equi [in Undecidability.Prelim]
eval [in Undecidability.Semantics]
F
F [in Undecidability.BPCP_FOL]F [in Undecidability.Infinite]
f [in Undecidability.Infinite]
filter [in Undecidability.Prelim]
fresh [in Undecidability.Semantics]
fullsatis [in Undecidability.Semantics]
fun_comp [in Undecidability.Weakening]
F_stack [in Undecidability.Infinite]
F1 [in Undecidability.BPCP_FOL]
F2 [in Undecidability.BPCP_FOL]
F3 [in Undecidability.BPCP_FOL]
G
G [in Undecidability.Infinite]generating [in Undecidability.Infinite]
gen' [in Undecidability.Infinite]
I
impl [in Undecidability.FOL]inclp [in Undecidability.Prelim]
infinite [in Undecidability.Infinite]
injective [in Undecidability.Infinite]
iprep [in Undecidability.BPCP_FOL]
K
kcast [in Undecidability.Kripke]ksat [in Undecidability.Kripke]
ksatis [in Undecidability.Kripke]
kvalid [in Undecidability.Kripke]
L
L [in Undecidability.Reductions]ldecidable [in Undecidability.MarkovPost]
le_f [in Undecidability.Infinite]
lift [in Undecidability.Deduction]
LL [in Undecidability.Infinite]
LX [in Undecidability.Infinite]
L_PCP [in Undecidability.PCP]
L_ded [in Undecidability.Deduction]
L_form [in Undecidability.FOL]
L_term [in Undecidability.FOL]
M
mkfresh [in Undecidability.Semantics]MP [in Undecidability.MarkovPost]
mu [in Undecidability.MarkovPost]
O
ofNat [in Undecidability.DecidableEnumerable]omap [in Undecidability.Prelim]
P
PCP [in Undecidability.PCP]pos [in Undecidability.Prelim]
POST [in Undecidability.MarkovPost]
POST' [in Undecidability.MarkovPost]
prep [in Undecidability.BPCP_FOL]
prv_intu [in Undecidability.Deduction]
prv_class [in Undecidability.Deduction]
prv_min [in Undecidability.Deduction]
Q
quasi_nat [in Undecidability.Infinite]R
reduces [in Undecidability.Reductions]rem [in Undecidability.Prelim]
ren [in Undecidability.Weakening]
ren_ctx [in Undecidability.Weakening]
ren_t [in Undecidability.Weakening]
R_nat_nat [in Undecidability.DecidableEnumerable]
S
sat [in Undecidability.Semantics]satis [in Undecidability.Semantics]
singles [in Undecidability.Weakening]
size [in Undecidability.Deduction]
SRS [in Undecidability.PCP]
stable [in Undecidability.MarkovPost]
stack [in Undecidability.PCP]
string [in Undecidability.PCP]
subst [in Undecidability.Semantics]
subst_t [in Undecidability.Semantics]
surjective [in Undecidability.Infinite]
symbol [in Undecidability.PCP]
T
tau1 [in Undecidability.PCP]tau2 [in Undecidability.PCP]
trans [in Undecidability.BPCP_CND]
T_list [in Undecidability.DecidableEnumerable]
T_prod [in Undecidability.DecidableEnumerable]
T_ [in Undecidability.DecidableEnumerable]
U
UA [in Undecidability.BPCP_FOL]update [in Undecidability.Semantics]
V
valid [in Undecidability.Semantics]valid_L [in Undecidability.Semantics]
vars_t [in Undecidability.Semantics]
Record Index
E
embedding [in Undecidability.Kripke]enumT [in Undecidability.DecidableEnumerable]
eqType [in Undecidability.Prelim]
I
interp [in Undecidability.Semantics]K
kmodel [in Undecidability.Kripke]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (646 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (312 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (102 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |