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

NTANtlDec

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) |