Global Index

other

(525 entries)

Notation Index

other

(13 entries)

Variable Index

other

(33 entries)

Library Index

other

(9 entries)

Lemma Index

other

(294 entries)

Constructor Index

other

(25 entries)

Axiom Index

other

(1 entry)

Inductive Index

other

(13 entries)

Projection Index

other

(6 entries)

Section Index

other

(19 entries)

Instance Index

other

(29 entries)

Abbreviation Index

other

(1 entry)

Definition Index

other

(80 entries)

Record Index

other

(2 entries)

Global Index

A

A [axiom, in NTA]
accept_in_states [lemma, in NTA]
Action [section, in Tree]
Action.HW [variable, in Tree]
Action.t [variable, in Tree]
AD1 [constructor, in NTA]
AD2 [constructor, in NTA]
AD3 [constructor, in NTA]
all_true_map_pw_map [lemma, in Lists]
all_true_map_pw [lemma, in Lists]
all_true_true [lemma, in Lists]
all_true [definition, in Lists]
all_phis [definition, in NTA]
all_phis' [definition, in NTA]
all_conts [definition, in NTA]
all_assns [definition, in NTA]
and_dec [instance, in Base]
apply_perm [definition, in Tree]
app_equi [lemma, in Lists]
app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]

B

Base [library]
bind_free_name [lemma, in NuTree]
BN [definition, in NuTree]
BN_equiv [lemma, in NuTree]
BN_no_nusk [lemma, in NuTree]
BN_no_nus [lemma, in NuTree]
BN_in_sub [lemma, in NuTree]
bool_eq_dec [instance, in Base]
bool_dec [instance, in Base]
bool_Prop_false [lemma, in Base]
bool_Prop_true [lemma, in Base]
bool2Prop [definition, in Base]
bound_in_names [lemma, in NuTree]

C

candidates [definition, in NtlDec]
candidates_valid [lemma, in NtlDec]
candsd1 [definition, in NTA]
candsd2 [definition, in NTA]
candsd3 [definition, in NTA]
cfind [lemma, in Base]
char_eq_dec [instance, in Perm]
compose [definition, in Perm]
compose_renaming [lemma, in NtlEqui]
concat_map_equi [lemma, in Lists]
concat_equi [lemma, in Lists]
concat_incl_list [lemma, in Lists]
concat_map_el [lemma, in Lists]
concat_nil' [lemma, in Lists]
concat_el_sub [lemma, in Lists]
concat_el [lemma, in Lists]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
Correct [section, in NtlDec]
Correct.A [variable, in NtlDec]
Correct.HW1 [variable, in NtlDec]
Correct.HW2 [variable, in NtlDec]
Correct.n [variable, in NtlDec]
Correct.t [variable, in NtlDec]

D

Dec [definition, in Base]
dec [definition, in Base]
Decb [abbreviation, in Base]
dec_accept_p [lemma, in NTA]
dec_accept_s [lemma, in NTA]
dec_accept [lemma, in NTA]
dec_transfer [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
Dec_auto_not [lemma, in Base]
Dec_auto [lemma, in Base]
Dec_reflect_eq [lemma, in Base]
Dec_reflect [lemma, in Base]
dec_ntl [lemma, in NtlDec]
dec2bool [definition, in Base]
Delta1 [definition, in NTA]
Delta2 [definition, in NTA]
Delta3 [definition, in NTA]
Depth [section, in NuTree]
dl_induction [lemma, in Lists]
dmap_nu_some_true [lemma, in NtlDec]
dmap_nu [definition, in NtlDec]
DM_exists [lemma, in Base]
DM_or [lemma, in Base]
DNLs [constructor, in NuTree]
DNNu [constructor, in NuTree]
DNT [definition, in NuTree]
DTR [definition, in Tree]
D1 [definition, in NTA]
D1' [projection, in NTA]
D2 [definition, in NTA]
D2' [projection, in NTA]
D3 [definition, in NTA]
D3' [projection, in NTA]

E

eqType [record, in Base]
EqType [constructor, in Base]
eqType_CS [definition, in Base]
eqType_dec [projection, in Base]
eqType_X [projection, in Base]
Equality [section, in NuTreeBonus]
Equality.HW1 [variable, in NuTreeBonus]
Equality.HW2 [variable, in NuTreeBonus]
Equality.n [variable, in NuTreeBonus]
Equality.n' [variable, in NuTreeBonus]
Equi [section, in Base]
equi [definition, in Base]
Equivariance [section, in NuTree]
Equivariance.HW [variable, in NuTree]
Equivariance.n [variable, in NuTree]
Equivariance.p [variable, in NuTree]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]

F

False_dec [instance, in Base]
filter [definition, in Base]
Filter [section, in Base]
filter_fst' [lemma, in Base]
filter_fst [lemma, in Base]
filter_app [lemma, in Base]
filter_id [lemma, in Base]
filter_incl [lemma, in Base]
Filter.X [variable, in Base]
FN [definition, in NuTree]
FN_sub_incl [lemma, in NtlEqui]
FN_sub_other [lemma, in NtlEqui]
FN_nu_sub [lemma, in NtlEqui]
FN_equiv_shift [lemma, in NuTree]
FN_equiv [lemma, in NuTree]
FN_in_sub [lemma, in NuTree]
free_in_renaming [lemma, in NtlEqui]
free_name_in_renaming' [lemma, in NtlEqui]
free_name_in_renaming [lemma, in NtlEqui]
free_sub_not [lemma, in NuTree]
free_in_names [lemma, in NuTree]
fresh [definition, in NuTree]
Freshness [section, in Lists]
freshness [lemma, in NuTree]
freshness' [lemma, in Lists]
fresh_name [lemma, in NuTree]
fresh' [definition, in Lists]

G

gt_name_list_max [lemma, in Lists]
gt_list_max [lemma, in Lists]
gt_depth_sub [lemma, in NuTree]

I

iff_dec [instance, in Base]
impl_dec [instance, in Base]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_cons [lemma, in Lists]
incl_equi_proper [instance, in Base]
incl_preorder [instance, in Base]
incl_app_left [lemma, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
Inv [definition, in Perm]
inv_comm [lemma, in Perm]
in_map2_iff [lemma, in Lists]
in_candsd3 [lemma, in NTA]
in_candsd2 [lemma, in NTA]
in_candsd1 [lemma, in NTA]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_incl_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_dmap_nu_iff [lemma, in NtlDec]

L

len_plist [lemma, in Lists]
Lists [library]
list_sum_zero [lemma, in Lists]
list_sum [definition, in Lists]
list_max_max [lemma, in Lists]
list_max_cons'' [lemma, in Lists]
list_max_cons' [lemma, in Lists]
list_max_dep' [lemma, in Lists]
list_max [definition, in Lists]
list_max' [definition, in Lists]
list_prop_rel [lemma, in Lists]
list_nominal [lemma, in Lists]
list_swap_perm [lemma, in Lists]
list_assoc [lemma, in Lists]
list_id [lemma, in Lists]
list_cc [lemma, in Base]
list_exists_not_incl [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_in_dec [instance, in Base]
list_cycle [lemma, in Base]
list_eq_dec [instance, in Base]
lPhi [definition, in NTA]
lphi_alt [lemma, in NTA]
lphi_alt' [lemma, in NTA]

M

map_pw_map_eq [lemma, in Lists]
map_pw_map [lemma, in Lists]
map_pw [definition, in Lists]
map_eq [lemma, in Lists]
map_nth_indep [lemma, in Lists]
map2 [definition, in Lists]
map2_all_true [lemma, in Lists]
Membership [section, in Base]
Membership.X [variable, in Base]

N

Name [definition, in Perm]
NameF [definition, in Perm]
names [definition, in Tree]
name_list_max_max [lemma, in Lists]
name_list_max [definition, in Lists]
name_assoc [lemma, in Perm]
name_id [lemma, in Perm]
name_rk_neq [lemma, in Perm]
name_eq [lemma, in Perm]
NatNumList [section, in Lists]
nat_eq_dec [instance, in Base]
nil_el_eq [lemma, in Base]
nonphi [definition, in NTA]
NoNus [inductive, in NuTree]
nonusA [constructor, in NuTree]
NoNusk [inductive, in NuTree]
nonuskA [constructor, in NuTree]
nonuskB [constructor, in NuTree]
not_disj [lemma, in Perm]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
no_nus_nu_number_z' [lemma, in NuTreeBonus]
no_nus_nu_number_z [lemma, in NuTreeBonus]
no_nusk_equiv [lemma, in NuTree]
NTA [record, in NTA]
NTA [library]
NtaAccept [inductive, in NTA]
NtAccept [inductive, in NuTree]
NtAction [section, in NuTree]
NtAction.HW [variable, in NuTree]
NtAction.n [variable, in NuTree]
nta_ntl_reject' [lemma, in NTA]
nta_ntl_reject [lemma, in NTA]
nta_accept_has_name [lemma, in NTA]
nta_swap_phi [lemma, in NTA]
nta_names [definition, in NTA]
ntd_S' [lemma, in NuTree]
ntd_S [lemma, in NuTree]
Nteq [inductive, in NuTreeBonus]
NteqA [constructor, in NuTreeBonus]
NteqB [constructor, in NuTreeBonus]
nth_el_indx_map [lemma, in Lists]
nth_el_indx [lemma, in Lists]
NtlDec [library]
NtlEq [definition, in NtlEqui]
NtlEqui [library]
NtlRho [definition, in NtlEqui]
ntl_refl [lemma, in NuTreeBonus]
ntl_nu_push [lemma, in NtlEqui]
ntl_nu_push'' [lemma, in NtlEqui]
ntl_nu_push' [lemma, in NtlEqui]
ntl_nusk_list [lemma, in NtlEqui]
ntl_pure_list [lemma, in NtlEqui]
ntl_nu_swap [lemma, in NtlEqui]
ntl_nu_swap' [lemma, in NtlEqui]
ntl_nu_rename [lemma, in NtlEqui]
ntl_nu_rename_2 [lemma, in NtlEqui]
ntl_nu_rename_1 [lemma, in NtlEqui]
ntl_nu_indep [lemma, in NtlEqui]
ntl_nu_add [lemma, in NtlEqui]
ntl_strengthening [lemma, in NtlEqui]
ntl_nu_ignore [lemma, in NtlEqui]
ntl_weakening [lemma, in NtlEqui]
ntl_alpha_eq [lemma, in NtlEqui]
ntl_closed [lemma, in NtlEqui]
ntl_renaming [lemma, in NtlEqui]
ntl_renaming'' [lemma, in NtlEqui]
ntl_renaming' [lemma, in NtlEqui]
ntl_eq_refl [lemma, in NtlEqui]
ntl_equiv [lemma, in NuTree]
ntl_equiv'' [lemma, in NuTree]
ntl_equiv' [lemma, in NuTree]
ntl_swap_list [lemma, in NuTree]
ntl_name_not_in [lemma, in NuTree]
ntl_name_in [lemma, in NuTree]
ntl_name [lemma, in NuTree]
ntl_dec_correct [lemma, in NtlDec]
ntl_dec_correct_2 [lemma, in NtlDec]
ntl_dec_correct_1 [lemma, in NtlDec]
ntl_dec_depth [lemma, in NtlDec]
ntl_sim [lemma, in NtlDec]
ntl_dec_similar [lemma, in NtlDec]
ntl_dec_true_name' [lemma, in NtlDec]
ntl_dec_true_name [lemma, in NtlDec]
ntl_dec [definition, in NtlDec]
NtStr [inductive, in NuTree]
NtStrA [constructor, in NuTree]
NtStrB [constructor, in NuTree]
Ntwr [inductive, in NuTree]
ntwrA [constructor, in NuTree]
ntwrB [constructor, in NuTree]
nt_eq_dec [instance, in NuTreeBonus]
nt_eq_correct [lemma, in NuTreeBonus]
nt_eq_correct_2 [lemma, in NuTreeBonus]
nt_eq_correct_1 [lemma, in NuTreeBonus]
nt_eq [definition, in NuTreeBonus]
nt_str_renaming [lemma, in NtlEqui]
nt_str_FN [lemma, in NuTree]
nt_str_dec [lemma, in NuTree]
nt_str_correct [lemma, in NuTree]
nt_str_correct_2 [lemma, in NuTree]
nt_str_correct_1 [lemma, in NuTree]
nt_str [definition, in NuTree]
nt_names_equiv [lemma, in NuTree]
nt_assoc3 [lemma, in NuTree]
nt_nominal [lemma, in NuTree]
nt_swap_perm'' [lemma, in NuTree]
nt_swap_perm' [lemma, in NuTree]
nt_swap_perm [lemma, in NuTree]
nt_depth_perm [lemma, in NuTree]
nt_perm_wr [lemma, in NuTree]
nt_perm_apply_inv [lemma, in NuTree]
nt_sym [lemma, in NuTree]
nt_id [lemma, in NuTree]
nt_assoc [lemma, in NuTree]
nt_apply_perm_step [lemma, in NuTree]
nt_apply_perm [definition, in NuTree]
nt_names_inhab [lemma, in NuTree]
nt_name_in_sub [lemma, in NuTree]
nt_names [definition, in NuTree]
nt_decrease' [lemma, in NuTree]
nt_decrease [lemma, in NuTree]
nt_depth [definition, in NuTree]
nt_wr_sub' [lemma, in NuTree]
nt_wr_sub [lemma, in NuTree]
Nu [constructor, in NuTree]
NuIndep [section, in NtlEqui]
NuIndep.HW1 [variable, in NtlEqui]
NuIndep.n [variable, in NtlEqui]
num_max_le [lemma, in Lists]
num_max_comm [lemma, in Lists]
num_max_or [lemma, in Lists]
num_max_zero [lemma, in Lists]
num_max [definition, in Lists]
NuNumber [definition, in NuTreeBonus]
NuPush [section, in NtlEqui]
NuRename [section, in NtlEqui]
NuRename.A [variable, in NtlEqui]
NuRename.HW1 [variable, in NtlEqui]
NuRename.n [variable, in NtlEqui]
NuSwap [section, in NtlEqui]
NuSwap.A [variable, in NtlEqui]
NuSwap.HW1 [variable, in NtlEqui]
NuSwap.n [variable, in NtlEqui]
NuTree [inductive, in NuTree]
NuTree [library]
NuTreeBonus [library]
nu_swap_FN [lemma, in NtlEqui]
nu_FN' [lemma, in NtlEqui]
nu_FN [lemma, in NtlEqui]

O

option_eq_dec [instance, in NTA]
or_dec [instance, in Base]

P

Perm [definition, in Perm]
Perm [library]
perm_list_shift [lemma, in Lists]
perm_list_el [lemma, in Lists]
perm_list_el'' [lemma, in Lists]
perm_list_el' [lemma, in Lists]
perm_list_inv [lemma, in Lists]
perm_list_step [lemma, in Lists]
perm_list [definition, in Lists]
perm_rk [lemma, in Perm]
perm_inv_perm [lemma, in Perm]
perm_compose_perm [lemma, in Perm]
perm_inv_compose [lemma, in Perm]
perm_inv_shift [lemma, in Perm]
perm_inj [lemma, in Perm]
perm_inj' [lemma, in Perm]
perm_id [lemma, in Perm]
perm_inv' [lemma, in Perm]
perm_inv [lemma, in Perm]
perm_apply_inv [lemma, in Tree]
perm_tree_wr [lemma, in Tree]
Phi [definition, in NTA]
Phi' [definition, in NTA]
plist [inductive, in Lists]
pListC [constructor, in Lists]
pListN [constructor, in Lists]
plist_eq [lemma, in Lists]
plist_len [lemma, in Lists]
prod_eq_dec [instance, in Base]
PSim [inductive, in NtlDec]
PSimA [constructor, in NtlDec]
PSimB [constructor, in NtlDec]
psim_perm' [lemma, in NtlDec]
psim_perm [lemma, in NtlDec]
pure_nu_number_z [lemma, in NuTreeBonus]
pure_no_nus [lemma, in NuTreeBonus]

Q

Q [definition, in NTA]
qlist [definition, in NTA]
qlist_correct [lemma, in NTA]
Q' [definition, in NTA]

R

rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_id [lemma, in NuTree]
rem_equiv' [lemma, in NuTree]
rem_equiv [lemma, in NuTree]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_equi [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
Renaming [definition, in NtlEqui]
Renaming [section, in NtlEqui]
renaming_invariant [lemma, in NtlEqui]
renaming_inverse [lemma, in NtlEqui]
renaming_nil [lemma, in NtlEqui]
renaming_sub' [lemma, in NtlEqui]
renaming_sub [lemma, in NtlEqui]
rep_nth_id [lemma, in Lists]
rep_nth_el' [lemma, in Lists]
rep_nth_indep [lemma, in Lists]
rep_nth_overwrite [lemma, in Lists]
rep_nth_el_or [lemma, in Lists]
rep_nth_el [lemma, in Lists]
rep_nth_exact [lemma, in Lists]
rep_nth_len' [lemma, in Lists]
rep_nth_len [lemma, in Lists]
rep_nth_nil [lemma, in Lists]
rep_nth [definition, in Lists]
rk [definition, in Perm]

S

s [definition, in NTA]
Sim [inductive, in NtlDec]
SimA [constructor, in NtlDec]
SimB [constructor, in NtlDec]
similar [definition, in NtlDec]
similar_correct' [lemma, in NtlDec]
similar_swap_perm [lemma, in NtlDec]
similar_equiv [lemma, in NtlDec]
similar_correct [lemma, in NtlDec]
sim_psim [lemma, in NtlDec]
sim_perm' [lemma, in NtlDec]
sim_perm [lemma, in NtlDec]
some_true_true [lemma, in Lists]
some_true [definition, in Lists]
states [definition, in NTA]
state_eq_dec' [instance, in NTA]
state_eq_dec [instance, in NTA]
step_var_agree [lemma, in NTA]
step_var_in_all [lemma, in NTA]
step_var [definition, in NTA]
Structure [section, in NuTree]
Structure.HW1 [variable, in NuTree]
Structure.HW2 [variable, in NuTree]
Structure.n [variable, in NuTree]
Structure.n' [variable, in NuTree]
sym_action_name [lemma, in Perm]
s' [projection, in NTA]

T

tdec [definition, in NTA]
tdec_p_correct [lemma, in NTA]
tdec_p_correct_2 [lemma, in NTA]
tdec_p_correct_1 [lemma, in NTA]
tdec_p [definition, in NTA]
tdec_s_correct [lemma, in NTA]
tdec_s_correct_2 [lemma, in NTA]
tdec_s_correct_1 [lemma, in NTA]
tdec_s [definition, in NTA]
tdec_correct [lemma, in NTA]
tdec_correct_2 [lemma, in NTA]
tdec_correct_1 [lemma, in NTA]
tdec_some_true [definition, in NTA]
tdec_all_true [definition, in NTA]
to_fun [definition, in NTA]
Tr [constructor, in NuTree]
TrA [constructor, in Tree]
transp [definition, in Perm]
transp_list_indep [lemma, in Lists]
transp_list_el [lemma, in Lists]
transp_FN' [lemma, in NtlEqui]
transp_FN [lemma, in NtlEqui]
transp_renaming [lemma, in NtlEqui]
transp_chain' [lemma, in Perm]
transp_chain'' [lemma, in Perm]
transp_chain [lemma, in Perm]
transp_diff [lemma, in Perm]
transp_id [lemma, in Perm]
transp_swap [lemma, in Perm]
transp_compose [lemma, in Perm]
transp_apply [lemma, in Perm]
transp_rk' [lemma, in Perm]
transp_perm_iff [lemma, in Perm]
transp_rk [lemma, in Perm]
transp_perm' [lemma, in Perm]
transp_perm [lemma, in Perm]
transp_inv [lemma, in Perm]
Tree [inductive, in Tree]
Tree [library]
treewrA [constructor, in Tree]
tree_name_free [lemma, in NuTree]
tree_nominal [lemma, in Tree]
tree_swap_perm [lemma, in Tree]
tree_sym [lemma, in Tree]
tree_id [lemma, in Tree]
tree_assoc [lemma, in Tree]
tree_wr_sub [lemma, in Tree]
tree_name_in_sub [lemma, in Tree]
True_dec [instance, in Base]
Twr [inductive, in Tree]
twr_ntwr [lemma, in NuTreeBonus]
t_to_nt_in [lemma, in NuTreeBonus]
t_to_nt [definition, in NuTreeBonus]

U

update [definition, in NTA]

other

_ *- _ [notation, in Lists]
_ == _ on _ [notation, in NTA]
_ El [ _ ] _ [notation, in NuTree]
_ *' _ [notation, in NuTree]
_ $ _ [notation, in Perm]
_ ** _ [notation, in Perm]
_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
_ *> _ [notation, in Tree]
eq_dec _ [notation, in Base]
% _ [notation, in NuTreeBonus]
| _ | [notation, in Base]