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 (525 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 (13 entries)
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 (33 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 (9 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 (294 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 (25 entries)
Axiom 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)
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 (13 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 (6 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 (19 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 (29 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 (1 entry)
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 (80 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 (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]



Notation Index

other

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



Variable Index

A

Action.HW [in Tree]
Action.t [in Tree]


C

Correct.A [in NtlDec]
Correct.HW1 [in NtlDec]
Correct.HW2 [in NtlDec]
Correct.n [in NtlDec]
Correct.t [in NtlDec]


E

Equality.HW1 [in NuTreeBonus]
Equality.HW2 [in NuTreeBonus]
Equality.n [in NuTreeBonus]
Equality.n' [in NuTreeBonus]
Equivariance.HW [in NuTree]
Equivariance.n [in NuTree]
Equivariance.p [in NuTree]
Equi.X [in Base]


F

Filter.X [in Base]


I

Inclusion.X [in Base]


M

Membership.X [in Base]


N

NtAction.HW [in NuTree]
NtAction.n [in NuTree]
NuIndep.HW1 [in NtlEqui]
NuIndep.n [in NtlEqui]
NuRename.A [in NtlEqui]
NuRename.HW1 [in NtlEqui]
NuRename.n [in NtlEqui]
NuSwap.A [in NtlEqui]
NuSwap.HW1 [in NtlEqui]
NuSwap.n [in NtlEqui]


R

Removal.X [in Base]


S

Structure.HW1 [in NuTree]
Structure.HW2 [in NuTree]
Structure.n [in NuTree]
Structure.n' [in NuTree]



Library Index

B

Base


L

Lists


N

NTA
NtlDec
NtlEqui
NuTree
NuTreeBonus


P

Perm


T

Tree



Lemma Index

A

accept_in_states [in NTA]
all_true_map_pw_map [in Lists]
all_true_map_pw [in Lists]
all_true_true [in Lists]
app_equi [in Lists]


B

bind_free_name [in NuTree]
BN_equiv [in NuTree]
BN_no_nusk [in NuTree]
BN_no_nus [in NuTree]
BN_in_sub [in NuTree]
bool_Prop_false [in Base]
bool_Prop_true [in Base]
bound_in_names [in NuTree]


C

candidates_valid [in NtlDec]
cfind [in Base]
compose_renaming [in NtlEqui]
concat_map_equi [in Lists]
concat_equi [in Lists]
concat_incl_list [in Lists]
concat_map_el [in Lists]
concat_nil' [in Lists]
concat_el_sub [in Lists]
concat_el [in Lists]


D

dec_accept_p [in NTA]
dec_accept_s [in NTA]
dec_accept [in NTA]
dec_transfer [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
Dec_auto_not [in Base]
Dec_auto [in Base]
Dec_reflect_eq [in Base]
Dec_reflect [in Base]
dec_ntl [in NtlDec]
dl_induction [in Lists]
dmap_nu_some_true [in NtlDec]
DM_exists [in Base]
DM_or [in Base]


E

equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]


F

filter_fst' [in Base]
filter_fst [in Base]
filter_app [in Base]
filter_id [in Base]
filter_incl [in Base]
FN_sub_incl [in NtlEqui]
FN_sub_other [in NtlEqui]
FN_nu_sub [in NtlEqui]
FN_equiv_shift [in NuTree]
FN_equiv [in NuTree]
FN_in_sub [in NuTree]
free_in_renaming [in NtlEqui]
free_name_in_renaming' [in NtlEqui]
free_name_in_renaming [in NtlEqui]
free_sub_not [in NuTree]
free_in_names [in NuTree]
freshness [in NuTree]
freshness' [in Lists]
fresh_name [in NuTree]


G

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


I

incl_cons [in Lists]
incl_app_left [in Base]
incl_lrcons [in Base]
incl_rcons [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
inv_comm [in Perm]
in_map2_iff [in Lists]
in_candsd3 [in NTA]
in_candsd2 [in NTA]
in_candsd1 [in NTA]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_dmap_nu_iff [in NtlDec]


L

len_plist [in Lists]
list_sum_zero [in Lists]
list_max_max [in Lists]
list_max_cons'' [in Lists]
list_max_cons' [in Lists]
list_max_dep' [in Lists]
list_prop_rel [in Lists]
list_nominal [in Lists]
list_swap_perm [in Lists]
list_assoc [in Lists]
list_id [in Lists]
list_cc [in Base]
list_exists_not_incl [in Base]
list_exists_DM [in Base]
list_cycle [in Base]
lphi_alt [in NTA]
lphi_alt' [in NTA]


M

map_pw_map_eq [in Lists]
map_pw_map [in Lists]
map_eq [in Lists]
map_nth_indep [in Lists]
map2_all_true [in Lists]


N

name_list_max_max [in Lists]
name_assoc [in Perm]
name_id [in Perm]
name_rk_neq [in Perm]
name_eq [in Perm]
nil_el_eq [in Base]
not_disj [in Perm]
not_in_cons [in Base]
no_nus_nu_number_z' [in NuTreeBonus]
no_nus_nu_number_z [in NuTreeBonus]
no_nusk_equiv [in NuTree]
nta_ntl_reject' [in NTA]
nta_ntl_reject [in NTA]
nta_accept_has_name [in NTA]
nta_swap_phi [in NTA]
ntd_S' [in NuTree]
ntd_S [in NuTree]
nth_el_indx_map [in Lists]
nth_el_indx [in Lists]
ntl_refl [in NuTreeBonus]
ntl_nu_push [in NtlEqui]
ntl_nu_push'' [in NtlEqui]
ntl_nu_push' [in NtlEqui]
ntl_nusk_list [in NtlEqui]
ntl_pure_list [in NtlEqui]
ntl_nu_swap [in NtlEqui]
ntl_nu_swap' [in NtlEqui]
ntl_nu_rename [in NtlEqui]
ntl_nu_rename_2 [in NtlEqui]
ntl_nu_rename_1 [in NtlEqui]
ntl_nu_indep [in NtlEqui]
ntl_nu_add [in NtlEqui]
ntl_strengthening [in NtlEqui]
ntl_nu_ignore [in NtlEqui]
ntl_weakening [in NtlEqui]
ntl_alpha_eq [in NtlEqui]
ntl_closed [in NtlEqui]
ntl_renaming [in NtlEqui]
ntl_renaming'' [in NtlEqui]
ntl_renaming' [in NtlEqui]
ntl_eq_refl [in NtlEqui]
ntl_equiv [in NuTree]
ntl_equiv'' [in NuTree]
ntl_equiv' [in NuTree]
ntl_swap_list [in NuTree]
ntl_name_not_in [in NuTree]
ntl_name_in [in NuTree]
ntl_name [in NuTree]
ntl_dec_correct [in NtlDec]
ntl_dec_correct_2 [in NtlDec]
ntl_dec_correct_1 [in NtlDec]
ntl_dec_depth [in NtlDec]
ntl_sim [in NtlDec]
ntl_dec_similar [in NtlDec]
ntl_dec_true_name' [in NtlDec]
ntl_dec_true_name [in NtlDec]
nt_eq_correct [in NuTreeBonus]
nt_eq_correct_2 [in NuTreeBonus]
nt_eq_correct_1 [in NuTreeBonus]
nt_str_renaming [in NtlEqui]
nt_str_FN [in NuTree]
nt_str_dec [in NuTree]
nt_str_correct [in NuTree]
nt_str_correct_2 [in NuTree]
nt_str_correct_1 [in NuTree]
nt_names_equiv [in NuTree]
nt_assoc3 [in NuTree]
nt_nominal [in NuTree]
nt_swap_perm'' [in NuTree]
nt_swap_perm' [in NuTree]
nt_swap_perm [in NuTree]
nt_depth_perm [in NuTree]
nt_perm_wr [in NuTree]
nt_perm_apply_inv [in NuTree]
nt_sym [in NuTree]
nt_id [in NuTree]
nt_assoc [in NuTree]
nt_apply_perm_step [in NuTree]
nt_names_inhab [in NuTree]
nt_name_in_sub [in NuTree]
nt_decrease' [in NuTree]
nt_decrease [in NuTree]
nt_wr_sub' [in NuTree]
nt_wr_sub [in NuTree]
num_max_le [in Lists]
num_max_comm [in Lists]
num_max_or [in Lists]
num_max_zero [in Lists]
nu_swap_FN [in NtlEqui]
nu_FN' [in NtlEqui]
nu_FN [in NtlEqui]


P

perm_list_shift [in Lists]
perm_list_el [in Lists]
perm_list_el'' [in Lists]
perm_list_el' [in Lists]
perm_list_inv [in Lists]
perm_list_step [in Lists]
perm_rk [in Perm]
perm_inv_perm [in Perm]
perm_compose_perm [in Perm]
perm_inv_compose [in Perm]
perm_inv_shift [in Perm]
perm_inj [in Perm]
perm_inj' [in Perm]
perm_id [in Perm]
perm_inv' [in Perm]
perm_inv [in Perm]
perm_apply_inv [in Tree]
perm_tree_wr [in Tree]
plist_eq [in Lists]
plist_len [in Lists]
psim_perm' [in NtlDec]
psim_perm [in NtlDec]
pure_nu_number_z [in NuTreeBonus]
pure_no_nus [in NuTreeBonus]


Q

qlist_correct [in NTA]


R

rem_id [in NuTree]
rem_equiv' [in NuTree]
rem_equiv [in NuTree]
rem_fst' [in Base]
rem_fst [in Base]
rem_equi [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_incl [in Base]
rem_not_in [in Base]
renaming_invariant [in NtlEqui]
renaming_inverse [in NtlEqui]
renaming_nil [in NtlEqui]
renaming_sub' [in NtlEqui]
renaming_sub [in NtlEqui]
rep_nth_id [in Lists]
rep_nth_el' [in Lists]
rep_nth_indep [in Lists]
rep_nth_overwrite [in Lists]
rep_nth_el_or [in Lists]
rep_nth_el [in Lists]
rep_nth_exact [in Lists]
rep_nth_len' [in Lists]
rep_nth_len [in Lists]
rep_nth_nil [in Lists]


S

similar_correct' [in NtlDec]
similar_swap_perm [in NtlDec]
similar_equiv [in NtlDec]
similar_correct [in NtlDec]
sim_psim [in NtlDec]
sim_perm' [in NtlDec]
sim_perm [in NtlDec]
some_true_true [in Lists]
step_var_agree [in NTA]
step_var_in_all [in NTA]
sym_action_name [in Perm]


T

tdec_p_correct [in NTA]
tdec_p_correct_2 [in NTA]
tdec_p_correct_1 [in NTA]
tdec_s_correct [in NTA]
tdec_s_correct_2 [in NTA]
tdec_s_correct_1 [in NTA]
tdec_correct [in NTA]
tdec_correct_2 [in NTA]
tdec_correct_1 [in NTA]
transp_list_indep [in Lists]
transp_list_el [in Lists]
transp_FN' [in NtlEqui]
transp_FN [in NtlEqui]
transp_renaming [in NtlEqui]
transp_chain' [in Perm]
transp_chain'' [in Perm]
transp_chain [in Perm]
transp_diff [in Perm]
transp_id [in Perm]
transp_swap [in Perm]
transp_compose [in Perm]
transp_apply [in Perm]
transp_rk' [in Perm]
transp_perm_iff [in Perm]
transp_rk [in Perm]
transp_perm' [in Perm]
transp_perm [in Perm]
transp_inv [in Perm]
tree_name_free [in NuTree]
tree_nominal [in Tree]
tree_swap_perm [in Tree]
tree_sym [in Tree]
tree_id [in Tree]
tree_assoc [in Tree]
tree_wr_sub [in Tree]
tree_name_in_sub [in Tree]
twr_ntwr [in NuTreeBonus]
t_to_nt_in [in NuTreeBonus]



Constructor Index

A

AD1 [in NTA]
AD2 [in NTA]
AD3 [in NTA]


D

DNLs [in NuTree]
DNNu [in NuTree]


E

EqType [in Base]


N

nonusA [in NuTree]
nonuskA [in NuTree]
nonuskB [in NuTree]
NteqA [in NuTreeBonus]
NteqB [in NuTreeBonus]
NtStrA [in NuTree]
NtStrB [in NuTree]
ntwrA [in NuTree]
ntwrB [in NuTree]
Nu [in NuTree]


P

pListC [in Lists]
pListN [in Lists]
PSimA [in NtlDec]
PSimB [in NtlDec]


S

SimA [in NtlDec]
SimB [in NtlDec]


T

Tr [in NuTree]
TrA [in Tree]
treewrA [in Tree]



Axiom Index

A

A [in NTA]



Inductive Index

N

NoNus [in NuTree]
NoNusk [in NuTree]
NtaAccept [in NTA]
NtAccept [in NuTree]
Nteq [in NuTreeBonus]
NtStr [in NuTree]
Ntwr [in NuTree]
NuTree [in NuTree]


P

plist [in Lists]
PSim [in NtlDec]


S

Sim [in NtlDec]


T

Tree [in Tree]
Twr [in Tree]



Projection Index

D

D1' [in NTA]
D2' [in NTA]
D3' [in NTA]


E

eqType_dec [in Base]
eqType_X [in Base]


S

s' [in NTA]



Section Index

A

Action [in Tree]


C

Correct [in NtlDec]


D

Depth [in NuTree]


E

Equality [in NuTreeBonus]
Equi [in Base]
Equivariance [in NuTree]


F

Filter [in Base]
Freshness [in Lists]


I

Inclusion [in Base]


M

Membership [in Base]


N

NatNumList [in Lists]
NtAction [in NuTree]
NuIndep [in NtlEqui]
NuPush [in NtlEqui]
NuRename [in NtlEqui]
NuSwap [in NtlEqui]


R

Removal [in Base]
Renaming [in NtlEqui]


S

Structure [in NuTree]



Instance Index

A

and_dec [in Base]
app_equi_proper [in Base]
app_incl_proper [in Base]


B

bool_eq_dec [in Base]
bool_dec [in Base]


C

char_eq_dec [in Perm]
cons_equi_proper [in Base]
cons_incl_proper [in Base]


E

equi_Equivalence [in Base]


F

False_dec [in Base]


I

iff_dec [in Base]
impl_dec [in Base]
incl_equi_proper [in Base]
incl_preorder [in Base]
in_equi_proper [in Base]
in_incl_proper [in Base]


L

list_exists_dec [in Base]
list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]


N

nat_eq_dec [in Base]
not_dec [in Base]
nt_eq_dec [in NuTreeBonus]


O

option_eq_dec [in NTA]
or_dec [in Base]


P

prod_eq_dec [in Base]


S

state_eq_dec' [in NTA]
state_eq_dec [in NTA]


T

True_dec [in Base]



Abbreviation Index

D

Decb [in Base]



Definition Index

A

all_true [in Lists]
all_phis [in NTA]
all_phis' [in NTA]
all_conts [in NTA]
all_assns [in NTA]
apply_perm [in Tree]


B

BN [in NuTree]
bool2Prop [in Base]


C

candidates [in NtlDec]
candsd1 [in NTA]
candsd2 [in NTA]
candsd3 [in NTA]
compose [in Perm]


D

Dec [in Base]
dec [in Base]
dec2bool [in Base]
Delta1 [in NTA]
Delta2 [in NTA]
Delta3 [in NTA]
dmap_nu [in NtlDec]
DNT [in NuTree]
DTR [in Tree]
D1 [in NTA]
D2 [in NTA]
D3 [in NTA]


E

eqType_CS [in Base]
equi [in Base]


F

filter [in Base]
FN [in NuTree]
fresh [in NuTree]
fresh' [in Lists]


I

inclp [in Base]
Inv [in Perm]


L

list_sum [in Lists]
list_max [in Lists]
list_max' [in Lists]
lPhi [in NTA]


M

map_pw [in Lists]
map2 [in Lists]


N

Name [in Perm]
NameF [in Perm]
names [in Tree]
name_list_max [in Lists]
nonphi [in NTA]
nta_names [in NTA]
NtlEq [in NtlEqui]
NtlRho [in NtlEqui]
ntl_dec [in NtlDec]
nt_eq [in NuTreeBonus]
nt_str [in NuTree]
nt_apply_perm [in NuTree]
nt_names [in NuTree]
nt_depth [in NuTree]
num_max [in Lists]
NuNumber [in NuTreeBonus]


P

Perm [in Perm]
perm_list [in Lists]
Phi [in NTA]
Phi' [in NTA]


Q

Q [in NTA]
qlist [in NTA]
Q' [in NTA]


R

rem [in Base]
Renaming [in NtlEqui]
rep_nth [in Lists]
rk [in Perm]


S

s [in NTA]
similar [in NtlDec]
some_true [in Lists]
states [in NTA]
step_var [in NTA]


T

tdec [in NTA]
tdec_p [in NTA]
tdec_s [in NTA]
tdec_some_true [in NTA]
tdec_all_true [in NTA]
to_fun [in NTA]
transp [in Perm]
t_to_nt [in NuTreeBonus]


U

update [in NTA]



Record Index

E

eqType [in Base]


N

NTA [in NTA]



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 (525 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 (13 entries)
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 (33 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 (9 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 (294 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 (25 entries)
Axiom 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)
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 (13 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 (6 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 (19 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 (29 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 (1 entry)
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 (80 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 (2 entries)