| 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 | _ | (485 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 | _ | (2 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 | _ | (293 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 | _ | (4 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 | _ | (9 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 | _ | (169 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 | _ | (8 entries) |
Global Index
A
A [definition, in reach]abstraction [inductive, in reach]
abstractionG [definition, in reach]
action0iX [definition, in reach]
action0X [definition, in reach]
action1iX [definition, in reach]
action1X [definition, in reach]
act0real1X [lemma, in reach]
act0real2X [lemma, in reach]
act0real3X [lemma, in reach]
act01X [lemma, in reach]
act0_edge_rest [lemma, in reach]
act1realX [lemma, in reach]
act1real1X [lemma, in reach]
act1real2X [lemma, in reach]
act1real3X [lemma, in reach]
act_CG [definition, in graphs]
act_free_CG [lemma, in graphs]
act_free_eq [lemma, in fingroup]
adds_all [definition, in finfun]
Aexpbound [lemma, in reach]
all_flatten [lemma, in fingroup]
all_maps [lemma, in fingroup]
all_seq [definition, in finfun]
all_seq_elem_size [lemma, in finfun]
An_bound [lemma, in reach]
An_boundU [definition, in main]
APP [lemma, in reach]
AU [definition, in main]
B
before_measure [lemma, in reach]boollogic [library]
C
cancell [lemma, in fingroup]cancelr [lemma, in fingroup]
canonical_congr [lemma, in eqrel]
canonical_congr1 [lemma, in eqrel]
canonical_elem [lemma, in eqrel]
canonical_fun [definition, in eqrel]
canonical_inj [lemma, in eqrel]
canonical_inj1 [lemma, in eqrel]
card_AC_A [lemma, in reach]
card_cat [lemma, in general]
card_finFun [lemma, in finfun]
card_flatten [lemma, in general]
card_nodes_visited [lemma, in main]
card_obs [lemma, in reach]
card_option [lemma, in general]
card_prod_fin [lemma, in reach]
card_quotient [lemma, in eqrel]
card_quotient_equals [lemma, in eqrel]
card_quotient_join_leq [lemma, in eqrel]
card_quotient_join_lt [lemma, in eqrel]
card_quotient_leq [lemma, in eqrel]
card_quotient_lower [lemma, in eqrel]
card_quotient_separate [lemma, in eqrel]
card_quotient_upper [lemma, in eqrel]
card_separate_quotient [lemma, in eqrel]
card_separate_quotient_eq [lemma, in eqrel]
card_sub_fin [lemma, in finfun]
carrier_wp [definition, in fingroup]
cayleyGraph [definition, in graphs]
classes_equal [lemma, in eqrel]
coal [definition, in reach]
coalE [definition, in reach]
coalSn_bound [lemma, in reach]
coalSn_strictbound [lemma, in reach]
coal0 [lemma, in reach]
coal_bound [lemma, in reach]
coal_cardP [lemma, in reach]
coal_defined [lemma, in reach]
coal_eqQX [lemma, in reach]
coal_eqQX_before [lemma, in reach]
coal_init_econf [lemma, in reach]
coal_leq [lemma, in reach]
coal_measure_between [lemma, in reach]
coal_mon1 [lemma, in reach]
coal_nbound [lemma, in reach]
coal_shift [lemma, in reach]
coal_stepn [lemma, in reach]
coal_stepn_between [lemma, in reach]
coal_triv_bound [lemma, in reach]
commutative [definition, in fingroup]
comm_cyclicgroup [lemma, in fingroup]
comm_tuplegroup [lemma, in fingroup]
conf [definition, in reach]
configs_bound [lemma, in main]
configs_boundU [lemma, in main]
count1_all_seq [lemma, in finfun]
count_adds_all [lemma, in finfun]
cyclicgroup [definition, in fingroup]
D
decomp_sim [lemma, in reach]degree_CG [definition, in graphs]
div [definition, in general]
diveuclr [inductive, in general]
divexr [constructor, in general]
div_mod [lemma, in general]
div_mod_exists [lemma, in general]
dom_abstr [definition, in reach]
dom_abstr_act0 [lemma, in reach]
dom_abstr_act1 [lemma, in reach]
dom_abstr_act1_edge_npred [lemma, in reach]
dom_abstr_rel [definition, in reach]
E
econf [definition, in reach]econfP [definition, in reach]
econf_conf [definition, in reach]
econf_conf_eevolution [lemma, in reach]
econf_conf_init_econf [lemma, in reach]
econf_det_abstG [lemma, in reach]
econf_observe [lemma, in reach]
econf_subd_eqd [lemma, in reach]
edgegroup_CG [definition, in graphs]
edges_CG [definition, in graphs]
edge_of_nat [definition, in graphs]
eevolution [definition, in reach]
eevolution_make_moves_from [lemma, in reach]
eevolution_make_moves_from_mult [lemma, in reach]
eevolution_repeat [lemma, in reach]
eevolution_seq [definition, in reach]
eevolution_seq_cat [lemma, in reach]
eevolution_step [lemma, in reach]
eevolution_sub [lemma, in reach]
eevolution_sum [lemma, in reach]
eg_orderP_CG [definition, in graphs]
eg_order_CG [definition, in graphs]
eg_order_positive_CG [definition, in graphs]
env [definition, in reach]
eqclass [definition, in eqrel]
eqclasses [definition, in eqrel]
eqclass_eq [lemma, in eqrel]
eqclass_pickeqc [lemma, in eqrel]
eqdQobs [definition, in reach]
eqdQobs_eevolution [lemma, in reach]
eqdQX [definition, in reach]
eqdQX_eevolution [lemma, in reach]
eqdQX_stepe [lemma, in reach]
eqdQX_stepe_gen [lemma, in reach]
eqd_ieqrel [definition, in eqrel]
eqd_ieqrelPx [lemma, in eqrel]
eqfgraph [definition, in finfun]
eqfgraphPx [lemma, in finfun]
eqrel [library]
eqrelType [inductive, in eqrel]
eqrel_ieqrel [lemma, in eqrel]
eqrel_of_ieqrel [definition, in eqrel]
eqrel_of_ieqrelType [definition, in eqrel]
eqrel_of_ieqrelType_congr [lemma, in eqrel]
eqrel_of_ieqrel_congr [lemma, in eqrel]
eqrel_of_ieqrel_inj [lemma, in eqrel]
equals_ieqrel [definition, in eqrel]
equiv [definition, in reach]
eq_div [lemma, in general]
eq_eqclass [lemma, in eqrel]
eq_finfun [lemma, in finfun]
eq_make_moves_from [lemma, in reach]
eq_make_moves_from_mult [lemma, in reach]
eq_maps_mem [lemma, in general]
eq_mod [lemma, in general]
erel_dom_abstr [lemma, in reach]
erel_dom_card_step_npred [lemma, in reach]
erel_dom_card_step_pred [lemma, in reach]
erel_join [lemma, in eqrel]
erel_observe_G [lemma, in reach]
erel_separate [lemma, in eqrel]
eucl_devr [lemma, in general]
evolution [definition, in reach]
evolution_ACP [lemma, in reach]
evolution_seq [definition, in reach]
evolution_seq_cat [lemma, in reach]
evolution_seq_repeat_subset [lemma, in reach]
evolution_step [lemma, in reach]
evolution_sub [lemma, in reach]
evolution_sum [lemma, in reach]
evolution_to_coal [definition, in reach]
evol_eevol_seq [lemma, in reach]
evol_eevol_seq_init [lemma, in reach]
exp [definition, in general]
expbound [definition, in reach]
expboundnn [lemma, in reach]
expboundSn [lemma, in reach]
expn1 [lemma, in general]
exp0n [lemma, in general]
exp_exp [lemma, in general]
exp_mul [lemma, in general]
exp_plus [lemma, in general]
exp_positive [lemma, in general]
F
fact [definition, in general]fact_exp [lemma, in general]
fact_middle [lemma, in general]
fact_positive [lemma, in general]
Fgraph [constructor, in finfun]
fgraphType [inductive, in finfun]
fgraph_enum [definition, in finfun]
fgraph_enumP [lemma, in finfun]
fgraph_enum_dep [definition, in finfun]
fgraph_enum_lenP [definition, in finfun]
fgraph_enum_val [definition, in finfun]
fgraph_fun_eq [lemma, in finfun]
fgraph_of_fun [definition, in finfun]
fgraph_of_fun_congr [lemma, in finfun]
fgraph_of_fun_inj [lemma, in finfun]
fgraph_of_fun_surj [lemma, in finfun]
finfun [library]
fingroup [library]
flatten [definition, in general]
free [definition, in fingroup]
fun_of_fgraph [definition, in finfun]
fval [definition, in finfun]
fval_eq [lemma, in finfun]
G
general [library]generators [definition, in fingroup]
generators_tuplegroup [lemma, in fingroup]
generators_wp [lemma, in fingroup]
gensU [lemma, in graphs]
gens_cyclicgroup [definition, in fingroup]
gens_tuplegroup [definition, in fingroup]
gens_U [definition, in graphs]
gens_wp [definition, in fingroup]
gen_cyclicgroup [lemma, in fingroup]
gen_x [lemma, in fingroup]
graph [inductive, in graphs]
graphCR [definition, in graphs]
graphs [library]
graphU [definition, in graphs]
gU [definition, in main]
I
ieqrel [inductive, in eqrel]ieqrelType [definition, in eqrel]
ieqrelType_of_eqrel [definition, in eqrel]
ieqrelType_of_eqrel_congr [lemma, in eqrel]
ieqrel_enum [definition, in eqrel]
ieqrel_enumP [lemma, in eqrel]
ieqrel_eqd [lemma, in eqrel]
ieqrel_eqrel [lemma, in eqrel]
ieqrel_of_eqrel [definition, in eqrel]
ieqrel_of_eqrelP [lemma, in eqrel]
ieqrel_of_eqrel_congr [lemma, in eqrel]
ieqrel_of_eqrel_inj [lemma, in eqrel]
ieqrel_pred [definition, in eqrel]
iffB [lemma, in general]
iforall [definition, in boollogic]
iforallPnx [lemma, in boollogic]
iforallPx [lemma, in boollogic]
iforall2 [definition, in boollogic]
iforall2Px [lemma, in boollogic]
iforall3 [definition, in boollogic]
iforall3Px [lemma, in boollogic]
image_exists [lemma, in general]
initiX [definition, in reach]
initX [definition, in reach]
initXreal1 [lemma, in reach]
initXreal2 [lemma, in reach]
initXreal3 [lemma, in reach]
initX_refl_dom [lemma, in reach]
initX_sym_dom [lemma, in reach]
initX_trans_dom [lemma, in reach]
init_econf [definition, in reach]
init_factors [lemma, in reach]
injective_card [lemma, in general]
invrP [lemma, in fingroup]
inv_inv [lemma, in fingroup]
inv_mkunitG [lemma, in fingroup]
inv_mkunitH_unit [lemma, in fingroup]
inv_modulo [definition, in fingroup]
inv_mul [lemma, in fingroup]
inv_unit [lemma, in fingroup]
inv_wp [definition, in fingroup]
irefl_dom [definition, in reach]
isym_dom [definition, in reach]
is_singleton [definition, in reach]
is_singleton_class [definition, in eqrel]
is_some [definition, in general]
is_some_action1X_finer [lemma, in reach]
is_some_act0X [lemma, in reach]
is_some_act1X [lemma, in reach]
is_some_act1_edge_npred [lemma, in reach]
is_some_initX [lemma, in reach]
is_some_init_finest [lemma, in reach]
is_some_map [lemma, in general]
is_some_None [lemma, in general]
is_some_update [lemma, in reach]
iterate_make_moves [definition, in reach]
iterate_make_moves_act [lemma, in reach]
iterate_make_moves_act_twice [lemma, in reach]
iterate_make_moves_repeat [lemma, in reach]
iterate_make_moves_repeat_allpebbles [lemma, in reach]
iterate_make_moves_repeat_singlepebble [lemma, in reach]
iterate_make_moves_sum [lemma, in reach]
itrans_dom [definition, in reach]
iX [definition, in reach]
iXX [definition, in reach]
iXX_eq [lemma, in reach]
iXX_XiX [lemma, in reach]
J
jag [inductive, in reach]join [definition, in eqrel]
join_rel [definition, in reach]
join_rel_same [lemma, in reach]
L
leqnexp [lemma, in general]leq_exp [lemma, in general]
leq_exp2l [lemma, in general]
leq_exp2r [lemma, in general]
M
main [lemma, in reach]main [library]
make_moves [definition, in reach]
make_moves_act [lemma, in reach]
make_moves_adds [lemma, in reach]
make_moves_from [definition, in reach]
make_moves_from_step [lemma, in reach]
make_moves_iterate_make_moves [lemma, in reach]
maps_adds_size [lemma, in finfun]
maps_prodE1_zip [lemma, in general]
maps_prodE2_zip [lemma, in general]
maps_sub_index [lemma, in general]
maps_val_fgraph_enum [lemma, in finfun]
map_option [definition, in general]
max [definition, in general]
max [definition, in reach]
max_lower [lemma, in general]
max_upper [lemma, in general]
measure_abstG [definition, in reach]
measure_eevolution_coal [lemma, in reach]
measure_init_abstG [lemma, in reach]
measure_leq [lemma, in reach]
measure_loop [lemma, in reach]
measure_lower_abstG [lemma, in reach]
measure_step_abstG [lemma, in reach]
measure_upper_abstG [lemma, in reach]
mem_gens_tuplegroup [lemma, in fingroup]
mem_gens_wp [lemma, in fingroup]
mkunitG [definition, in fingroup]
mkunitG_gen [lemma, in fingroup]
mkunitG_mul [lemma, in fingroup]
mkunitG_unit [lemma, in fingroup]
mkunitH [definition, in fingroup]
mkunitH_gen [lemma, in fingroup]
mkunitH_genH [lemma, in fingroup]
mkunitH_g_unit [lemma, in fingroup]
mkunitH_mul [lemma, in fingroup]
mkunitH_unit [lemma, in fingroup]
mk_econf [definition, in reach]
mk_ord [definition, in graphs]
mod [definition, in general]
mod0 [lemma, in general]
mod_add [lemma, in general]
mod_cancel [lemma, in general]
mod_lt [lemma, in general]
mod_small [lemma, in general]
move [inductive, in reach]
move_eqd [definition, in reach]
move_eqPx [lemma, in reach]
multiply [definition, in general]
multiply_exp [lemma, in general]
multiply_middle [lemma, in general]
mul_modulo [definition, in fingroup]
mul_wp [definition, in fingroup]
m_edge [constructor, in reach]
m_jump [constructor, in reach]
m_positive [lemma, in graphs]
m_posU [lemma, in graphs]
N
next [definition, in reach]nodes_of_conf [definition, in main]
nodes_visited [definition, in main]
nodes_visited_bound [lemma, in main]
nodes_visited_boundU [lemma, in main]
node_s_CG [definition, in graphs]
node_t_CG [definition, in graphs]
NoneF [definition, in general]
O
obs [definition, in reach]obs_abstG [definition, in reach]
obs_relX [lemma, in reach]
one_cyclicgroup [definition, in fingroup]
option_enum [definition, in general]
option_enumP [lemma, in general]
option_eqd [definition, in general]
option_eqPx [lemma, in general]
order [definition, in fingroup]
orderUgt1 [lemma, in main]
order_cyclicgroup [lemma, in fingroup]
order_tuplegroup [lemma, in fingroup]
order_wp [lemma, in fingroup]
P
P [axiom, in reach]pickeqc [definition, in eqrel]
pickeqc_eqclass [lemma, in eqrel]
pickeqc_eqd [lemma, in eqrel]
pigeon [lemma, in general]
pigeon_nat [lemma, in general]
piQ [definition, in reach]
piS [definition, in reach]
piX [definition, in reach]
predictableiX [definition, in reach]
predictableX [definition, in reach]
predictableX_edge_cond [lemma, in reach]
predictableX_ix [lemma, in reach]
pred_mon [lemma, in reach]
Prop3 [definition, in main]
Q
Q [axiom, in reach]quotient [definition, in eqrel]
quotient_map [definition, in eqrel]
quotient_map_injective [lemma, in eqrel]
R
R [definition, in reach]reach [library]
realisesiX [definition, in reach]
realisesiX_X [lemma, in reach]
realisesX [definition, in reach]
realisesX_iX [lemma, in reach]
realises1iX [definition, in reach]
realises1iX_X [lemma, in reach]
realises1X [definition, in reach]
realises1X_iX [lemma, in reach]
realises2iX [definition, in reach]
realises2iX_X [lemma, in reach]
realises2X [definition, in reach]
realises2X_iX [lemma, in reach]
realises3iX [definition, in reach]
realises3iX_X [lemma, in reach]
realises3X [definition, in reach]
realises3X_iX [lemma, in reach]
real_econf [lemma, in reach]
refl_dom [definition, in reach]
repeatQobs [lemma, in reach]
repeatQobs_mult [lemma, in reach]
repeat_add [lemma, in reach]
Rexpbound [lemma, in reach]
RPP [lemma, in reach]
RSn_bound [lemma, in reach]
RSn_boundU [definition, in main]
RU [definition, in main]
R0_bound [lemma, in reach]
R0_boundU [definition, in main]
S
separate [definition, in eqrel]separate_rel [definition, in reach]
separate_singleton [lemma, in eqrel]
setAC [definition, in reach]
setACP [definition, in reach]
set_rel [definition, in eqrel]
sim [definition, in reach]
sim_rel [definition, in reach]
size_adds_all [lemma, in finfun]
size_all_seq [lemma, in finfun]
size_bound_An [lemma, in reach]
size_bound_RSn [lemma, in reach]
size_bound_R0 [lemma, in reach]
size_eevolution_seq [lemma, in reach]
size_evolution_seq [lemma, in reach]
size_gens_cyclicgroup [lemma, in fingroup]
size_gens_tuplegroup [lemma, in fingroup]
size_gens_wp [lemma, in fingroup]
size_stepn_seq [lemma, in reach]
SomeF [definition, in general]
state_space [inductive, in reach]
state_space_G [definition, in reach]
state_space_G_action [definition, in reach]
state_space_G_obs [definition, in reach]
stepe [definition, in reach]
stepe_econf [lemma, in reach]
stepe_eqd [lemma, in reach]
stepe_Q [lemma, in reach]
stepe_S [lemma, in reach]
stepe_X0 [lemma, in reach]
stepe_X1 [lemma, in reach]
stepn [definition, in reach]
stepn_seq [definition, in reach]
step_eevolution [lemma, in reach]
sub_n0 [lemma, in reach]
sum_seq [definition, in fingroup]
sum_seq_cat [lemma, in fingroup]
sum_seq_flatten [lemma, in fingroup]
sum_unit_vector [lemma, in fingroup]
sym_dom [definition, in reach]
T
transitive [definition, in fingroup]trans_dom [definition, in reach]
tuplegroup [definition, in fingroup]
U
union [definition, in reach]uniq_div [lemma, in general]
uniq_mod [lemma, in general]
unitrP [lemma, in fingroup]
unit_vector [definition, in fingroup]
unit_vector_gen [lemma, in fingroup]
unit_wp [definition, in fingroup]
update [definition, in reach]
update_eqrel [lemma, in reach]
V
vertices_CG [definition, in graphs]W
wp [definition, in fingroup]X
X [definition, in reach]XiX [definition, in reach]
XiX_action1 [lemma, in reach]
XiX_iXX [lemma, in reach]
Z
zip [definition, in general]Axiom Index
P
P [in reach]Q
Q [in reach]Lemma Index
A
act0real1X [in reach]act0real2X [in reach]
act0real3X [in reach]
act01X [in reach]
act0_edge_rest [in reach]
act1realX [in reach]
act1real1X [in reach]
act1real2X [in reach]
act1real3X [in reach]
act_free_CG [in graphs]
act_free_eq [in fingroup]
Aexpbound [in reach]
all_flatten [in fingroup]
all_maps [in fingroup]
all_seq_elem_size [in finfun]
An_bound [in reach]
APP [in reach]
B
before_measure [in reach]C
cancell [in fingroup]cancelr [in fingroup]
canonical_congr [in eqrel]
canonical_congr1 [in eqrel]
canonical_elem [in eqrel]
canonical_inj [in eqrel]
canonical_inj1 [in eqrel]
card_AC_A [in reach]
card_cat [in general]
card_finFun [in finfun]
card_flatten [in general]
card_nodes_visited [in main]
card_obs [in reach]
card_option [in general]
card_prod_fin [in reach]
card_quotient [in eqrel]
card_quotient_equals [in eqrel]
card_quotient_join_leq [in eqrel]
card_quotient_join_lt [in eqrel]
card_quotient_leq [in eqrel]
card_quotient_lower [in eqrel]
card_quotient_separate [in eqrel]
card_quotient_upper [in eqrel]
card_separate_quotient [in eqrel]
card_separate_quotient_eq [in eqrel]
card_sub_fin [in finfun]
classes_equal [in eqrel]
coalSn_bound [in reach]
coalSn_strictbound [in reach]
coal0 [in reach]
coal_bound [in reach]
coal_cardP [in reach]
coal_defined [in reach]
coal_eqQX [in reach]
coal_eqQX_before [in reach]
coal_init_econf [in reach]
coal_leq [in reach]
coal_measure_between [in reach]
coal_mon1 [in reach]
coal_nbound [in reach]
coal_shift [in reach]
coal_stepn [in reach]
coal_stepn_between [in reach]
coal_triv_bound [in reach]
comm_cyclicgroup [in fingroup]
comm_tuplegroup [in fingroup]
configs_bound [in main]
configs_boundU [in main]
count1_all_seq [in finfun]
count_adds_all [in finfun]
D
decomp_sim [in reach]div_mod [in general]
div_mod_exists [in general]
dom_abstr_act0 [in reach]
dom_abstr_act1 [in reach]
dom_abstr_act1_edge_npred [in reach]
E
econf_conf_eevolution [in reach]econf_conf_init_econf [in reach]
econf_det_abstG [in reach]
econf_observe [in reach]
econf_subd_eqd [in reach]
eevolution_make_moves_from [in reach]
eevolution_make_moves_from_mult [in reach]
eevolution_repeat [in reach]
eevolution_seq_cat [in reach]
eevolution_step [in reach]
eevolution_sub [in reach]
eevolution_sum [in reach]
eqclass_eq [in eqrel]
eqclass_pickeqc [in eqrel]
eqdQobs_eevolution [in reach]
eqdQX_eevolution [in reach]
eqdQX_stepe [in reach]
eqdQX_stepe_gen [in reach]
eqd_ieqrelPx [in eqrel]
eqfgraphPx [in finfun]
eqrel_ieqrel [in eqrel]
eqrel_of_ieqrelType_congr [in eqrel]
eqrel_of_ieqrel_congr [in eqrel]
eqrel_of_ieqrel_inj [in eqrel]
eq_div [in general]
eq_eqclass [in eqrel]
eq_finfun [in finfun]
eq_make_moves_from [in reach]
eq_make_moves_from_mult [in reach]
eq_maps_mem [in general]
eq_mod [in general]
erel_dom_abstr [in reach]
erel_dom_card_step_npred [in reach]
erel_dom_card_step_pred [in reach]
erel_join [in eqrel]
erel_observe_G [in reach]
erel_separate [in eqrel]
eucl_devr [in general]
evolution_ACP [in reach]
evolution_seq_cat [in reach]
evolution_seq_repeat_subset [in reach]
evolution_step [in reach]
evolution_sub [in reach]
evolution_sum [in reach]
evol_eevol_seq [in reach]
evol_eevol_seq_init [in reach]
expboundnn [in reach]
expboundSn [in reach]
expn1 [in general]
exp0n [in general]
exp_exp [in general]
exp_mul [in general]
exp_plus [in general]
exp_positive [in general]
F
fact_exp [in general]fact_middle [in general]
fact_positive [in general]
fgraph_enumP [in finfun]
fgraph_fun_eq [in finfun]
fgraph_of_fun_congr [in finfun]
fgraph_of_fun_inj [in finfun]
fgraph_of_fun_surj [in finfun]
fval_eq [in finfun]
G
generators_tuplegroup [in fingroup]generators_wp [in fingroup]
gensU [in graphs]
gen_cyclicgroup [in fingroup]
gen_x [in fingroup]
I
ieqrelType_of_eqrel_congr [in eqrel]ieqrel_enumP [in eqrel]
ieqrel_eqd [in eqrel]
ieqrel_eqrel [in eqrel]
ieqrel_of_eqrelP [in eqrel]
ieqrel_of_eqrel_congr [in eqrel]
ieqrel_of_eqrel_inj [in eqrel]
iffB [in general]
iforallPnx [in boollogic]
iforallPx [in boollogic]
iforall2Px [in boollogic]
iforall3Px [in boollogic]
image_exists [in general]
initXreal1 [in reach]
initXreal2 [in reach]
initXreal3 [in reach]
initX_refl_dom [in reach]
initX_sym_dom [in reach]
initX_trans_dom [in reach]
init_factors [in reach]
injective_card [in general]
invrP [in fingroup]
inv_inv [in fingroup]
inv_mkunitG [in fingroup]
inv_mkunitH_unit [in fingroup]
inv_mul [in fingroup]
inv_unit [in fingroup]
is_some_action1X_finer [in reach]
is_some_act0X [in reach]
is_some_act1X [in reach]
is_some_act1_edge_npred [in reach]
is_some_initX [in reach]
is_some_init_finest [in reach]
is_some_map [in general]
is_some_None [in general]
is_some_update [in reach]
iterate_make_moves_act [in reach]
iterate_make_moves_act_twice [in reach]
iterate_make_moves_repeat [in reach]
iterate_make_moves_repeat_allpebbles [in reach]
iterate_make_moves_repeat_singlepebble [in reach]
iterate_make_moves_sum [in reach]
iXX_eq [in reach]
iXX_XiX [in reach]
J
join_rel_same [in reach]L
leqnexp [in general]leq_exp [in general]
leq_exp2l [in general]
leq_exp2r [in general]
M
main [in reach]make_moves_act [in reach]
make_moves_adds [in reach]
make_moves_from_step [in reach]
make_moves_iterate_make_moves [in reach]
maps_adds_size [in finfun]
maps_prodE1_zip [in general]
maps_prodE2_zip [in general]
maps_sub_index [in general]
maps_val_fgraph_enum [in finfun]
max_lower [in general]
max_upper [in general]
measure_eevolution_coal [in reach]
measure_init_abstG [in reach]
measure_leq [in reach]
measure_loop [in reach]
measure_lower_abstG [in reach]
measure_step_abstG [in reach]
measure_upper_abstG [in reach]
mem_gens_tuplegroup [in fingroup]
mem_gens_wp [in fingroup]
mkunitG_gen [in fingroup]
mkunitG_mul [in fingroup]
mkunitG_unit [in fingroup]
mkunitH_gen [in fingroup]
mkunitH_genH [in fingroup]
mkunitH_g_unit [in fingroup]
mkunitH_mul [in fingroup]
mkunitH_unit [in fingroup]
mod0 [in general]
mod_add [in general]
mod_cancel [in general]
mod_lt [in general]
mod_small [in general]
move_eqPx [in reach]
multiply_exp [in general]
multiply_middle [in general]
m_positive [in graphs]
m_posU [in graphs]
N
nodes_visited_bound [in main]nodes_visited_boundU [in main]
O
obs_relX [in reach]option_enumP [in general]
option_eqPx [in general]
orderUgt1 [in main]
order_cyclicgroup [in fingroup]
order_tuplegroup [in fingroup]
order_wp [in fingroup]
P
pickeqc_eqclass [in eqrel]pickeqc_eqd [in eqrel]
pigeon [in general]
pigeon_nat [in general]
predictableX_edge_cond [in reach]
predictableX_ix [in reach]
pred_mon [in reach]
Q
quotient_map_injective [in eqrel]R
realisesiX_X [in reach]realisesX_iX [in reach]
realises1iX_X [in reach]
realises1X_iX [in reach]
realises2iX_X [in reach]
realises2X_iX [in reach]
realises3iX_X [in reach]
realises3X_iX [in reach]
real_econf [in reach]
repeatQobs [in reach]
repeatQobs_mult [in reach]
repeat_add [in reach]
Rexpbound [in reach]
RPP [in reach]
RSn_bound [in reach]
R0_bound [in reach]
S
separate_singleton [in eqrel]size_adds_all [in finfun]
size_all_seq [in finfun]
size_bound_An [in reach]
size_bound_RSn [in reach]
size_bound_R0 [in reach]
size_eevolution_seq [in reach]
size_evolution_seq [in reach]
size_gens_cyclicgroup [in fingroup]
size_gens_tuplegroup [in fingroup]
size_gens_wp [in fingroup]
size_stepn_seq [in reach]
stepe_econf [in reach]
stepe_eqd [in reach]
stepe_Q [in reach]
stepe_S [in reach]
stepe_X0 [in reach]
stepe_X1 [in reach]
step_eevolution [in reach]
sub_n0 [in reach]
sum_seq_cat [in fingroup]
sum_seq_flatten [in fingroup]
sum_unit_vector [in fingroup]
U
uniq_div [in general]uniq_mod [in general]
unitrP [in fingroup]
unit_vector_gen [in fingroup]
update_eqrel [in reach]
X
XiX_action1 [in reach]XiX_iXX [in reach]
Constructor Index
D
divexr [in general]F
Fgraph [in finfun]M
m_edge [in reach]m_jump [in reach]
Inductive Index
A
abstraction [in reach]D
diveuclr [in general]E
eqrelType [in eqrel]F
fgraphType [in finfun]G
graph [in graphs]I
ieqrel [in eqrel]J
jag [in reach]M
move [in reach]S
state_space [in reach]Definition Index
A
A [in reach]abstractionG [in reach]
action0iX [in reach]
action0X [in reach]
action1iX [in reach]
action1X [in reach]
act_CG [in graphs]
adds_all [in finfun]
all_seq [in finfun]
An_boundU [in main]
AU [in main]
C
canonical_fun [in eqrel]carrier_wp [in fingroup]
cayleyGraph [in graphs]
coal [in reach]
coalE [in reach]
commutative [in fingroup]
conf [in reach]
cyclicgroup [in fingroup]
D
degree_CG [in graphs]div [in general]
dom_abstr [in reach]
dom_abstr_rel [in reach]
E
econf [in reach]econfP [in reach]
econf_conf [in reach]
edgegroup_CG [in graphs]
edges_CG [in graphs]
edge_of_nat [in graphs]
eevolution [in reach]
eevolution_seq [in reach]
eg_orderP_CG [in graphs]
eg_order_CG [in graphs]
eg_order_positive_CG [in graphs]
env [in reach]
eqclass [in eqrel]
eqclasses [in eqrel]
eqdQobs [in reach]
eqdQX [in reach]
eqd_ieqrel [in eqrel]
eqfgraph [in finfun]
eqrel_of_ieqrel [in eqrel]
eqrel_of_ieqrelType [in eqrel]
equals_ieqrel [in eqrel]
equiv [in reach]
evolution [in reach]
evolution_seq [in reach]
evolution_to_coal [in reach]
exp [in general]
expbound [in reach]
F
fact [in general]fgraph_enum [in finfun]
fgraph_enum_dep [in finfun]
fgraph_enum_lenP [in finfun]
fgraph_enum_val [in finfun]
fgraph_of_fun [in finfun]
flatten [in general]
free [in fingroup]
fun_of_fgraph [in finfun]
fval [in finfun]
G
generators [in fingroup]gens_cyclicgroup [in fingroup]
gens_tuplegroup [in fingroup]
gens_U [in graphs]
gens_wp [in fingroup]
graphCR [in graphs]
graphU [in graphs]
gU [in main]
I
ieqrelType [in eqrel]ieqrelType_of_eqrel [in eqrel]
ieqrel_enum [in eqrel]
ieqrel_of_eqrel [in eqrel]
ieqrel_pred [in eqrel]
iforall [in boollogic]
iforall2 [in boollogic]
iforall3 [in boollogic]
initiX [in reach]
initX [in reach]
init_econf [in reach]
inv_modulo [in fingroup]
inv_wp [in fingroup]
irefl_dom [in reach]
isym_dom [in reach]
is_singleton [in reach]
is_singleton_class [in eqrel]
is_some [in general]
iterate_make_moves [in reach]
itrans_dom [in reach]
iX [in reach]
iXX [in reach]
J
join [in eqrel]join_rel [in reach]
M
make_moves [in reach]make_moves_from [in reach]
map_option [in general]
max [in general]
max [in reach]
measure_abstG [in reach]
mkunitG [in fingroup]
mkunitH [in fingroup]
mk_econf [in reach]
mk_ord [in graphs]
mod [in general]
move_eqd [in reach]
multiply [in general]
mul_modulo [in fingroup]
mul_wp [in fingroup]
N
next [in reach]nodes_of_conf [in main]
nodes_visited [in main]
node_s_CG [in graphs]
node_t_CG [in graphs]
NoneF [in general]
O
obs [in reach]obs_abstG [in reach]
one_cyclicgroup [in fingroup]
option_enum [in general]
option_eqd [in general]
order [in fingroup]
P
pickeqc [in eqrel]piQ [in reach]
piS [in reach]
piX [in reach]
predictableiX [in reach]
predictableX [in reach]
Prop3 [in main]
Q
quotient [in eqrel]quotient_map [in eqrel]
R
R [in reach]realisesiX [in reach]
realisesX [in reach]
realises1iX [in reach]
realises1X [in reach]
realises2iX [in reach]
realises2X [in reach]
realises3iX [in reach]
realises3X [in reach]
refl_dom [in reach]
RSn_boundU [in main]
RU [in main]
R0_boundU [in main]
S
separate [in eqrel]separate_rel [in reach]
setAC [in reach]
setACP [in reach]
set_rel [in eqrel]
sim [in reach]
sim_rel [in reach]
SomeF [in general]
state_space_G [in reach]
state_space_G_action [in reach]
state_space_G_obs [in reach]
stepe [in reach]
stepn [in reach]
stepn_seq [in reach]
sum_seq [in fingroup]
sym_dom [in reach]
T
transitive [in fingroup]trans_dom [in reach]
tuplegroup [in fingroup]
U
union [in reach]unit_vector [in fingroup]
unit_wp [in fingroup]
update [in reach]
V
vertices_CG [in graphs]W
wp [in fingroup]X
X [in reach]XiX [in reach]
Z
zip [in general]Library Index
B
boollogicE
eqrelF
finfunfingroup
G
generalgraphs
M
mainR
reach| 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 | _ | (485 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 | _ | (2 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 | _ | (293 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 | _ | (4 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 | _ | (9 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 | _ | (169 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 | _ | (8 entries) |
This page has been generated by coqdoc