| 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 | (2340 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 | (54 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (365 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 | (27 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 | (1162 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 | (46 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 | (6 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (102 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 | (106 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 | (26 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 | (56 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 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 | (23 entries) |
Global Index
A
above_largest [lemma, in graphs.preliminaries]AddEdge [section, in graphs.treewidth]
AddEdge.discT [variable, in graphs.treewidth]
AddEdge.T [variable, in graphs.treewidth]
AddEdge.T' [variable, in graphs.treewidth]
AddEdge.t0 [variable, in graphs.treewidth]
AddEdge.t1 [variable, in graphs.treewidth]
AddNode [section, in graphs.sgraph]
AddNode.G [variable, in graphs.sgraph]
AddNode.N [variable, in graphs.sgraph]
add_edge_induced_iso [lemma, in graphs.cp_minor]
add_edge_split_disjoint [lemma, in graphs.excluded]
add_edge_split_connected [lemma, in graphs.excluded]
add_edge_separation [lemma, in graphs.excluded]
add_node_complete [lemma, in graphs.sgraph]
add_node_lift_Path [lemma, in graphs.sgraph]
add_node [definition, in graphs.sgraph]
add_node_irrefl [lemma, in graphs.sgraph]
add_node_sym [lemma, in graphs.sgraph]
add_node_rel [definition, in graphs.sgraph]
add_edge_keep_connected_l [lemma, in graphs.sgraph]
add_edge_avoid [lemma, in graphs.sgraph]
add_edge_pathC [lemma, in graphs.sgraph]
add_edge_connected_sym [lemma, in graphs.sgraph]
add_edge_sym [lemma, in graphs.sgraph]
add_edgeC [lemma, in graphs.sgraph]
add_edge_connected [lemma, in graphs.sgraph]
add_edge_Path [lemma, in graphs.sgraph]
add_edge [definition, in graphs.sgraph]
add_edge_irrefl_ [lemma, in graphs.sgraph]
add_edge_sym_ [lemma, in graphs.sgraph]
add_edge_rel [definition, in graphs.sgraph]
add_edge_is_forest [lemma, in graphs.treewidth]
add_edge_break [lemma, in graphs.treewidth]
add_vertex_iso [instance, in graphs.mgraph]
add_vlabel_edge [lemma, in graphs.mgraph]
add_vlabel_two [lemma, in graphs.mgraph]
add_vlabel_mon0 [lemma, in graphs.mgraph]
add_vlabel_unit [lemma, in graphs.mgraph]
add_vlabel_C [lemma, in graphs.mgraph]
add_vlabel_iso [lemma, in graphs.mgraph]
add_vlabel_iso' [lemma, in graphs.mgraph]
add_vlabel_iso'' [lemma, in graphs.mgraph]
add_edge_vlabel [lemma, in graphs.mgraph]
add_edge_rev [lemma, in graphs.mgraph]
add_edge_C [lemma, in graphs.mgraph]
add_edge_iso [lemma, in graphs.mgraph]
add_edge_iso' [lemma, in graphs.mgraph]
add_edge_iso'' [lemma, in graphs.mgraph]
add_vertex [definition, in graphs.mgraph]
add_vlabel [definition, in graphs.mgraph]
add_edge [definition, in graphs.mgraph]
add_test_cong [abbreviation, in graphs.mgraph2]
add_test [abbreviation, in graphs.mgraph2]
add_vlabel2_mon0 [lemma, in graphs.mgraph2]
add_vlabel2_edge [lemma, in graphs.mgraph2]
add_vlabel2_two [lemma, in graphs.mgraph2]
add_vlabel2_unit' [lemma, in graphs.mgraph2]
add_vlabel2_unit [lemma, in graphs.mgraph2]
add_vlabel2_C [lemma, in graphs.mgraph2]
add_vlabel2_iso [lemma, in graphs.mgraph2]
add_vlabel2_iso' [lemma, in graphs.mgraph2]
add_vlabel2_iso'' [lemma, in graphs.mgraph2]
add_edge2_vlabel [lemma, in graphs.mgraph2]
add_edge2_rev [lemma, in graphs.mgraph2]
add_edge2_C [lemma, in graphs.mgraph2]
add_edge2_iso [lemma, in graphs.mgraph2]
add_edge2_iso' [lemma, in graphs.mgraph2]
add_edge2_iso'' [lemma, in graphs.mgraph2]
add_vertex2_iso [instance, in graphs.mgraph2]
add_vlabel2 [definition, in graphs.mgraph2]
add_edge2 [definition, in graphs.mgraph2]
add_vertex2 [definition, in graphs.mgraph2]
add_node_minor [lemma, in graphs.minor]
adjacent [definition, in graphs.skeleton]
adjacentI [lemma, in graphs.skeleton]
adjacentP [lemma, in graphs.skeleton]
adjacent_induced [lemma, in graphs.skeleton]
adjacent_edge [lemma, in graphs.skeleton]
adjacent_sym [lemma, in graphs.skeleton]
admissible [definition, in graphs.mgraph2_tw2]
admissible_eqv_clot [lemma, in graphs.mgraph2_tw2]
admitted_case [axiom, in graphs.preliminaries]
all_cons [lemma, in graphs.preliminaries]
avoid_nonseperator [lemma, in graphs.connectivity]
A10 [projection, in graphs.pttdom]
A10_ [projection, in graphs.ptt]
A11 [projection, in graphs.ptt]
A12 [projection, in graphs.ptt]
A13 [projection, in graphs.pttdom]
A13_ [lemma, in graphs.ptt]
A14 [projection, in graphs.pttdom]
A14_ [lemma, in graphs.ptt]
B
b [section, in graphs.finite_quotient]bag [definition, in graphs.checkpoint]
bagP [lemma, in graphs.checkpoint]
bagPn [lemma, in graphs.checkpoint]
bag_interval_cap [lemma, in graphs.checkpoint]
bag_cp [lemma, in graphs.checkpoint]
bag_disj [lemma, in graphs.checkpoint]
bag_exit_edge [lemma, in graphs.checkpoint]
bag_exit' [lemma, in graphs.checkpoint]
bag_exit [lemma, in graphs.checkpoint]
bag_sub_sinterval [lemma, in graphs.checkpoint]
bag_nontrivial [lemma, in graphs.checkpoint]
bag_id [lemma, in graphs.checkpoint]
bag_edges_disj [lemma, in graphs.skeleton]
below_smallest [lemma, in graphs.preliminaries]
bgraph [definition, in graphs.skeleton]
bgraph_eq_io [lemma, in graphs.skeleton]
bigcup_set1 [lemma, in graphs.preliminaries]
bigD1 [lemma, in graphs.structures]
bigID [lemma, in graphs.structures]
big_unit [lemma, in graphs.structures]
big_sum [lemma, in graphs.structures]
big_pred1 [lemma, in graphs.structures]
big_pred1_eq [lemma, in graphs.structures]
big_seq1 [lemma, in graphs.structures]
big_split [lemma, in graphs.structures]
big_cat [lemma, in graphs.structures]
big_mkcond [lemma, in graphs.structures]
bij [record, in graphs.bij]
Bij [constructor, in graphs.bij]
Bij [section, in graphs.finmap_plus]
bij [library]
BijCast [section, in graphs.finmap_plus]
BijCast.A [variable, in graphs.finmap_plus]
BijCast.A' [variable, in graphs.finmap_plus]
BijCast.eqA [variable, in graphs.finmap_plus]
BijCast.T [variable, in graphs.finmap_plus]
bijD1 [definition, in graphs.bij]
BijD1 [section, in graphs.bij]
bijD1_bwd [definition, in graphs.bij]
bijD1_fwd [definition, in graphs.bij]
BijD1.T [variable, in graphs.bij]
BijD1.z [variable, in graphs.bij]
bijK [projection, in graphs.bij]
bijK' [projection, in graphs.bij]
BijT [section, in graphs.bij]
BijT.inP [variable, in graphs.bij]
BijT.P [variable, in graphs.bij]
BijT.T [variable, in graphs.bij]
bij_perm_enum [lemma, in graphs.bij]
bij_same [lemma, in graphs.bij]
bij_sumA [lemma, in graphs.bij]
bij_sumC [lemma, in graphs.bij]
bij_Equivalence [instance, in graphs.bij]
bij_comp [definition, in graphs.bij]
bij_sym [definition, in graphs.bij]
bij_id [definition, in graphs.bij]
bij_eqLR [lemma, in graphs.bij]
bij_imsetC [lemma, in graphs.bij]
bij_mem_imset [lemma, in graphs.bij]
bij_injective' [lemma, in graphs.bij]
bij_injective [lemma, in graphs.bij]
bij_bijective' [lemma, in graphs.bij]
bij_bijective [lemma, in graphs.bij]
bij_bwd [projection, in graphs.bij]
bij_fwd [projection, in graphs.bij]
bij_castE [lemma, in graphs.finmap_plus]
bij_cast [definition, in graphs.finmap_plus]
bij_setD [definition, in graphs.finmap_plus]
bij_surj [lemma, in graphs.preliminaries]
bij_card_eq [lemma, in graphs.preliminaries]
bij_quotE' [lemma, in graphs.finite_quotient]
bij_quotE [lemma, in graphs.finite_quotient]
bij_quot [definition, in graphs.finite_quotient]
Bij.g [variable, in graphs.finmap_plus]
Bij.G [variable, in graphs.finmap_plus]
Bij.g_inj [variable, in graphs.finmap_plus]
Bij.T [variable, in graphs.finmap_plus]
Bij.vset [variable, in graphs.finmap_plus]
bipartition [definition, in graphs.connectivity]
bip_separation_vcover [lemma, in graphs.connectivity]
bool_option_unit [definition, in graphs.bij]
bool_two [lemma, in graphs.bij]
bool_swap [definition, in graphs.bij]
Bounded [section, in graphs.bounded]
bounded [library]
Bounded.aT [variable, in graphs.bounded]
Bounded.F [variable, in graphs.bounded]
Bounded.F_wf [variable, in graphs.bounded]
Bounded.measure [variable, in graphs.bounded]
Bounded.P [variable, in graphs.bounded]
Bounded.rT [variable, in graphs.bounded]
Bounded.x0 [variable, in graphs.bounded]
b.e [variable, in graphs.finite_quotient]
b.h [variable, in graphs.finite_quotient]
b.S [variable, in graphs.finite_quotient]
b.T [variable, in graphs.finite_quotient]
C
can_bijD1_bwd [lemma, in graphs.bij]can_bijD1_fwd [lemma, in graphs.bij]
can_vset' [lemma, in graphs.finmap_plus]
can_vset [lemma, in graphs.finmap_plus]
can_irred_of [lemma, in graphs.digraph]
car [projection, in graphs.structures]
cardsCT [lemma, in graphs.preliminaries]
cardsDsub [lemma, in graphs.finmap_plus]
cardsI [lemma, in graphs.preliminaries]
cardsIsub [lemma, in graphs.finmap_plus]
cards2P [lemma, in graphs.preliminaries]
cards3 [lemma, in graphs.preliminaries]
card_matching_of [lemma, in graphs.connectivity]
card_dimatching_of [lemma, in graphs.connectivity]
card_bij [lemma, in graphs.bij]
card_void [lemma, in graphs.preliminaries]
card_le1P [lemma, in graphs.preliminaries]
card_gt2P [lemma, in graphs.preliminaries]
card_gt1P [lemma, in graphs.preliminaries]
card_gtnP [lemma, in graphs.preliminaries]
card_le1 [lemma, in graphs.preliminaries]
card_ltnT [lemma, in graphs.preliminaries]
card_val [lemma, in graphs.skeleton]
card_del_edge [lemma, in graphs.digraph]
card1P [lemma, in graphs.preliminaries]
card12 [lemma, in graphs.preliminaries]
cases_without_edge [lemma, in graphs.excluded]
castL [definition, in graphs.digraph]
cast_proof [lemma, in graphs.finmap_plus]
CEquivalence [abbreviation, in graphs.structures]
checkpoint [library]
CheckpointOrder [section, in graphs.checkpoint]
CheckpointOrder.conn_io [variable, in graphs.checkpoint]
CheckpointOrder.G [variable, in graphs.checkpoint]
CheckpointOrder.i [variable, in graphs.checkpoint]
CheckpointOrder.o [variable, in graphs.checkpoint]
CheckPoints [section, in graphs.checkpoint]
CheckpointsAndMinors [section, in graphs.cp_minor]
CheckpointsAndMinors.conn_G [variable, in graphs.cp_minor]
CheckpointsAndMinors.G [variable, in graphs.cp_minor]
CheckPoints.G [variable, in graphs.checkpoint]
CheckPoints.G_conn [variable, in graphs.checkpoint]
CheckPoints.G_conn' [variable, in graphs.checkpoint]
_ ⋄ _ [notation, in graphs.checkpoint]
CK4F [definition, in graphs.extraction_def]
CK4F_lens_rest [lemma, in graphs.extraction_def]
CK4F_remove_loops [lemma, in graphs.extraction_def]
CK4F_remove_edges [lemma, in graphs.extraction_def]
CK4F_split_cpM [lemma, in graphs.extraction_def]
CK4F_split_cpR [lemma, in graphs.extraction_def]
CK4F_split_cpL [lemma, in graphs.extraction_def]
CK4F_lens [lemma, in graphs.extraction_def]
CK4F_redirect [lemma, in graphs.extraction_def]
CK4F_one [lemma, in graphs.extraction_def]
CK4F_remove_component [lemma, in graphs.extraction_def]
CK4F_induced2 [lemma, in graphs.extraction_def]
CK4F_sub [lemma, in graphs.extraction_def]
CK4F_igraph [lemma, in graphs.extraction_def]
CK4F_component [lemma, in graphs.extraction_top]
clique [definition, in graphs.sgraph]
cliqueb [definition, in graphs.sgraph]
cliqueP [lemma, in graphs.sgraph]
cliquePn [lemma, in graphs.sgraph]
Cliques [section, in graphs.sgraph]
Cliques.G [variable, in graphs.sgraph]
clique1 [lemma, in graphs.sgraph]
clique2 [lemma, in graphs.sgraph]
cnv [projection, in graphs.pttdom]
cnvdot [projection, in graphs.pttdom]
cnvdot_ [projection, in graphs.ptt]
cnvI [projection, in graphs.pttdom]
cnvI_ [projection, in graphs.ptt]
cnvpar [projection, in graphs.pttdom]
cnvpar_ [projection, in graphs.ptt]
cnvtop [lemma, in graphs.ptt]
cnvtst [lemma, in graphs.pttdom]
cnv_test [lemma, in graphs.pttdom]
cnv_inj [lemma, in graphs.pttdom]
cnv_eqv [projection, in graphs.pttdom]
cnv_eqv_ [projection, in graphs.ptt]
cnv_iso2 [instance, in graphs.mgraph2]
cnv1 [lemma, in graphs.pttdom]
cnv2dot [lemma, in graphs.mgraph2]
cnv2I [lemma, in graphs.mgraph2]
cnv2par [lemma, in graphs.mgraph2]
codom_Some [lemma, in graphs.preliminaries]
collapse_bags [lemma, in graphs.cp_minor]
compatible [definition, in graphs.mgraph2_tw2]
complete [definition, in graphs.sgraph]
complete_irrefl [lemma, in graphs.sgraph]
complete_sym [lemma, in graphs.sgraph]
complete_rel [definition, in graphs.sgraph]
component [definition, in graphs.extraction_def]
componentless_top [lemma, in graphs.extraction_iso]
componentless_one [lemma, in graphs.extraction_iso]
components [definition, in graphs.sgraph]
components_subset [lemma, in graphs.sgraph]
components_nonempty [lemma, in graphs.sgraph]
components_pblockP [lemma, in graphs.sgraph]
component_in [definition, in graphs.excluded]
component_exchange [lemma, in graphs.sgraph]
component_of_components [lemma, in graphs.sgraph]
component_of [definition, in graphs.sgraph]
component_exit [lemma, in graphs.sgraph]
component_induced [lemma, in graphs.extraction_top]
component_hom [lemma, in graphs.skeleton]
component_can_e' [lemma, in graphs.skeleton]
component_can_e [lemma, in graphs.skeleton]
component_can_v' [lemma, in graphs.skeleton]
component_can_v [lemma, in graphs.skeleton]
component_e' [definition, in graphs.skeleton]
component_e [definition, in graphs.skeleton]
component_v' [definition, in graphs.skeleton]
component_v [definition, in graphs.skeleton]
component1 [definition, in graphs.extraction_top]
comp_dom2_redirect [lemma, in graphs.extraction_iso]
comp_exit [lemma, in graphs.extraction_iso]
conn [abbreviation, in graphs.excluded]
conn [abbreviation, in graphs.excluded]
connected [definition, in graphs.sgraph]
connectedb [definition, in graphs.sgraph]
connectedI_clique [lemma, in graphs.excluded]
connectedP [lemma, in graphs.sgraph]
connectedTE [lemma, in graphs.sgraph]
connectedTI [lemma, in graphs.sgraph]
connectedU_edge [lemma, in graphs.sgraph]
connectedU_common_point [lemma, in graphs.sgraph]
connected_component_set [lemma, in graphs.extraction_def]
connected_induced [lemma, in graphs.extraction_def]
connected_interiorR [lemma, in graphs.sgraph]
connected_interior [lemma, in graphs.sgraph]
connected_add_node [lemma, in graphs.sgraph]
connected_component_of [lemma, in graphs.sgraph]
connected_one_component [lemma, in graphs.sgraph]
connected_in_components [lemma, in graphs.sgraph]
connected_card_gt1 [lemma, in graphs.sgraph]
connected_induced [lemma, in graphs.sgraph]
connected_in_subgraph [lemma, in graphs.sgraph]
connected_path [lemma, in graphs.sgraph]
connected_center [lemma, in graphs.sgraph]
connected_restrict_in [lemma, in graphs.sgraph]
connected_restrict [lemma, in graphs.sgraph]
connected_bag [lemma, in graphs.checkpoint]
connected_interval [lemma, in graphs.checkpoint]
connected_CP_closed [lemma, in graphs.checkpoint]
connected_cp_closed [lemma, in graphs.checkpoint]
connected_igraph [lemma, in graphs.skeleton]
connected_bgraph [lemma, in graphs.skeleton]
connected_skeleton [lemma, in graphs.skeleton]
connected_skeleton' [lemma, in graphs.skeleton]
connected0 [lemma, in graphs.sgraph]
connected1 [lemma, in graphs.sgraph]
connected2 [lemma, in graphs.sgraph]
connectivity [library]
connector [record, in graphs.connectivity]
connectorC_edge [lemma, in graphs.connectivity]
connector_dimatching [lemma, in graphs.connectivity]
connector_nodes [lemma, in graphs.connectivity]
connector_cat [lemma, in graphs.connectivity]
connector_sep [lemma, in graphs.connectivity]
connector_extend [lemma, in graphs.connectivity]
connector_eq [lemma, in graphs.connectivity]
connector_right [lemma, in graphs.connectivity]
connector_left [lemma, in graphs.connectivity]
connector_lst [lemma, in graphs.connectivity]
connector_fst [lemma, in graphs.connectivity]
connectRI [lemma, in graphs.sgraph]
connectUP [lemma, in graphs.preliminaries]
connect_range [lemma, in graphs.sgraph]
connect_restrict_case [lemma, in graphs.sgraph]
connect_img [lemma, in graphs.preliminaries]
connect_symI [lemma, in graphs.preliminaries]
connect_restrict_mono [lemma, in graphs.preliminaries]
connect_mono [lemma, in graphs.preliminaries]
conn_disjoint [projection, in graphs.connectivity]
conn_end [projection, in graphs.connectivity]
conn_begin [projection, in graphs.connectivity]
conn_irred [projection, in graphs.connectivity]
consistent [definition, in graphs.mgraph]
consistentT [lemma, in graphs.mgraph]
consistentTT [lemma, in graphs.mgraph]
consistentU [lemma, in graphs.mgraph]
consistent_setD [lemma, in graphs.skeleton]
consistent_del1 [lemma, in graphs.mgraph]
const0 [definition, in graphs.bounded]
const0_eq [lemma, in graphs.bounded]
const0_rec [definition, in graphs.bounded]
contraNnot [lemma, in graphs.preliminaries]
contraPeq [lemma, in graphs.preliminaries]
contraPN [lemma, in graphs.preliminaries]
contraPneq [lemma, in graphs.preliminaries]
contraPT [lemma, in graphs.preliminaries]
contraTnot [lemma, in graphs.preliminaries]
contra_notT [lemma, in graphs.preliminaries]
cover_matching [lemma, in graphs.connectivity]
CP [definition, in graphs.checkpoint]
cp [definition, in graphs.checkpoint]
cpNI [lemma, in graphs.checkpoint]
cpN_trans [lemma, in graphs.checkpoint]
cpo [definition, in graphs.checkpoint]
cpo_cp [lemma, in graphs.checkpoint]
cpo_max [lemma, in graphs.checkpoint]
cpo_min [lemma, in graphs.checkpoint]
cpo_order [lemma, in graphs.checkpoint]
cpo_antisym [lemma, in graphs.checkpoint]
cpo_total [lemma, in graphs.checkpoint]
cpo_trans [lemma, in graphs.checkpoint]
cpo_refl [lemma, in graphs.checkpoint]
cpP [lemma, in graphs.checkpoint]
cpPn [lemma, in graphs.checkpoint]
CProper [section, in graphs.structures]
CProper [abbreviation, in graphs.structures]
CProper.A [variable, in graphs.structures]
CProper.B [variable, in graphs.structures]
CProper.C [variable, in graphs.structures]
CProper.f [variable, in graphs.structures]
CProper.g [variable, in graphs.structures]
CProper.Hf [variable, in graphs.structures]
CProper.Hg [variable, in graphs.structures]
CProper.R [variable, in graphs.structures]
CProper.S [variable, in graphs.structures]
CProper.T [variable, in graphs.structures]
CProper1 [lemma, in graphs.structures]
CProper2 [lemma, in graphs.structures]
cpTI [lemma, in graphs.checkpoint]
cpxx [lemma, in graphs.checkpoint]
CP_tree_sinterval [lemma, in graphs.checkpoint]
cp_sub_interval [lemma, in graphs.checkpoint]
CP_tree_paths [lemma, in graphs.checkpoint]
CP_path [lemma, in graphs.checkpoint]
CP_base [lemma, in graphs.checkpoint]
CP_closed [lemma, in graphs.checkpoint]
CP_mono [lemma, in graphs.checkpoint]
CP_extensive [lemma, in graphs.checkpoint]
CP_set2 [lemma, in graphs.checkpoint]
cp_neighbours [lemma, in graphs.checkpoint]
cp_tighten [lemma, in graphs.checkpoint]
cp_tightenR [lemma, in graphs.checkpoint]
cp_widen [lemma, in graphs.checkpoint]
cp_widenR [lemma, in graphs.checkpoint]
cp_mid [lemma, in graphs.checkpoint]
cp_triangle [lemma, in graphs.checkpoint]
cp_sym [lemma, in graphs.checkpoint]
cp_minor [library]
cr [definition, in graphs.preliminaries]
crK [lemma, in graphs.preliminaries]
C3 [definition, in graphs.sgraph]
D
decC [lemma, in graphs.skeleton]decE [lemma, in graphs.skeleton]
decompL [definition, in graphs.treewidth]
DecompTheory [section, in graphs.treewidth]
DecompTheory.B [variable, in graphs.treewidth]
DecompTheory.decD [variable, in graphs.treewidth]
DecompTheory.G [variable, in graphs.treewidth]
DecompTheory.T [variable, in graphs.treewidth]
decompU [definition, in graphs.treewidth]
decomp_dom [lemma, in graphs.mgraph2_tw2]
decomp_cnv [lemma, in graphs.mgraph2_tw2]
decomp_dot2 [lemma, in graphs.mgraph2_tw2]
decomp_par2 [lemma, in graphs.mgraph2_tw2]
decomp_quot [lemma, in graphs.mgraph2_tw2]
decomp_clique [lemma, in graphs.treewidth]
decomp_link [lemma, in graphs.treewidth]
decomp_small [lemma, in graphs.treewidth]
decomp_iso [lemma, in graphs.treewidth]
decomp_iso2 [lemma, in graphs.skeleton]
DelEdge [section, in graphs.digraph]
DelEdge.a [variable, in graphs.digraph]
DelEdge.ab [variable, in graphs.digraph]
DelEdge.b [variable, in graphs.digraph]
DelEdge.G [variable, in graphs.digraph]
del_edge_connector [lemma, in graphs.connectivity]
del_edge_liftS [definition, in graphs.digraph]
del_edge_lift_proof [lemma, in graphs.digraph]
del_edge_path_case [lemma, in graphs.digraph]
del_edge [definition, in graphs.digraph]
del_rel [definition, in graphs.digraph]
derived [section, in graphs.pttdom]
derived [section, in graphs.ptt]
derived.X [variable, in graphs.pttdom]
derived.X [variable, in graphs.ptt]
[ _ ] [notation, in graphs.pttdom]
dhom_comp [lemma, in graphs.digraph]
dhom_id [lemma, in graphs.digraph]
DiGraph [abbreviation, in graphs.digraph]
diGraph [abbreviation, in graphs.digraph]
digraph [library]
DiGraphTheory [section, in graphs.digraph]
DiGraphTheory.D [variable, in graphs.digraph]
DiGraphTheory.Fixed [section, in graphs.digraph]
DiGraphTheory.Fixed.p [variable, in graphs.digraph]
DiGraphTheory.Fixed.q [variable, in graphs.digraph]
DiGraphTheory.Fixed.x [variable, in graphs.digraph]
DiGraphTheory.Fixed.y [variable, in graphs.digraph]
DiGraphTheory.Fixed.z [variable, in graphs.digraph]
digraph_of [definition, in graphs.mgraph]
diHall [lemma, in graphs.connectivity]
dimatching [definition, in graphs.connectivity]
dimatching_of [definition, in graphs.connectivity]
DiPathTheory [section, in graphs.digraph]
DiPathTheory.Finite [section, in graphs.digraph]
DiPathTheory.Finite.x [variable, in graphs.digraph]
DiPathTheory.Finite.y [variable, in graphs.digraph]
DiPathTheory.G [variable, in graphs.digraph]
DiPathTheory.IPath [section, in graphs.digraph]
DiPathTheory.IPath.x [variable, in graphs.digraph]
DiPathTheory.IPath.y [variable, in graphs.digraph]
disconnected [definition, in graphs.sgraph]
disconnectedE [lemma, in graphs.sgraph]
disjointE [lemma, in graphs.preliminaries]
disjointFl [lemma, in graphs.preliminaries]
disjointFr [lemma, in graphs.preliminaries]
disjointNI [lemma, in graphs.preliminaries]
disjointP [lemma, in graphs.preliminaries]
disjointsU [lemma, in graphs.preliminaries]
disjoints1 [lemma, in graphs.preliminaries]
disjointW [lemma, in graphs.preliminaries]
disjoint_transR [lemma, in graphs.preliminaries]
disjoint_transL [definition, in graphs.preliminaries]
disjoint_exists [lemma, in graphs.preliminaries]
disjoint_part [lemma, in graphs.digraph]
Disjoint3 [section, in graphs.preliminaries]
disjoint3P [lemma, in graphs.preliminaries]
disjoint3_cases [inductive, in graphs.preliminaries]
Disjoint3.A [variable, in graphs.preliminaries]
Disjoint3.B [variable, in graphs.preliminaries]
Disjoint3.C [variable, in graphs.preliminaries]
Disjoint3.T [variable, in graphs.preliminaries]
diso [record, in graphs.digraph]
Diso [constructor, in graphs.digraph]
diso_Equivalence [instance, in graphs.digraph]
diso_comp [definition, in graphs.digraph]
diso_sym [definition, in graphs.digraph]
diso_id [definition, in graphs.digraph]
diso_hom' [projection, in graphs.digraph]
diso_hom [projection, in graphs.digraph]
diso_v [projection, in graphs.digraph]
Diso' [lemma, in graphs.digraph]
Diso'' [lemma, in graphs.digraph]
Dis3In1 [constructor, in graphs.preliminaries]
Dis3In2 [constructor, in graphs.preliminaries]
Dis3In3 [constructor, in graphs.preliminaries]
Dis3Notin [constructor, in graphs.preliminaries]
di_edge [abbreviation, in graphs.digraph]
dom [projection, in graphs.pttdom]
domE [projection, in graphs.ptt]
domtst [lemma, in graphs.pttdom]
dom_tst [lemma, in graphs.pttdom]
dom_test [lemma, in graphs.pttdom]
dom_eqv [projection, in graphs.pttdom]
dom_eqv_ [instance, in graphs.ptt]
dom_iso2 [instance, in graphs.mgraph2]
dom2E [lemma, in graphs.mgraph2]
dot [projection, in graphs.pttdom]
dotA [projection, in graphs.pttdom]
dotA_ [projection, in graphs.ptt]
dotcnv [lemma, in graphs.pttdom]
dotx1 [projection, in graphs.pttdom]
dotx1_ [projection, in graphs.ptt]
dot_test [lemma, in graphs.pttdom]
dot_eqv [projection, in graphs.pttdom]
dot_eqv_ [projection, in graphs.ptt]
dot_iso2 [instance, in graphs.mgraph2]
dot1x [lemma, in graphs.pttdom]
dot2A [lemma, in graphs.mgraph2]
dot2Aflat [lemma, in graphs.mgraph2]
dot2one [lemma, in graphs.mgraph2]
dot2one' [lemma, in graphs.mgraph2]
dot2unit_l [lemma, in graphs.mgraph2]
dot2unit_r' [lemma, in graphs.mgraph2]
dot2unit_r [lemma, in graphs.mgraph2]
E
eC [abbreviation, in graphs.finite_quotient]edge [projection, in graphs.mgraph]
edgeless_bag [lemma, in graphs.extraction_def]
edgeLP [lemma, in graphs.digraph]
edgep [definition, in graphs.digraph]
edgep_proof [lemma, in graphs.digraph]
edges [definition, in graphs.connectivity]
edges [definition, in graphs.mgraph]
edgesP [lemma, in graphs.connectivity]
edges_at_iso [lemma, in graphs.mgraph]
edges_in1 [lemma, in graphs.mgraph]
edges_in [definition, in graphs.mgraph]
edges_at [definition, in graphs.mgraph]
edge_comp [lemma, in graphs.skeleton]
edge_setN [lemma, in graphs.skeleton]
edge_set_component [lemma, in graphs.skeleton]
edge_component [lemma, in graphs.skeleton]
edge_set_adj [lemma, in graphs.skeleton]
edge_diso' [lemma, in graphs.digraph]
edge_diso [lemma, in graphs.digraph]
edge_rel [projection, in graphs.digraph]
edge_in_set [lemma, in graphs.mgraph]
edge_set1 [lemma, in graphs.mgraph]
edge_set [definition, in graphs.mgraph]
edge_graph [definition, in graphs.mgraph]
edge_graph2_iso [instance, in graphs.mgraph2]
edge_graph2 [definition, in graphs.mgraph2]
edge_surjective [definition, in graphs.minor]
edone [library]
elabel [projection, in graphs.mgraph]
elabel_iso' [lemma, in graphs.mgraph]
elabel_iso [lemma, in graphs.mgraph]
elabel_hom [projection, in graphs.mgraph]
elem_of [projection, in graphs.pttdom]
empty_uniqe [lemma, in graphs.preliminaries]
endpoint [projection, in graphs.mgraph]
endpoint_iso' [lemma, in graphs.mgraph]
endpoint_iso [lemma, in graphs.mgraph]
endpoint_hom [projection, in graphs.mgraph]
enum_unit [lemma, in graphs.preliminaries]
enum_sum [lemma, in graphs.preliminaries]
eqb_negR [lemma, in graphs.preliminaries]
eqmodE [lemma, in graphs.finite_quotient]
equiv [library]
Equivalence [section, in graphs.preliminaries]
equivalence_partition_gt1P [lemma, in graphs.preliminaries]
equivalence_rel_of_sym [lemma, in graphs.preliminaries]
Equivalence.e [variable, in graphs.preliminaries]
Equivalence.T [variable, in graphs.preliminaries]
equiv_of_trans [definition, in graphs.preliminaries]
equiv_of_sym [lemma, in graphs.preliminaries]
equiv_of_refl [definition, in graphs.preliminaries]
equiv_of [definition, in graphs.preliminaries]
equiv_comp_pi [lemma, in graphs.finite_quotient]
equiv_compE [lemma, in graphs.finite_quotient]
equiv_comp [definition, in graphs.finite_quotient]
equiv_of_fn [lemma, in graphs.equiv]
equiv_of_nn [lemma, in graphs.equiv]
equiv_of_ff [lemma, in graphs.equiv]
equiv_rel_Equivalence [instance, in graphs.equiv]
equiv_of_sub' [lemma, in graphs.equiv]
equiv_of_sub [lemma, in graphs.equiv]
equiv_of_transfer [lemma, in graphs.equiv]
equiv_ofE [lemma, in graphs.equiv]
equiv_of_class [lemma, in graphs.equiv]
equiv_clot_Kl [lemma, in graphs.mgraph]
Eqv [projection, in graphs.structures]
eqv [projection, in graphs.structures]
eqvbN [lemma, in graphs.pttdom]
eqvbT [lemma, in graphs.pttdom]
eqvb_neq [lemma, in graphs.pttdom]
eqvb_par1 [lemma, in graphs.pttdom]
eqvb_transL [lemma, in graphs.structures]
eqvb_transR [lemma, in graphs.structures]
eqvb_trans [lemma, in graphs.structures]
eqvxx [lemma, in graphs.structures]
eqv_test_equiv [lemma, in graphs.pttdom]
eqv_test [definition, in graphs.pttdom]
eqv_update [lemma, in graphs.finmap_plus]
eqv_big [lemma, in graphs.structures]
eqv_bigl [lemma, in graphs.structures]
eqv_bigr [lemma, in graphs.structures]
eqv_big_bij [lemma, in graphs.structures]
eqv_map [lemma, in graphs.structures]
eqv_morphim [instance, in graphs.structures]
eqv_sym [instance, in graphs.structures]
eqv_ [definition, in graphs.structures]
eqv_clot_LR [lemma, in graphs.equiv]
eqv_clot_injR [lemma, in graphs.equiv]
eqv_clot_injL [lemma, in graphs.equiv]
eqv_clot1E [lemma, in graphs.equiv]
eqv_clot_cat [lemma, in graphs.equiv]
eqv_clot_map_eq [lemma, in graphs.equiv]
eqv_clot_mapF [lemma, in graphs.equiv]
eqv_clot_map [lemma, in graphs.equiv]
eqv_inj.f_inj [variable, in graphs.equiv]
eqv_inj.eq2E [variable, in graphs.equiv]
eqv_inj.eq_e [variable, in graphs.equiv]
eqv_inj.f [variable, in graphs.equiv]
eqv_inj.e2 [variable, in graphs.equiv]
eqv_inj.e1 [variable, in graphs.equiv]
eqv_inj.T2 [variable, in graphs.equiv]
eqv_inj.T1 [variable, in graphs.equiv]
eqv_inj [section, in graphs.equiv]
eqv_clot_nothing' [lemma, in graphs.equiv]
eqv_clot_nothing [lemma, in graphs.equiv]
eqv_clot_eq [lemma, in graphs.equiv]
eqv_clot_subrel [lemma, in graphs.equiv]
eqv_clot_tl [lemma, in graphs.equiv]
eqv_clot_hd' [lemma, in graphs.equiv]
eqv_clot_hd [lemma, in graphs.equiv]
eqv_clot_trans [lemma, in graphs.equiv]
eqv_clot_iso [lemma, in graphs.equiv]
eqv_clot_map' [lemma, in graphs.equiv]
eqv_clot_subset [lemma, in graphs.equiv]
eqv_clot_pair [lemma, in graphs.equiv]
eqv_clotE [lemma, in graphs.equiv]
eqv_clot [definition, in graphs.equiv]
eqv_clot_union_rel [lemma, in graphs.mgraph]
eqv_clot_map_lr [lemma, in graphs.mgraph]
eqv' [definition, in graphs.pttdom]
eqv' [projection, in graphs.structures]
eqv'_sym [lemma, in graphs.pttdom]
Eqv'_sym [projection, in graphs.structures]
eqv01 [lemma, in graphs.pttdom]
eqv01 [projection, in graphs.structures]
eqv10 [lemma, in graphs.structures]
eqv11 [lemma, in graphs.pttdom]
eqv11 [projection, in graphs.structures]
eq_connected [lemma, in graphs.sgraph]
eq_diso [lemma, in graphs.sgraph]
eq_unit [lemma, in graphs.structures]
eq_setoid [definition, in graphs.structures]
eq_set1P [lemma, in graphs.preliminaries]
eq_quot_finMixin [lemma, in graphs.finite_quotient]
eq_equiv_class [lemma, in graphs.equiv]
eq_equiv [lemma, in graphs.equiv]
eq_eqv [lemma, in graphs.mgraph]
ereprK [abbreviation, in graphs.finite_quotient]
eseparates [definition, in graphs.mgraph]
eval [definition, in graphs.pttdom]
eval [definition, in graphs.ptt]
eval_TW2 [lemma, in graphs.mgraph2_tw2]
excluded [library]
excluded_minor_TW2 [lemma, in graphs.excluded]
existsb_case [lemma, in graphs.preliminaries]
existsb_eq [lemma, in graphs.preliminaries]
existsPn [lemma, in graphs.preliminaries]
exists_inPn [lemma, in graphs.preliminaries]
ExtractionDef [section, in graphs.extraction_def]
ExtractionDef.SplitCP [section, in graphs.extraction_def]
ExtractionDef.SplitCP.CK4F_G [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.G [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.Hio [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.Hz [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.Hz' [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.z [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.Zi [variable, in graphs.extraction_def]
ExtractionDef.SplitCP.Zo [variable, in graphs.extraction_def]
ExtractionDef.sym [variable, in graphs.extraction_def]
ExtractionIso [section, in graphs.extraction_iso]
ExtractionIso.sym [variable, in graphs.extraction_iso]
ExtractionTop [section, in graphs.extraction_top]
ExtractionTop.sym [variable, in graphs.extraction_top]
extraction_iso [library]
extraction_top [library]
extraction_def [library]
ex_smallest [lemma, in graphs.preliminaries]
ex2_iff_morphism [instance, in graphs.preliminaries]
F
FinEncodingModuloRel [section, in graphs.finite_quotient]FinEncodingModuloRel.C [variable, in graphs.finite_quotient]
FinEncodingModuloRel.CD [variable, in graphs.finite_quotient]
FinEncodingModuloRel.D [variable, in graphs.finite_quotient]
FinEncodingModuloRel.DC [variable, in graphs.finite_quotient]
FinEncodingModuloRel.eD [variable, in graphs.finite_quotient]
FinEncodingModuloRel.encD [variable, in graphs.finite_quotient]
finite_quotient [library]
finmap_plus [library]
Fix [definition, in graphs.bounded]
Fix_eq [lemma, in graphs.bounded]
flat_labels [definition, in graphs.structures]
flesh_out [lemma, in graphs.skeleton]
flesh_out_graph [definition, in graphs.skeleton]
Foldr1 [section, in graphs.preliminaries]
foldr1 [definition, in graphs.preliminaries]
foldr1_set_default [lemma, in graphs.preliminaries]
Foldr1.F [variable, in graphs.preliminaries]
Foldr1.I [variable, in graphs.preliminaries]
Foldr1.op [variable, in graphs.preliminaries]
Foldr1.R [variable, in graphs.preliminaries]
foo [definition, in graphs.bounded]
foo_eq [lemma, in graphs.bounded]
foo_rec [definition, in graphs.bounded]
ForallE [lemma, in graphs.equiv]
forallPn [lemma, in graphs.preliminaries]
forall_inPn [lemma, in graphs.preliminaries]
forest [record, in graphs.sgraph]
Forest [constructor, in graphs.sgraph]
forestI [lemma, in graphs.sgraph]
forestP [lemma, in graphs.sgraph]
Forests [section, in graphs.sgraph]
Forests.G [variable, in graphs.sgraph]
forestT_unique [lemma, in graphs.sgraph]
forest_is_forest [projection, in graphs.sgraph]
forest_TW1 [lemma, in graphs.treewidth]
forest_vseparator [lemma, in graphs.treewidth]
forest3 [lemma, in graphs.sgraph]
fresh_bijE' [lemma, in graphs.finmap_plus]
fresh_bij' [lemma, in graphs.finmap_plus]
fresh_bijE [lemma, in graphs.finmap_plus]
fresh_bij [lemma, in graphs.finmap_plus]
Fresh2Bij [section, in graphs.finmap_plus]
Fresh2Bij.A [variable, in graphs.finmap_plus]
Fresh2Bij.B [variable, in graphs.finmap_plus]
Fresh2Bij.f [variable, in graphs.finmap_plus]
Fresh2Bij.Hx [variable, in graphs.finmap_plus]
Fresh2Bij.Hy [variable, in graphs.finmap_plus]
Fresh2Bij.T [variable, in graphs.finmap_plus]
Fresh2Bij.x [variable, in graphs.finmap_plus]
Fresh2Bij.y [variable, in graphs.finmap_plus]
fresh2_bij [definition, in graphs.finmap_plus]
fsetDDD [lemma, in graphs.finmap_plus]
fsetDEl [lemma, in graphs.finmap_plus]
fsetDl [lemma, in graphs.finmap_plus]
fsetD_bijE [lemma, in graphs.finmap_plus]
fsetD_bij [definition, in graphs.finmap_plus]
fsetD_bij_can_bwd [lemma, in graphs.finmap_plus]
fsetD_bij_can_fwd [lemma, in graphs.finmap_plus]
fsetD_bij_bwd [definition, in graphs.finmap_plus]
fsetD_bij_fwd [definition, in graphs.finmap_plus]
fsetD_bij_bwd_proof [lemma, in graphs.finmap_plus]
fsetD_bij_fwd_proof [lemma, in graphs.finmap_plus]
fsetD_bij.E [variable, in graphs.finmap_plus]
fsetD_bij.f [variable, in graphs.finmap_plus]
fsetD_bij.C' [variable, in graphs.finmap_plus]
fsetD_bij.C [variable, in graphs.finmap_plus]
fsetD_bij.B [variable, in graphs.finmap_plus]
fsetD_bij.A [variable, in graphs.finmap_plus]
fsetD_bij.T [variable, in graphs.finmap_plus]
fsetD_bij [section, in graphs.finmap_plus]
fsetUDU [lemma, in graphs.finmap_plus]
FsetU1Fun [section, in graphs.finmap_plus]
FsetU1Fun.A [variable, in graphs.finmap_plus]
FsetU1Fun.B [variable, in graphs.finmap_plus]
FsetU1Fun.f [variable, in graphs.finmap_plus]
FsetU1Fun.T [variable, in graphs.finmap_plus]
FsetU1Fun.x [variable, in graphs.finmap_plus]
FsetU1Fun.y [variable, in graphs.finmap_plus]
fsetU1_fun_can [lemma, in graphs.finmap_plus]
fsetU1_fun [definition, in graphs.finmap_plus]
fset01 [lemma, in graphs.finmap_plus]
fset1D [lemma, in graphs.finmap_plus]
fset1UE [lemma, in graphs.finmap_plus]
fset1U0 [lemma, in graphs.finmap_plus]
fset2_maxn_neq [lemma, in graphs.finmap_plus]
fset2_cases [lemma, in graphs.finmap_plus]
fset2_inv [lemma, in graphs.finmap_plus]
fst [definition, in graphs.digraph]
fst_inj [lemma, in graphs.connectivity]
fst_lst_eq [lemma, in graphs.connectivity]
fst_idp [lemma, in graphs.connectivity]
fst_mem [lemma, in graphs.digraph]
fsvalK [lemma, in graphs.finmap_plus]
fsval_eqF [lemma, in graphs.finmap_plus]
fun_decompose [lemma, in graphs.preliminaries]
F_rec_narrow [lemma, in graphs.bounded]
F_rec [definition, in graphs.bounded]
G
get_edge [lemma, in graphs.extraction_def]graph [abbreviation, in graphs.mgraph2_tw2]
graph [abbreviation, in graphs.extraction_def]
graph [abbreviation, in graphs.extraction_top]
graph [abbreviation, in graphs.skeleton]
graph [abbreviation, in graphs.skeleton]
graph [abbreviation, in graphs.extraction_iso]
graph [abbreviation, in graphs.mgraph]
graph [record, in graphs.mgraph]
Graph [constructor, in graphs.mgraph]
graph [abbreviation, in graphs.mgraph2]
graph_of_TW2 [lemma, in graphs.mgraph2_tw2]
graph_of_term [definition, in graphs.extraction_def]
graph_minor_TW2 [lemma, in graphs.extraction_top]
graph_of [projection, in graphs.mgraph2]
graph2 [abbreviation, in graphs.mgraph2_tw2]
graph2 [abbreviation, in graphs.extraction_def]
graph2 [abbreviation, in graphs.extraction_top]
graph2 [abbreviation, in graphs.skeleton]
graph2 [abbreviation, in graphs.extraction_iso]
graph2 [record, in graphs.mgraph2]
Graph2 [constructor, in graphs.mgraph2]
G1 [abbreviation, in graphs.mgraph]
G12 [abbreviation, in graphs.mgraph]
G2 [abbreviation, in graphs.mgraph]
g2_pttdom [definition, in graphs.mgraph2]
g2_ptt [definition, in graphs.mgraph2]
g2_A12 [lemma, in graphs.mgraph2]
g2_A12' [lemma, in graphs.mgraph2]
g2_A11 [lemma, in graphs.mgraph2]
g2_A10 [lemma, in graphs.mgraph2]
g2_var [definition, in graphs.mgraph2]
g2_top [definition, in graphs.mgraph2]
g2_one [definition, in graphs.mgraph2]
g2_dom [definition, in graphs.mgraph2]
g2_cnv [definition, in graphs.mgraph2]
g2_dot [definition, in graphs.mgraph2]
g2_par [definition, in graphs.mgraph2]
H
h [section, in graphs.mgraph2]Hall [lemma, in graphs.connectivity]
has_edge [lemma, in graphs.skeleton]
helly [library]
helly3_lifting [lemma, in graphs.helly]
Hom [constructor, in graphs.mgraph]
hom_eqL [lemma, in graphs.mgraph2_tw2]
hom_s [definition, in graphs.sgraph]
hom_skel [lemma, in graphs.skeleton]
hom_merge_union_K [lemma, in graphs.mgraph]
hom_union_merge_l [lemma, in graphs.mgraph]
hom_merge_merge [lemma, in graphs.mgraph]
hom_sym [lemma, in graphs.mgraph]
hom_comp [lemma, in graphs.mgraph]
hom_id [lemma, in graphs.mgraph]
hom2_sskel [lemma, in graphs.skeleton]
h_merge_union_Ke [definition, in graphs.mgraph]
h_merge_union_Ke1 [definition, in graphs.mgraph]
h_merge_union_K [definition, in graphs.mgraph]
h_union_merge_l [definition, in graphs.mgraph]
h_mergeE [lemma, in graphs.mgraph]
h_merge [definition, in graphs.mgraph]
h' [definition, in graphs.mgraph]
h.fe [variable, in graphs.mgraph2]
h.fv [variable, in graphs.mgraph2]
h.Hfe [variable, in graphs.mgraph2]
h.Hfv [variable, in graphs.mgraph2]
h.Hfvmon0 [variable, in graphs.mgraph2]
h.Hfvmon2 [variable, in graphs.mgraph2]
h.X [variable, in graphs.mgraph2]
h.Y [variable, in graphs.mgraph2]
I
i [abbreviation, in graphs.structures]idp [definition, in graphs.digraph]
idx [definition, in graphs.sgraph]
idxR [lemma, in graphs.sgraph]
idx_swap [lemma, in graphs.sgraph]
idx_swap_aux [lemma, in graphs.sgraph]
idx_srev [lemma, in graphs.sgraph]
idx_nLR [lemma, in graphs.sgraph]
idx_inj [lemma, in graphs.sgraph]
idx_catR [lemma, in graphs.sgraph]
idx_catL [lemma, in graphs.sgraph]
idx_end [lemma, in graphs.sgraph]
idx_start [lemma, in graphs.sgraph]
idx_mem [lemma, in graphs.sgraph]
id_surj [lemma, in graphs.preliminaries]
id_bij [lemma, in graphs.preliminaries]
iend [definition, in graphs.cp_minor]
igraph [definition, in graphs.cp_minor]
igraph [definition, in graphs.skeleton]
igraph_K4F_add_node [lemma, in graphs.cp_minor]
igraph_K4F [lemma, in graphs.cp_minor]
igraph_proof [lemma, in graphs.skeleton]
imfsetU [lemma, in graphs.finmap_plus]
imfset_bij_bwdE [lemma, in graphs.finmap_plus]
imfset_bij [definition, in graphs.finmap_plus]
imfset_bij_bwd [definition, in graphs.finmap_plus]
imfset_bij_fwd [definition, in graphs.finmap_plus]
imfset_inv [lemma, in graphs.finmap_plus]
imfset_comp [lemma, in graphs.finmap_plus]
imfset_sep [lemma, in graphs.finmap_plus]
imfset0 [lemma, in graphs.finmap_plus]
imfset1 [lemma, in graphs.finmap_plus]
imfset1U [lemma, in graphs.finmap_plus]
imset_valT [lemma, in graphs.preliminaries]
imset_pre_val [lemma, in graphs.preliminaries]
incident [definition, in graphs.mgraph]
incident_iso [lemma, in graphs.mgraph]
inD [lemma, in graphs.set_tac]
independent [definition, in graphs.digraph]
independent_walks [lemma, in graphs.connectivity]
independent_nodes [lemma, in graphs.digraph]
independent_sym [lemma, in graphs.digraph]
index_rev [lemma, in graphs.sgraph]
index_rcons [lemma, in graphs.sgraph]
induced [definition, in graphs.sgraph]
induced [definition, in graphs.digraph]
induced [definition, in graphs.mgraph]
InducedSubgraph [section, in graphs.sgraph]
InducedSubgraph [section, in graphs.digraph]
InducedSubgraph.G [variable, in graphs.sgraph]
InducedSubgraph.G [variable, in graphs.digraph]
InducedSubgraph.S [variable, in graphs.sgraph]
InducedSubgraph.S [variable, in graphs.digraph]
induced_K4_free [lemma, in graphs.extraction_def]
induced_forest [lemma, in graphs.sgraph]
induced_path [lemma, in graphs.sgraph]
induced_sub [lemma, in graphs.sgraph]
induced_irrefl [lemma, in graphs.sgraph]
induced_sym [lemma, in graphs.sgraph]
induced_rel [definition, in graphs.sgraph]
induced_type [definition, in graphs.sgraph]
induced_path [lemma, in graphs.digraph]
induced_rel [definition, in graphs.digraph]
induced_type [definition, in graphs.digraph]
induced_sub [lemma, in graphs.mgraph]
induced_proof [definition, in graphs.mgraph]
induced_minor [lemma, in graphs.minor]
induced2 [definition, in graphs.extraction_def]
induced2 [abbreviation, in graphs.extraction_top]
induced2_induced [lemma, in graphs.extraction_def]
induced2_compN_small [lemma, in graphs.extraction_top]
inD_debug [lemma, in graphs.set_tac]
inE [definition, in graphs.sgraph]
inE [definition, in graphs.digraph]
infer_testE [lemma, in graphs.pttdom]
infer_test [definition, in graphs.pttdom]
inj_imset [lemma, in graphs.preliminaries]
inj_card_onto_pred [lemma, in graphs.preliminaries]
inj_omap [lemma, in graphs.preliminaries]
inj_card_leq [lemma, in graphs.preliminaries]
inl_codom_inr [lemma, in graphs.preliminaries]
inl_inj [lemma, in graphs.preliminaries]
inl_eqE [lemma, in graphs.preliminaries]
input [projection, in graphs.mgraph2]
inr_codom_inl [lemma, in graphs.preliminaries]
inr_inj [lemma, in graphs.preliminaries]
inr_eqE [lemma, in graphs.preliminaries]
interior [definition, in graphs.digraph]
Interior [section, in graphs.digraph]
interiorN [lemma, in graphs.digraph]
interiorW [lemma, in graphs.digraph]
interior_rev [lemma, in graphs.sgraph]
interior_idp [lemma, in graphs.sgraph]
interior_eq_nodes [lemma, in graphs.digraph]
interior_edgep [lemma, in graphs.digraph]
Interior.G [variable, in graphs.digraph]
Interior.x [variable, in graphs.digraph]
Interior.y [variable, in graphs.digraph]
interior0E [lemma, in graphs.digraph]
interval [definition, in graphs.checkpoint]
intervalI_cp [lemma, in graphs.checkpoint]
intervalL [lemma, in graphs.checkpoint]
intervalR [lemma, in graphs.checkpoint]
interval_interval_cap [lemma, in graphs.checkpoint]
interval_edge_cp [lemma, in graphs.checkpoint]
interval_cp_cover [lemma, in graphs.checkpoint]
interval_bag_disj [lemma, in graphs.checkpoint]
interval_sym [lemma, in graphs.checkpoint]
interval_cp_edge_cover [lemma, in graphs.skeleton]
interval_bag_edge_cover [lemma, in graphs.skeleton]
interval_edges_disj_cp [lemma, in graphs.skeleton]
interval_bag_edges_disj [lemma, in graphs.skeleton]
interval_edges_sym [lemma, in graphs.skeleton]
interval_edges [definition, in graphs.skeleton]
in_component_of [lemma, in graphs.sgraph]
in_eqv_update [lemma, in graphs.finmap_plus]
in_fsep [lemma, in graphs.finmap_plus]
in_imfsetT [lemma, in graphs.finmap_plus]
in_pathS [definition, in graphs.digraph]
in_ipath [definition, in graphs.digraph]
in_tail [lemma, in graphs.digraph]
in_nodes [definition, in graphs.digraph]
IO [abbreviation, in graphs.mgraph2]
IPath [record, in graphs.digraph]
IPath_finMixin [definition, in graphs.digraph]
IPath_countMixin [definition, in graphs.digraph]
IPath_choiceMixin [definition, in graphs.digraph]
IPath_eqMixin [definition, in graphs.digraph]
irred [definition, in graphs.digraph]
irredE [lemma, in graphs.digraph]
irredxx [lemma, in graphs.digraph]
irred_in_sinterval [lemma, in graphs.cp_minor]
irred_edge [lemma, in graphs.sgraph]
irred_rev [lemma, in graphs.sgraph]
irred_eq_nodes [lemma, in graphs.digraph]
irred_of [definition, in graphs.digraph]
irred_upath [lemma, in graphs.digraph]
irred_is_edge [lemma, in graphs.digraph]
irred_catE [lemma, in graphs.digraph]
irred_catI [lemma, in graphs.digraph]
irred_cat [lemma, in graphs.digraph]
irred_catD [lemma, in graphs.digraph]
irred_ind [lemma, in graphs.digraph]
irred_edgeR [lemma, in graphs.digraph]
irred_edgeL [lemma, in graphs.digraph]
irred_edge [lemma, in graphs.digraph]
irred_idp [lemma, in graphs.digraph]
irreflexive_restrict [lemma, in graphs.sgraph]
iso [record, in graphs.mgraph]
Iso [constructor, in graphs.mgraph]
iso_connected [lemma, in graphs.sgraph]
iso_subgraph [lemma, in graphs.sgraph]
iso_disconnected_io [lemma, in graphs.extraction_top]
iso_component [definition, in graphs.skeleton]
iso_pointxx [lemma, in graphs.skeleton]
iso_split_par2 [lemma, in graphs.extraction_iso]
iso_one [lemma, in graphs.extraction_iso]
iso_top [lemma, in graphs.extraction_iso]
iso_subgraph_forT [definition, in graphs.mgraph]
iso_Equivalence [instance, in graphs.mgraph]
iso_comp [definition, in graphs.mgraph]
iso_sym [definition, in graphs.mgraph]
iso_id [definition, in graphs.mgraph]
iso_hom [projection, in graphs.mgraph]
iso_d [projection, in graphs.mgraph]
iso_e [projection, in graphs.mgraph]
iso_v [projection, in graphs.mgraph]
iso_iso2' [lemma, in graphs.mgraph2]
iso_iso2 [lemma, in graphs.mgraph2]
iso_K4_free [lemma, in graphs.minor]
iso_strict_minor [lemma, in graphs.minor]
Iso' [definition, in graphs.mgraph]
iso2 [record, in graphs.mgraph2]
Iso2 [constructor, in graphs.mgraph2]
iso2prop [definition, in graphs.mgraph2]
iso2prop_Equivalence [instance, in graphs.mgraph2]
iso2_disconnected_component [lemma, in graphs.extraction_top]
iso2_GTG [lemma, in graphs.extraction_top]
iso2_TGT [lemma, in graphs.extraction_top]
iso2_subgraph_forT [lemma, in graphs.mgraph2]
iso2_Equivalence [instance, in graphs.mgraph2]
iso2_comp [definition, in graphs.mgraph2]
iso2_sym [definition, in graphs.mgraph2]
iso2_id [definition, in graphs.mgraph2]
iso2_output [projection, in graphs.mgraph2]
iso2_input [projection, in graphs.mgraph2]
iso2_iso [projection, in graphs.mgraph2]
ISplit [constructor, in graphs.digraph]
isplit [inductive, in graphs.digraph]
isplitP [lemma, in graphs.digraph]
istart [definition, in graphs.cp_minor]
is_test_alt [lemma, in graphs.pttdom]
is_test [definition, in graphs.pttdom]
is_forestPn [lemma, in graphs.sgraph]
is_forestP [lemma, in graphs.sgraph]
is_forestb [definition, in graphs.sgraph]
is_tree [definition, in graphs.sgraph]
is_forest [definition, in graphs.sgraph]
is_dhom [definition, in graphs.digraph]
is_hom [record, in graphs.mgraph]
ival [projection, in graphs.digraph]
ivalP [projection, in graphs.digraph]
J
JoinSG [section, in graphs.sgraph]JoinSG.G1 [variable, in graphs.sgraph]
JoinSG.G2 [variable, in graphs.sgraph]
JoinT [section, in graphs.treewidth]
JoinT.T1 [variable, in graphs.treewidth]
JoinT.T2 [variable, in graphs.treewidth]
join_disc [lemma, in graphs.sgraph]
join_rel_irrefl [lemma, in graphs.sgraph]
join_rel_sym [lemma, in graphs.sgraph]
join_rel [definition, in graphs.sgraph]
join_width [lemma, in graphs.treewidth]
join_decomp [lemma, in graphs.treewidth]
join_is_forest [lemma, in graphs.treewidth]
K
kernel [definition, in graphs.finite_quotient]kernelb [definition, in graphs.finite_quotient]
kernelP [lemma, in graphs.finite_quotient]
kernel_equivalence [lemma, in graphs.finite_quotient]
kernel_eqv_clot [lemma, in graphs.equiv]
Km_width [lemma, in graphs.treewidth]
Km_bag [lemma, in graphs.treewidth]
Kn_clique [lemma, in graphs.minor]
Konig [lemma, in graphs.connectivity]
K3_free_forest [lemma, in graphs.minor]
K4 [definition, in graphs.sgraph]
K4_free_add_edge_sep_size2 [lemma, in graphs.excluded]
K4_of_vseparators [lemma, in graphs.excluded]
K4_of_paths [lemma, in graphs.excluded]
K4_free [definition, in graphs.minor]
L
labels [record, in graphs.structures]Labels [constructor, in graphs.structures]
largest [definition, in graphs.preliminaries]
last_rev_belast [lemma, in graphs.sgraph]
last_belast_eq [lemma, in graphs.preliminaries]
last_take [lemma, in graphs.preliminaries]
le [projection, in graphs.structures]
Le [abbreviation, in graphs.mgraph]
Le [abbreviation, in graphs.mgraph2]
lens [definition, in graphs.extraction_def]
lens_components [lemma, in graphs.extraction_def]
lens_sinterval [lemma, in graphs.extraction_def]
lens_io_set [lemma, in graphs.extraction_def]
leq_subn [lemma, in graphs.preliminaries]
lift_Path [lemma, in graphs.sgraph]
lift_Path_on [lemma, in graphs.sgraph]
lift_equiv [lemma, in graphs.preliminaries]
lift_path [lemma, in graphs.preliminaries]
lift_upath [lemma, in graphs.digraph]
lift_upath_on [lemma, in graphs.digraph]
lift_pathp [lemma, in graphs.digraph]
lift_pathp_on [lemma, in graphs.digraph]
line_of_walk [lemma, in graphs.mgraph]
line_graph [definition, in graphs.mgraph]
link [definition, in graphs.treewidth]
Link [section, in graphs.treewidth]
link_rel_sep2 [lemma, in graphs.cp_minor]
link_rel [abbreviation, in graphs.extraction_def]
link_is_forest [lemma, in graphs.treewidth]
link_has_None [lemma, in graphs.treewidth]
link_unique_None [lemma, in graphs.treewidth]
link_bypass [lemma, in graphs.treewidth]
link_unique_lift [lemma, in graphs.treewidth]
link_path_cp [lemma, in graphs.checkpoint]
link_seq_cp [lemma, in graphs.checkpoint]
link_avoid [lemma, in graphs.checkpoint]
link_graph [definition, in graphs.checkpoint]
link_irrefl [lemma, in graphs.checkpoint]
link_sym [lemma, in graphs.checkpoint]
link_rel [definition, in graphs.checkpoint]
Link.T [variable, in graphs.treewidth]
Link.U [variable, in graphs.treewidth]
Link.U_disc [variable, in graphs.treewidth]
lst [definition, in graphs.digraph]
lst_inj [lemma, in graphs.connectivity]
lst_idp [lemma, in graphs.connectivity]
lst_mem [lemma, in graphs.digraph]
ltn_subn [lemma, in graphs.helly]
lv [projection, in graphs.structures]
Lv [abbreviation, in graphs.mgraph]
Lv [abbreviation, in graphs.mgraph2]
lv_monoid [projection, in graphs.structures]
M
map_equivE [lemma, in graphs.finite_quotient]map_equiv_class [lemma, in graphs.finite_quotient]
map_equiv_rel [definition, in graphs.finite_quotient]
map_equiv.e [variable, in graphs.finite_quotient]
map_equiv.h [variable, in graphs.finite_quotient]
map_equiv.T [variable, in graphs.finite_quotient]
map_equiv.S [variable, in graphs.finite_quotient]
map_equiv [section, in graphs.finite_quotient]
map_pairs [definition, in graphs.equiv]
map_pairs_id [lemma, in graphs.mgraph]
map_map_pairs [lemma, in graphs.mgraph]
map_of_total [lemma, in graphs.minor]
matching [definition, in graphs.connectivity]
matching_cover_map [lemma, in graphs.connectivity]
matching_of_dimatching [lemma, in graphs.connectivity]
matching_of [definition, in graphs.connectivity]
Max [section, in graphs.bounded]
MaxnL [constructor, in graphs.preliminaries]
maxnP [lemma, in graphs.preliminaries]
MaxnR [constructor, in graphs.preliminaries]
maxn_fsetD [lemma, in graphs.finmap_plus]
maxn_fset2 [lemma, in graphs.finmap_plus]
maxn_eq [lemma, in graphs.preliminaries]
maxn_cases [inductive, in graphs.preliminaries]
max_mono [lemma, in graphs.preliminaries]
Max.split [variable, in graphs.bounded]
Max.split_lt [variable, in graphs.bounded]
measure [abbreviation, in graphs.extraction_def]
measure_lens_rest [lemma, in graphs.extraction_def]
measure_remove_edges [lemma, in graphs.extraction_def]
measure_split_cpM [lemma, in graphs.extraction_def]
measure_split_cpR [lemma, in graphs.extraction_def]
measure_split_cpL [lemma, in graphs.extraction_def]
measure_lens [lemma, in graphs.extraction_def]
measure_redirect [lemma, in graphs.extraction_def]
measure_remove_component [lemma, in graphs.extraction_def]
measure_igraph [lemma, in graphs.extraction_def]
measure_node [lemma, in graphs.extraction_def]
measure_subgraph [lemma, in graphs.extraction_def]
measure_io [lemma, in graphs.extraction_def]
measure_card [lemma, in graphs.extraction_def]
memKset [lemma, in graphs.preliminaries]
mem_component [lemma, in graphs.sgraph]
mem_prev [lemma, in graphs.sgraph]
mem_maxn [lemma, in graphs.finmap_plus]
mem_cpl [lemma, in graphs.checkpoint]
mem_cover [lemma, in graphs.preliminaries]
mem_preim [lemma, in graphs.preliminaries]
mem_catD [lemma, in graphs.preliminaries]
mem_tail [lemma, in graphs.preliminaries]
mem_del_edge_liftS [lemma, in graphs.digraph]
mem_eq_nodes [lemma, in graphs.digraph]
mem_pcat_edgeR [lemma, in graphs.digraph]
mem_pcat_edgeL [lemma, in graphs.digraph]
mem_edgep [lemma, in graphs.digraph]
mem_idp [lemma, in graphs.digraph]
mem_pcat [lemma, in graphs.digraph]
mem_pcatT [lemma, in graphs.digraph]
mem_path [lemma, in graphs.digraph]
mem_bigcup [lemma, in graphs.minor]
Menger [lemma, in graphs.connectivity]
merge [definition, in graphs.mgraph]
MergeSubgraph [section, in graphs.mgraph]
MergeSubgraph.A [variable, in graphs.mgraph]
MergeSubgraph.con1 [variable, in graphs.mgraph]
MergeSubgraph.con2 [variable, in graphs.mgraph]
MergeSubgraph.disE [variable, in graphs.mgraph]
MergeSubgraph.eqvI [variable, in graphs.mgraph]
MergeSubgraph.E1 [variable, in graphs.mgraph]
MergeSubgraph.E2 [variable, in graphs.mgraph]
MergeSubgraph.G [variable, in graphs.mgraph]
MergeSubgraph.h [variable, in graphs.mgraph]
MergeSubgraph.V1 [variable, in graphs.mgraph]
MergeSubgraph.V2 [variable, in graphs.mgraph]
merge_unionE [lemma, in graphs.finite_quotient]
merge_union [definition, in graphs.finite_quotient]
merge_union_bwd_hom [lemma, in graphs.finite_quotient]
merge_union_fwd_hom [lemma, in graphs.finite_quotient]
merge_union_can' [lemma, in graphs.finite_quotient]
merge_union_can [lemma, in graphs.finite_quotient]
merge_union_rel [definition, in graphs.finite_quotient]
merge_disjoint_union [definition, in graphs.finite_quotient]
merge_disjoint_union_can' [lemma, in graphs.finite_quotient]
merge_disjoint_union_can [lemma, in graphs.finite_quotient]
merge_union_bwdEr [definition, in graphs.finite_quotient]
merge_union_bwdEl [definition, in graphs.finite_quotient]
merge_union_bwdP [lemma, in graphs.finite_quotient]
merge_union_bwdR [constructor, in graphs.finite_quotient]
merge_union_bwdL [constructor, in graphs.finite_quotient]
merge_union_bwd_spec [inductive, in graphs.finite_quotient]
merge_union_bwd [definition, in graphs.finite_quotient]
merge_union_fwd [definition, in graphs.finite_quotient]
merge_subgraph_par [lemma, in graphs.extraction_iso]
merge_subgraph_dot [lemma, in graphs.extraction_iso]
merge_subgraph_isoE [lemma, in graphs.mgraph]
merge_subgraph_iso [definition, in graphs.mgraph]
merge_subgraph_hom [lemma, in graphs.mgraph]
merge_subgraph_e [definition, in graphs.mgraph]
merge_subgraph_v [definition, in graphs.mgraph]
merge_seq [abbreviation, in graphs.mgraph]
merge_union_KE [lemma, in graphs.mgraph]
merge_union_K [definition, in graphs.mgraph]
merge_add_vlabelE [lemma, in graphs.mgraph]
merge_add_vlabel [lemma, in graphs.mgraph]
merge_add_edgeE [lemma, in graphs.mgraph]
merge_add_edge [lemma, in graphs.mgraph]
merge_merge_seqE [lemma, in graphs.mgraph]
merge_merge_seq [definition, in graphs.mgraph]
merge_nothingE [lemma, in graphs.mgraph]
merge_nothing [definition, in graphs.mgraph]
merge_sameE [definition, in graphs.mgraph]
merge_same [definition, in graphs.mgraph]
merge_same'E [lemma, in graphs.mgraph]
merge_same' [definition, in graphs.mgraph]
merge_same'_hom [lemma, in graphs.mgraph]
merge_isoE [lemma, in graphs.mgraph]
merge_iso [definition, in graphs.mgraph]
merge_hom [lemma, in graphs.mgraph]
merge_mergeE [lemma, in graphs.mgraph]
merge_merge [lemma, in graphs.mgraph]
merge_nothing'E [lemma, in graphs.mgraph]
merge_nothing' [lemma, in graphs.mgraph]
merge_surjE [lemma, in graphs.mgraph]
merge_surj [lemma, in graphs.mgraph]
merge_seq [abbreviation, in graphs.mgraph]
merge_union_K_l [lemma, in graphs.mgraph2]
merge_merge [lemma, in graphs.mgraph2]
merge_nothing [lemma, in graphs.mgraph2]
merge_same' [lemma, in graphs.mgraph2]
merge_same [lemma, in graphs.mgraph2]
merge_iso2 [lemma, in graphs.mgraph2]
merge2 [definition, in graphs.mgraph2]
merge2_seq [abbreviation, in graphs.mgraph2]
merge2_add_vlabel [lemma, in graphs.mgraph2]
merge2_add_edge [lemma, in graphs.mgraph2]
merge2_merge [lemma, in graphs.mgraph2]
merge2_nothing [lemma, in graphs.mgraph2]
merge2_same' [lemma, in graphs.mgraph2]
merge2_same [lemma, in graphs.mgraph2]
merge2_surj [lemma, in graphs.mgraph2]
merge2_iso2 [lemma, in graphs.mgraph2]
merge2_seq [abbreviation, in graphs.mgraph2]
mgraph [library]
mgraph_rel [definition, in graphs.mgraph]
mgraph2 [library]
mgraph2_tw2 [library]
minimal_separation [lemma, in graphs.connectivity]
minor [definition, in graphs.minor]
minor [library]
minorRE [lemma, in graphs.minor]
minor_exclusion_2p [lemma, in graphs.extraction_top]
minor_rmapI [lemma, in graphs.minor]
minor_with [lemma, in graphs.minor]
minor_induced_add_node [lemma, in graphs.minor]
minor_K4_free [lemma, in graphs.minor]
minor_of_clique [lemma, in graphs.minor]
minor_trans [lemma, in graphs.minor]
minor_map_comp [lemma, in graphs.minor]
minor_rmap_comp [lemma, in graphs.minor]
minor_of_rmap [lemma, in graphs.minor]
minor_of_map [lemma, in graphs.minor]
minor_rmap_map [lemma, in graphs.minor]
minor_map_rmap [lemma, in graphs.minor]
minor_rmap [definition, in graphs.minor]
minor_map [definition, in graphs.minor]
min_vcover_matching [lemma, in graphs.connectivity]
min_max_cover [lemma, in graphs.connectivity]
monA [projection, in graphs.structures]
monC [projection, in graphs.structures]
monoidLaws [record, in graphs.structures]
MonoidLaws [constructor, in graphs.structures]
monU [projection, in graphs.structures]
monUl [lemma, in graphs.structures]
mon_eqv [projection, in graphs.structures]
mon0 [projection, in graphs.structures]
mon2 [projection, in graphs.structures]
N
N [definition, in graphs.connectivity]nat_size_ind [lemma, in graphs.preliminaries]
NB [abbreviation, in graphs.excluded]
NB [abbreviation, in graphs.excluded]
ncp [definition, in graphs.checkpoint]
ncpP [lemma, in graphs.checkpoint]
ncp_interval [lemma, in graphs.checkpoint]
ncp_bag [lemma, in graphs.checkpoint]
ncp_CP [lemma, in graphs.checkpoint]
ncp0 [lemma, in graphs.checkpoint]
neighbor [definition, in graphs.sgraph]
Neighbor [section, in graphs.sgraph]
neighborC [lemma, in graphs.sgraph]
neighborP [lemma, in graphs.sgraph]
neighborUl [lemma, in graphs.sgraph]
neighborUr [lemma, in graphs.sgraph]
neighborW [lemma, in graphs.sgraph]
neighbor_interiorL [lemma, in graphs.sgraph]
neighbor_split [lemma, in graphs.sgraph]
neighbor_add_edge [lemma, in graphs.sgraph]
neighbor_del_edge1 [lemma, in graphs.sgraph]
neighbor_del_edge2 [lemma, in graphs.sgraph]
neighbor_del_edgeR [lemma, in graphs.sgraph]
neighbor_add_edgeC [lemma, in graphs.sgraph]
neighbor_connected [lemma, in graphs.sgraph]
Neighbor.G [variable, in graphs.sgraph]
neighbours [definition, in graphs.cp_minor]
nodes [definition, in graphs.digraph]
nodesE [lemma, in graphs.digraph]
nodes_prev [lemma, in graphs.sgraph]
nodes_pcat [lemma, in graphs.digraph]
nodes_eqE [lemma, in graphs.digraph]
non_forerst_K3 [lemma, in graphs.minor]
Nopicks [constructor, in graphs.preliminaries]
notinD [lemma, in graphs.set_tac]
notinD_debug [lemma, in graphs.set_tac]
notin_tail [lemma, in graphs.preliminaries]
no_K4_smallest_vseparator [lemma, in graphs.excluded]
nt [definition, in graphs.pttdom]
nterm [inductive, in graphs.pttdom]
nt_correct [lemma, in graphs.pttdom]
nt_par [definition, in graphs.pttdom]
nt_dot [definition, in graphs.pttdom]
nt_dom [definition, in graphs.pttdom]
nt_cnv [definition, in graphs.pttdom]
nt_var [definition, in graphs.pttdom]
nt_one [definition, in graphs.pttdom]
nt_conn [constructor, in graphs.pttdom]
nt_test [constructor, in graphs.pttdom]
num_edges [definition, in graphs.digraph]
O
one [projection, in graphs.pttdom]one_test [lemma, in graphs.pttdom]
ops [projection, in graphs.pttdom]
ops [projection, in graphs.ptt]
ops_ [record, in graphs.pttdom]
option_void [definition, in graphs.bij]
option_sum_unit [lemma, in graphs.bij]
option_bij [definition, in graphs.bij]
option2x [definition, in graphs.bij]
option2_swap [definition, in graphs.bij]
orb_sum [lemma, in graphs.preliminaries]
ord_fresh [lemma, in graphs.preliminaries]
ord_size_enum [lemma, in graphs.preliminaries]
ord1 [definition, in graphs.preliminaries]
ord2 [definition, in graphs.preliminaries]
ord3 [definition, in graphs.preliminaries]
ord3P [lemma, in graphs.helly]
output [projection, in graphs.mgraph2]
P
Pack [section, in graphs.digraph]Packaged [section, in graphs.sgraph]
Packaged.G [variable, in graphs.sgraph]
Packaged.Prev [section, in graphs.sgraph]
Packaged.Prev.p [variable, in graphs.sgraph]
Packaged.Prev.q [variable, in graphs.sgraph]
Packaged.Prev.x [variable, in graphs.sgraph]
Packaged.Prev.y [variable, in graphs.sgraph]
Packaged.Prev.z [variable, in graphs.sgraph]
Pack.PathDef [section, in graphs.digraph]
Pack.PathDef.x [variable, in graphs.digraph]
Pack.PathDef.y [variable, in graphs.digraph]
Pack.T [variable, in graphs.digraph]
pairs [definition, in graphs.equiv]
par [projection, in graphs.pttdom]
parA [projection, in graphs.pttdom]
paratst [lemma, in graphs.pttdom]
parA_ [projection, in graphs.ptt]
parC [projection, in graphs.pttdom]
parC_ [projection, in graphs.ptt]
pardot [lemma, in graphs.pttdom]
partition_components [lemma, in graphs.sgraph]
partition_big [lemma, in graphs.structures]
partition0 [lemma, in graphs.sgraph]
partopx [lemma, in graphs.ptt]
partst [lemma, in graphs.pttdom]
parxtop [lemma, in graphs.ptt]
par_nontest [lemma, in graphs.pttdom]
par_tst_cnv [lemma, in graphs.pttdom]
par_test [lemma, in graphs.pttdom]
par_eqv [projection, in graphs.pttdom]
par_component [lemma, in graphs.extraction_top]
par_eqv_ [projection, in graphs.ptt]
par_iso2 [instance, in graphs.mgraph2]
par1tst [lemma, in graphs.pttdom]
par11 [projection, in graphs.pttdom]
par11_ [projection, in graphs.ptt]
par2A [lemma, in graphs.mgraph2]
par2C [lemma, in graphs.mgraph2]
par2dot [lemma, in graphs.mgraph2]
par2edgeunit [lemma, in graphs.mgraph2]
par2oneone [lemma, in graphs.mgraph2]
par2top [lemma, in graphs.mgraph2]
par2unitunit [lemma, in graphs.mgraph2]
Path [abbreviation, in graphs.treewidth]
Path [record, in graphs.digraph]
PathIndexing [section, in graphs.sgraph]
PathIndexing.G [variable, in graphs.sgraph]
PathIndexing.IDX [section, in graphs.sgraph]
PathIndexing.IDX.dis_pq [variable, in graphs.sgraph]
PathIndexing.IDX.irr_q [variable, in graphs.sgraph]
PathIndexing.IDX.irr_p [variable, in graphs.sgraph]
PathIndexing.IDX.irr_pq [variable, in graphs.sgraph]
PathIndexing.IDX.p [variable, in graphs.sgraph]
PathIndexing.IDX.q [variable, in graphs.sgraph]
PathIndexing.IDX.x [variable, in graphs.sgraph]
PathIndexing.IDX.y [variable, in graphs.sgraph]
PathIndexing.IDX.z [variable, in graphs.sgraph]
PathOps [section, in graphs.digraph]
PathOps.p [variable, in graphs.digraph]
PathOps.q [variable, in graphs.digraph]
PathOps.T [variable, in graphs.digraph]
PathOps.x [variable, in graphs.digraph]
PathOps.y [variable, in graphs.digraph]
PathOps.z [variable, in graphs.digraph]
pathp [definition, in graphs.digraph]
PathP [section, in graphs.digraph]
pathpP [lemma, in graphs.digraph]
pathpW [lemma, in graphs.digraph]
pathpxx [lemma, in graphs.digraph]
pathp_rev [lemma, in graphs.sgraph]
pathp_shorten [lemma, in graphs.digraph]
pathp_split [inductive, in graphs.digraph]
pathp_rcons [lemma, in graphs.digraph]
pathp_cons [lemma, in graphs.digraph]
pathp_nil [lemma, in graphs.digraph]
pathp_concat [lemma, in graphs.digraph]
pathp_cat [lemma, in graphs.digraph]
pathp_last [lemma, in graphs.digraph]
PathP.T [variable, in graphs.digraph]
PathRP [lemma, in graphs.sgraph]
PathS [definition, in graphs.digraph]
pathS [definition, in graphs.digraph]
PathS [section, in graphs.digraph]
pathS_eta [lemma, in graphs.digraph]
PathS.G [variable, in graphs.digraph]
PathTheory [section, in graphs.digraph]
PathTheory.Fixed [section, in graphs.digraph]
PathTheory.Fixed.p [variable, in graphs.digraph]
PathTheory.Fixed.q [variable, in graphs.digraph]
PathTheory.Fixed.x [variable, in graphs.digraph]
PathTheory.Fixed.y [variable, in graphs.digraph]
PathTheory.Fixed.z [variable, in graphs.digraph]
PathTheory.G [variable, in graphs.digraph]
path_neighborR [lemma, in graphs.sgraph]
path_neighborL [lemma, in graphs.sgraph]
path_in_connected [lemma, in graphs.sgraph]
Path_from_induced [lemma, in graphs.sgraph]
Path_to_induced [lemma, in graphs.sgraph]
path_to_induced [lemma, in graphs.sgraph]
path_srev [lemma, in graphs.sgraph]
path_return [lemma, in graphs.treewidth]
path_restrict [lemma, in graphs.preliminaries]
Path_from_induced [lemma, in graphs.digraph]
Path_to_induced [lemma, in graphs.digraph]
path_to_induced [lemma, in graphs.digraph]
path_of_ipath [definition, in graphs.digraph]
Path_connect [lemma, in graphs.digraph]
path_closed [lemma, in graphs.digraph]
Path_ind [lemma, in graphs.digraph]
path_begin [lemma, in graphs.digraph]
path_end [lemma, in graphs.digraph]
path_last [lemma, in graphs.digraph]
Path_countMixin [definition, in graphs.digraph]
Path_choiceMixin [definition, in graphs.digraph]
Path_eqMixin [definition, in graphs.digraph]
pblock_eqvE [lemma, in graphs.preliminaries]
pcat [definition, in graphs.digraph]
pcatA [lemma, in graphs.digraph]
pcatS [definition, in graphs.digraph]
pcatSE [lemma, in graphs.digraph]
pcat_subset [lemma, in graphs.digraph]
pcat_idR [lemma, in graphs.digraph]
pcat_idL [lemma, in graphs.digraph]
pcat_proof [definition, in graphs.digraph]
perm_index_enum [lemma, in graphs.bij]
perm_big [lemma, in graphs.structures]
pe_partition [definition, in graphs.preliminaries]
Picks [constructor, in graphs.preliminaries]
picksP [lemma, in graphs.preliminaries]
picks_spec [inductive, in graphs.preliminaries]
piK [lemma, in graphs.finite_quotient]
piK' [lemma, in graphs.finite_quotient]
pimset [definition, in graphs.preliminaries]
pimsetP [lemma, in graphs.preliminaries]
pimset_card [lemma, in graphs.preliminaries]
piP [lemma, in graphs.finite_quotient]
PiSpec [constructor, in graphs.finite_quotient]
pi_hom [lemma, in graphs.skeleton]
pi_surj [lemma, in graphs.finite_quotient]
pi_spec [inductive, in graphs.finite_quotient]
point [abbreviation, in graphs.mgraph2]
point [abbreviation, in graphs.mgraph2]
pos [abbreviation, in graphs.set_tac]
PPSplit [constructor, in graphs.digraph]
ppsplitP [lemma, in graphs.digraph]
predIpcatR [lemma, in graphs.excluded]
preim_omap_None [lemma, in graphs.preliminaries]
preim_omap_Some [lemma, in graphs.preliminaries]
preliminaries [library]
prev [definition, in graphs.sgraph]
prevK [lemma, in graphs.sgraph]
prev_edge [lemma, in graphs.sgraph]
prev_edge_proof [lemma, in graphs.sgraph]
prev_irred [lemma, in graphs.sgraph]
prev_cat [lemma, in graphs.sgraph]
prev_inj [lemma, in graphs.sgraph]
prev_proof [definition, in graphs.sgraph]
project_path [lemma, in graphs.preliminaries]
propers_ind [lemma, in graphs.preliminaries]
proper_separation_symmetry [lemma, in graphs.connectivity]
proper_vseparator [lemma, in graphs.connectivity]
proper_separation [definition, in graphs.connectivity]
proper_ind [lemma, in graphs.preliminaries]
PSplit [constructor, in graphs.digraph]
psplit [inductive, in graphs.digraph]
psplitP [lemma, in graphs.digraph]
ptt [record, in graphs.ptt]
ptt [library]
pttdom [record, in graphs.pttdom]
pttdom [library]
pval [projection, in graphs.digraph]
Q
quot [module, in graphs.finite_quotient]QUOT [module, in graphs.finite_quotient]
QuotBij [section, in graphs.finite_quotient]
QuotBij.e1 [variable, in graphs.finite_quotient]
QuotBij.e2 [variable, in graphs.finite_quotient]
QuotBij.h [variable, in graphs.finite_quotient]
QuotBij.h_inv_can [variable, in graphs.finite_quotient]
QuotBij.h_can [variable, in graphs.finite_quotient]
QuotBij.h_inv_homo [variable, in graphs.finite_quotient]
QuotBij.h_homo [variable, in graphs.finite_quotient]
QuotBij.h_inv [variable, in graphs.finite_quotient]
QuotBij.T1 [variable, in graphs.finite_quotient]
QuotBij.T2 [variable, in graphs.finite_quotient]
QuotFun [section, in graphs.finite_quotient]
QuotFun.e1 [variable, in graphs.finite_quotient]
QuotFun.e2 [variable, in graphs.finite_quotient]
QuotFun.h1 [variable, in graphs.finite_quotient]
QuotFun.T1 [variable, in graphs.finite_quotient]
QuotFun.T2 [variable, in graphs.finite_quotient]
quot_union_KE [lemma, in graphs.finite_quotient]
quot_union_K [definition, in graphs.finite_quotient]
quot_union_K.kh [variable, in graphs.finite_quotient]
quot_union_K.k [variable, in graphs.finite_quotient]
quot_union_K.e [variable, in graphs.finite_quotient]
quot_union_K.K [variable, in graphs.finite_quotient]
quot_union_K.S [variable, in graphs.finite_quotient]
quot_union_K [section, in graphs.finite_quotient]
quot_idE [lemma, in graphs.finite_quotient]
quot_id [definition, in graphs.finite_quotient]
quot_id.H [variable, in graphs.finite_quotient]
quot_id.e [variable, in graphs.finite_quotient]
quot_id.T [variable, in graphs.finite_quotient]
quot_id [section, in graphs.finite_quotient]
quot_quotE [lemma, in graphs.finite_quotient]
quot_quot [definition, in graphs.finite_quotient]
quot_quot.e' [variable, in graphs.finite_quotient]
quot_quot.e [variable, in graphs.finite_quotient]
quot_quot.T [variable, in graphs.finite_quotient]
quot_quot [section, in graphs.finite_quotient]
quot_bijE' [lemma, in graphs.finite_quotient]
quot_bijE [lemma, in graphs.finite_quotient]
quot_bij [definition, in graphs.finite_quotient]
quot_kernelE' [lemma, in graphs.finite_quotient]
quot_kernelE [lemma, in graphs.finite_quotient]
quot_kernel [definition, in graphs.finite_quotient]
quot_kernel_can' [lemma, in graphs.finite_quotient]
quot_kernel_can [lemma, in graphs.finite_quotient]
quot_kernel.Hf [variable, in graphs.finite_quotient]
quot_kernel.Hr [variable, in graphs.finite_quotient]
quot_kernel.f' [variable, in graphs.finite_quotient]
quot_kernel.f [variable, in graphs.finite_quotient]
quot_kernel.r [variable, in graphs.finite_quotient]
quot_kernel [section, in graphs.finite_quotient]
quot_sameE' [lemma, in graphs.finite_quotient]
quot_sameE [lemma, in graphs.finite_quotient]
quot_same [definition, in graphs.finite_quotient]
quot_fun_can [lemma, in graphs.finite_quotient]
quot_fun [definition, in graphs.finite_quotient]
quot.eqquotP [lemma, in graphs.finite_quotient]
QUOT.eqquotP [axiom, in graphs.finite_quotient]
quot.pi [definition, in graphs.finite_quotient]
QUOT.pi [axiom, in graphs.finite_quotient]
quot.quot [definition, in graphs.finite_quotient]
QUOT.quot [axiom, in graphs.finite_quotient]
quot.repr [definition, in graphs.finite_quotient]
QUOT.repr [axiom, in graphs.finite_quotient]
quot.reprK [lemma, in graphs.finite_quotient]
QUOT.reprK [axiom, in graphs.finite_quotient]
quot.s [section, in graphs.finite_quotient]
quot.s.e [variable, in graphs.finite_quotient]
quot.s.T [variable, in graphs.finite_quotient]
R
rcons_pathp [lemma, in graphs.digraph]rec_bag [lemma, in graphs.extraction_def]
redirect [definition, in graphs.extraction_def]
redirect_to [definition, in graphs.extraction_def]
redirect_output_proof [lemma, in graphs.extraction_def]
redirect_consistent [lemma, in graphs.extraction_def]
redirect_proof1 [lemma, in graphs.extraction_def]
reduce_shuffle [lemma, in graphs.pttdom]
reindex [lemma, in graphs.structures]
reindex_onto [lemma, in graphs.structures]
relabel [definition, in graphs.mgraph2]
relabel_edge [lemma, in graphs.mgraph2]
relabel_two [lemma, in graphs.mgraph2]
relabel_unit [lemma, in graphs.mgraph2]
relabel_add_edge [lemma, in graphs.mgraph2]
relabel_merge [lemma, in graphs.mgraph2]
relabel_union [lemma, in graphs.mgraph2]
relabel_iso [instance, in graphs.mgraph2]
relabel2 [definition, in graphs.mgraph2]
relabel2_var [lemma, in graphs.mgraph2]
relabel2_top [lemma, in graphs.mgraph2]
relabel2_one [lemma, in graphs.mgraph2]
relabel2_dom [lemma, in graphs.mgraph2]
relabel2_cnv [lemma, in graphs.mgraph2]
relabel2_par [lemma, in graphs.mgraph2]
relabel2_dot [lemma, in graphs.mgraph2]
relabel2_iso [instance, in graphs.mgraph2]
relType [record, in graphs.digraph]
RelType [constructor, in graphs.digraph]
relU_sym' [lemma, in graphs.preliminaries]
rel_of_pairs_mapE [lemma, in graphs.equiv]
rel_of_pairs_map_eq [lemma, in graphs.equiv]
rel_of_pairs_mono [lemma, in graphs.equiv]
rel_of_pairs [definition, in graphs.equiv]
rel_car [projection, in graphs.digraph]
rel0 [abbreviation, in graphs.preliminaries]
rel0_sym [lemma, in graphs.preliminaries]
rel0_irrefl [lemma, in graphs.preliminaries]
remove_component [lemma, in graphs.sgraph]
remove_edges_restrict [lemma, in graphs.skeleton]
remove_edges_cross [lemma, in graphs.skeleton]
remove_edges_connected [lemma, in graphs.skeleton]
remove_loops [lemma, in graphs.skeleton]
remove_edge_add [lemma, in graphs.skeleton]
remove_vertex [definition, in graphs.mgraph]
remove_edges_sub [lemma, in graphs.mgraph]
remove_edges [definition, in graphs.mgraph]
rename [definition, in graphs.sgraph]
rename_width [lemma, in graphs.treewidth]
rename_decomp [lemma, in graphs.treewidth]
rename_sdecomp [lemma, in graphs.minor]
restrict [definition, in graphs.preliminaries]
restrictE [lemma, in graphs.preliminaries]
restrict_upath [lemma, in graphs.sgraph]
restrict_path [lemma, in graphs.preliminaries]
restrict_mono [lemma, in graphs.preliminaries]
rev_upath [lemma, in graphs.sgraph]
rev_inj [lemma, in graphs.preliminaries]
rmap_disjE [lemma, in graphs.excluded]
rmap_add_edge_sym [lemma, in graphs.minor]
rwT [lemma, in graphs.pttdom]
S
s [section, in graphs.mgraph2_tw2]s [section, in graphs.mgraph]
s [section, in graphs.mgraph2]
same_component [lemma, in graphs.sgraph]
sbag_conn [projection, in graphs.treewidth]
sbag_edge [projection, in graphs.treewidth]
sbag_cover [projection, in graphs.treewidth]
sc [definition, in graphs.preliminaries]
sconnect_sym [lemma, in graphs.sgraph]
sc_eq [lemma, in graphs.preliminaries]
sc_sym [lemma, in graphs.preliminaries]
sdecomp [record, in graphs.treewidth]
SDecomp [constructor, in graphs.treewidth]
sdecomp_sskel [lemma, in graphs.mgraph2_tw2]
sdecomp_tree_subrel [lemma, in graphs.treewidth]
sdecomp_subrel [lemma, in graphs.treewidth]
sedge [projection, in graphs.sgraph]
sedge_equiv_in [lemma, in graphs.sgraph]
sedge_in_equiv [lemma, in graphs.sgraph]
sedge_equiv [lemma, in graphs.sgraph]
separates [definition, in graphs.connectivity]
separatesb [definition, in graphs.connectivity]
separatesI [lemma, in graphs.connectivity]
separatesNE [lemma, in graphs.connectivity]
separatesNeq [lemma, in graphs.connectivity]
separatesP [lemma, in graphs.connectivity]
separates0P [lemma, in graphs.connectivity]
separate_nonadjacent [lemma, in graphs.connectivity]
separation [definition, in graphs.connectivity]
separation_K4side [lemma, in graphs.excluded]
separation_connected_same_component [lemma, in graphs.connectivity]
separation_sym [lemma, in graphs.connectivity]
separation_separates [lemma, in graphs.connectivity]
separation_decomp [lemma, in graphs.treewidth]
separator [definition, in graphs.connectivity]
separatorb [definition, in graphs.connectivity]
SeparatorConnector [section, in graphs.connectivity]
SeparatorConnector.ConnectorTheory [section, in graphs.connectivity]
SeparatorConnector.ConnectorTheory.A [variable, in graphs.connectivity]
SeparatorConnector.ConnectorTheory.B [variable, in graphs.connectivity]
SeparatorConnector.ConnectorTheory.conn_p [variable, in graphs.connectivity]
SeparatorConnector.ConnectorTheory.n [variable, in graphs.connectivity]
SeparatorConnector.ConnectorTheory.p [variable, in graphs.connectivity]
SeparatorConnector.G [variable, in graphs.connectivity]
separatorI [lemma, in graphs.connectivity]
separatorP [lemma, in graphs.connectivity]
separatorPn [lemma, in graphs.connectivity]
separator_min [lemma, in graphs.connectivity]
separator_cap [lemma, in graphs.connectivity]
sepatates_cp [lemma, in graphs.cp_minor]
sep_inL [lemma, in graphs.connectivity]
sep_inR [lemma, in graphs.connectivity]
setBox [record, in graphs.set_tac]
SetBox [constructor, in graphs.set_tac]
setBoxed [projection, in graphs.set_tac]
setIPn [lemma, in graphs.set_tac]
setN01E [lemma, in graphs.preliminaries]
setoid [record, in graphs.structures]
Setoid [constructor, in graphs.structures]
setoid_of_ops [projection, in graphs.pttdom]
SetTac [section, in graphs.set_tac]
SetTac.A [variable, in graphs.set_tac]
SetTac.B [variable, in graphs.set_tac]
SetTac.C [variable, in graphs.set_tac]
SetTac.T [variable, in graphs.set_tac]
setT_bij [definition, in graphs.bij]
setT_bij_hom [lemma, in graphs.mgraph]
setUPn [lemma, in graphs.set_tac]
setU_dec [lemma, in graphs.finite_quotient]
setU1_neq [lemma, in graphs.preliminaries]
setU1_mem [lemma, in graphs.preliminaries]
set_pred0 [lemma, in graphs.cp_minor]
set_tac_subIl [lemma, in graphs.set_tac]
set_tac_subIr [lemma, in graphs.set_tac]
set_tac_subUl [lemma, in graphs.set_tac]
set_tac [library]
set1_inj [lemma, in graphs.preliminaries]
set10 [lemma, in graphs.preliminaries]
set2C [lemma, in graphs.preliminaries]
sgP [definition, in graphs.sgraph]
sgraph [record, in graphs.sgraph]
SGraph [constructor, in graphs.sgraph]
sgraph [library]
sgraph_of_forest [projection, in graphs.sgraph]
sg_edgeNeq [lemma, in graphs.sgraph]
sg_irrefl [definition, in graphs.sgraph]
sg_sym [definition, in graphs.sgraph]
sg_irrefl' [projection, in graphs.sgraph]
sg_sym' [projection, in graphs.sgraph]
sig [abbreviation, in graphs.finite_quotient]
sigraph [abbreviation, in graphs.extraction_def]
sig_sum_bij.NonDisjoint.eqvI [variable, in graphs.finite_quotient]
sig_sum_bij.NonDisjoint.e [variable, in graphs.finite_quotient]
sig_sum_bij.NonDisjoint [section, in graphs.finite_quotient]
sig_sum_bij.Disjoint.disUV [variable, in graphs.finite_quotient]
sig_sum_bij.Disjoint [section, in graphs.finite_quotient]
sig_sum_bij.V [variable, in graphs.finite_quotient]
sig_sum_bij.U [variable, in graphs.finite_quotient]
sig_sum_bij.T [variable, in graphs.finite_quotient]
sig_sum_bij [section, in graphs.finite_quotient]
SimplePaths [section, in graphs.sgraph]
SimplePaths.G [variable, in graphs.sgraph]
simple_check_point_wf [definition, in graphs.extraction_def]
simple_check_point_term [definition, in graphs.extraction_def]
sinterval [definition, in graphs.checkpoint]
sintervalP2 [lemma, in graphs.checkpoint]
sinterval_cp_cover [lemma, in graphs.checkpoint]
sinterval_bag_cover [lemma, in graphs.checkpoint]
sinterval_components [lemma, in graphs.checkpoint]
sinterval_connectedL [lemma, in graphs.checkpoint]
sinterval_connectL [lemma, in graphs.checkpoint]
sinterval_noedge_cp [lemma, in graphs.checkpoint]
sinterval_disj_cp [lemma, in graphs.checkpoint]
sinterval_outside [lemma, in graphs.checkpoint]
sinterval_exit [lemma, in graphs.checkpoint]
sinterval_sub [lemma, in graphs.checkpoint]
sinterval_bounds [lemma, in graphs.checkpoint]
sinterval_sym [lemma, in graphs.checkpoint]
size_ind [definition, in graphs.preliminaries]
sjoin [definition, in graphs.sgraph]
skeleton [definition, in graphs.skeleton]
Skeleton [section, in graphs.skeleton]
skeleton [library]
Skeleton.L [variable, in graphs.skeleton]
skelP [lemma, in graphs.skeleton]
skel_K4_free [lemma, in graphs.mgraph2_tw2]
skel_union_join [lemma, in graphs.mgraph2_tw2]
skel_sub [lemma, in graphs.skeleton]
skel_iso [instance, in graphs.skeleton]
sk_rel_mergeE [lemma, in graphs.skeleton]
sk_rel_irrefl [lemma, in graphs.skeleton]
sk_rel_sym [lemma, in graphs.skeleton]
sk_rel [definition, in graphs.skeleton]
smallest [definition, in graphs.preliminaries]
small_clique [lemma, in graphs.sgraph]
small_K_free [lemma, in graphs.minor]
Some_eqE [lemma, in graphs.preliminaries]
source [abbreviation, in graphs.mgraph]
source [abbreviation, in graphs.mgraph]
splitL [lemma, in graphs.digraph]
splitR [lemma, in graphs.digraph]
split_K4_nontrivial [lemma, in graphs.extraction_def]
split_at_last [lemma, in graphs.sgraph]
split_io_loop [lemma, in graphs.extraction_iso]
split_io_edge_lens [lemma, in graphs.extraction_iso]
split_io_edge [lemma, in graphs.extraction_iso]
split_io_edge_aux [lemma, in graphs.extraction_iso]
split_component [lemma, in graphs.extraction_iso]
split_cp [lemma, in graphs.extraction_iso]
split_pip [lemma, in graphs.extraction_iso]
split_at_first [lemma, in graphs.digraph]
split_at_first_aux [lemma, in graphs.digraph]
srestrict [definition, in graphs.sgraph]
srestrict_sym [lemma, in graphs.sgraph]
srev [definition, in graphs.sgraph]
srevK [lemma, in graphs.sgraph]
srev_nodes [lemma, in graphs.sgraph]
srev_rcons [lemma, in graphs.sgraph]
sskeleton [definition, in graphs.skeleton]
SSkeleton [section, in graphs.skeleton]
sskeleton_add [lemma, in graphs.extraction_def]
sskeleton_remove_io [lemma, in graphs.skeleton]
sskeleton_adjacent [lemma, in graphs.skeleton]
sskeleton_subgraph_for [lemma, in graphs.skeleton]
SSkeleton.IsoComponents [section, in graphs.skeleton]
SSkeleton.IsoComponents.C [variable, in graphs.skeleton]
SSkeleton.IsoComponents.comp_C [variable, in graphs.skeleton]
SSkeleton.IsoComponents.G [variable, in graphs.skeleton]
SSkeleton.IsoComponents.G1 [variable, in graphs.skeleton]
SSkeleton.IsoComponents.G2 [variable, in graphs.skeleton]
SSkeleton.L [variable, in graphs.skeleton]
sskelP [lemma, in graphs.skeleton]
sskel_K4_free [lemma, in graphs.mgraph2_tw2]
sskel_iso2 [instance, in graphs.skeleton]
ssplit_K4_nontrivial [lemma, in graphs.cp_minor]
ssplit_disconnected [lemma, in graphs.sgraph]
strict_is_minor [lemma, in graphs.minor]
strict_minor [definition, in graphs.minor]
structures [library]
Subalgebra [section, in graphs.mgraph2_tw2]
Subalgebra.L [variable, in graphs.mgraph2_tw2]
Subalgebra.Quotients [section, in graphs.mgraph2_tw2]
Subalgebra.Quotients.G1 [variable, in graphs.mgraph2_tw2]
Subalgebra.Quotients.G2 [variable, in graphs.mgraph2_tw2]
Subalgebra.Quotients.P [variable, in graphs.mgraph2_tw2]
subcp [lemma, in graphs.checkpoint]
subgraph [definition, in graphs.sgraph]
subgraph [definition, in graphs.mgraph]
subgraph_sub [lemma, in graphs.mgraph]
subgraph_for [definition, in graphs.mgraph]
subgraph_for_iso [lemma, in graphs.mgraph2]
subgraph_K4_free [lemma, in graphs.minor]
subrelP [lemma, in graphs.preliminaries]
subrel_restrict [lemma, in graphs.preliminaries]
subrel_del_edge [definition, in graphs.digraph]
subrel_pathp [lemma, in graphs.digraph]
subsetIlP1 [lemma, in graphs.excluded]
subset_seqL [lemma, in graphs.preliminaries]
subset_seqR [lemma, in graphs.preliminaries]
subset_cons [lemma, in graphs.preliminaries]
subset_tl [lemma, in graphs.equiv]
subset_catR [lemma, in graphs.equiv]
subset_catL [lemma, in graphs.equiv]
subset_pcatR [lemma, in graphs.digraph]
subset_pcatL [lemma, in graphs.digraph]
subtree_cut [lemma, in graphs.helly]
subT_bij [definition, in graphs.bij]
sub_connector [lemma, in graphs.connectivity]
sub_forest [lemma, in graphs.sgraph]
sub_inr [lemma, in graphs.treewidth]
sub_inl [lemma, in graphs.treewidth]
sub_equiv_of [lemma, in graphs.preliminaries]
sub_restrict_connect [lemma, in graphs.preliminaries]
sub_trans [lemma, in graphs.preliminaries]
sub_connect [lemma, in graphs.preliminaries]
sub_in11W [lemma, in graphs.preliminaries]
sub_val_eq [lemma, in graphs.preliminaries]
sub_sub [lemma, in graphs.skeleton]
sub_pointxx [lemma, in graphs.skeleton]
sub_edge [definition, in graphs.mgraph]
sub_vertex [definition, in graphs.mgraph]
sub_minor [lemma, in graphs.minor]
sumA [definition, in graphs.bij]
sumA' [definition, in graphs.bij]
sumC [definition, in graphs.bij]
sumf [definition, in graphs.bij]
sumUx [lemma, in graphs.bij]
sumxU [lemma, in graphs.bij]
sum_option_r [lemma, in graphs.bij]
sum_option_l [lemma, in graphs.bij]
sum_bij [instance, in graphs.bij]
sum_eqE [definition, in graphs.preliminaries]
sum_left [definition, in graphs.finite_quotient]
sunit [definition, in graphs.sgraph]
surjective [definition, in graphs.preliminaries]
surj_repr_pi [lemma, in graphs.finite_quotient]
svertex [projection, in graphs.sgraph]
svseparator_uniq [lemma, in graphs.connectivity]
svseparator_neighbours [lemma, in graphs.connectivity]
svseparator_connected [lemma, in graphs.connectivity]
symmetric_restrict_sedge [lemma, in graphs.sgraph]
symmetric_restrict [lemma, in graphs.preliminaries]
s.A [variable, in graphs.mgraph2_tw2]
s.Edges [section, in graphs.mgraph]
s.Edges.G [variable, in graphs.mgraph]
s.graph_of_term [variable, in graphs.mgraph2_tw2]
s.h_merge_nothing'.H [variable, in graphs.mgraph]
s.h_merge_nothing'.r [variable, in graphs.mgraph]
s.h_merge_nothing'.F [variable, in graphs.mgraph]
s.h_merge_nothing' [section, in graphs.mgraph]
s.L [variable, in graphs.mgraph]
s.L [variable, in graphs.mgraph2]
s.merge [section, in graphs.mgraph]
s.merge_union_K.ke [variable, in graphs.mgraph]
s.merge_union_K.kh [variable, in graphs.mgraph]
s.merge_union_K.kv [variable, in graphs.mgraph]
s.merge_union_K.k [variable, in graphs.mgraph]
s.merge_union_K.h [variable, in graphs.mgraph]
s.merge_union_K.K [variable, in graphs.mgraph]
s.merge_union_K.F [variable, in graphs.mgraph]
s.merge_union_K [section, in graphs.mgraph]
s.merge_merge_seq.kk' [variable, in graphs.mgraph]
s.merge_merge_seq.k' [variable, in graphs.mgraph]
s.merge_merge_seq.k [variable, in graphs.mgraph]
s.merge_merge_seq.h [variable, in graphs.mgraph]
s.merge_merge_seq.F [variable, in graphs.mgraph]
s.merge_merge_seq [section, in graphs.mgraph]
s.merge_nothing.H [variable, in graphs.mgraph]
s.merge_nothing.h [variable, in graphs.mgraph]
s.merge_nothing.F [variable, in graphs.mgraph]
s.merge_nothing [section, in graphs.mgraph]
s.merge_same.H [variable, in graphs.mgraph]
s.merge_same.k [variable, in graphs.mgraph]
s.merge_same.h [variable, in graphs.mgraph]
s.merge_same.F [variable, in graphs.mgraph]
s.merge_same [section, in graphs.mgraph]
s.merge_same'.H [variable, in graphs.mgraph]
s.merge_same'.k [variable, in graphs.mgraph]
s.merge_same'.h [variable, in graphs.mgraph]
s.merge_same'.F [variable, in graphs.mgraph]
s.merge_same' [section, in graphs.mgraph]
s.merge_merge.e' [variable, in graphs.mgraph]
s.merge_merge.e [variable, in graphs.mgraph]
s.merge_merge.F [variable, in graphs.mgraph]
s.merge_merge [section, in graphs.mgraph]
s.merge_surj.Hvlabel [variable, in graphs.mgraph]
s.merge_surj.Helabel [variable, in graphs.mgraph]
s.merge_surj.Hendpoints [variable, in graphs.mgraph]
s.merge_surj.Hsurj [variable, in graphs.mgraph]
s.merge_surj.Hr [variable, in graphs.mgraph]
s.merge_surj.fe [variable, in graphs.mgraph]
s.merge_surj.fv' [variable, in graphs.mgraph]
s.merge_surj.fv [variable, in graphs.mgraph]
s.merge_surj.H [variable, in graphs.mgraph]
s.merge_surj.r [variable, in graphs.mgraph]
s.merge_surj.G [variable, in graphs.mgraph]
s.merge_surj [section, in graphs.mgraph]
s.merge.F [variable, in graphs.mgraph]
s.merge.G [variable, in graphs.mgraph]
s.merge.h [variable, in graphs.mgraph]
s.merge.l [variable, in graphs.mgraph]
s.Subgraphs [section, in graphs.mgraph]
s.Subgraphs.E [variable, in graphs.mgraph]
s.Subgraphs.G [variable, in graphs.mgraph]
s.Subgraphs.in_V [variable, in graphs.mgraph]
s.Subgraphs.V [variable, in graphs.mgraph]
s.union_merge_r.l [variable, in graphs.mgraph]
s.union_merge_r.G [variable, in graphs.mgraph]
s.union_merge_r.F [variable, in graphs.mgraph]
s.union_merge_r [section, in graphs.mgraph]
s.union_merge_l.l [variable, in graphs.mgraph]
s.union_merge_l.G [variable, in graphs.mgraph]
s.union_merge_l.F [variable, in graphs.mgraph]
s.union_merge_l [section, in graphs.mgraph]
_ .d [notation, in graphs.mgraph]
_ .e [notation, in graphs.mgraph]
_ ≃ _ [notation, in graphs.mgraph]
_ ∔ _ [notation, in graphs.mgraph]
_ ⊎ _ [notation, in graphs.mgraph]
_ [tst _ <- _ ] [notation, in graphs.mgraph]
_ ∔ [ _ , _ , _ ] [notation, in graphs.mgraph]
_ ≃2p _ [notation, in graphs.mgraph2]
_ ≃2 _ [notation, in graphs.mgraph2]
_ [tst _ <- _ ] [notation, in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] [notation, in graphs.mgraph2]
_ ∔ _ [notation, in graphs.mgraph2]
T
t [section, in graphs.finite_quotient]tail [definition, in graphs.digraph]
tailW [lemma, in graphs.digraph]
take_find [lemma, in graphs.preliminaries]
target [abbreviation, in graphs.mgraph]
target [abbreviation, in graphs.mgraph]
term [inductive, in graphs.pttdom]
term [inductive, in graphs.ptt]
terms [section, in graphs.pttdom]
terms [section, in graphs.ptt]
terms.A [variable, in graphs.pttdom]
terms.A [variable, in graphs.ptt]
terms.e [section, in graphs.pttdom]
terms.e [section, in graphs.ptt]
terms.e.f [variable, in graphs.pttdom]
terms.e.f [variable, in graphs.ptt]
terms.e.X [variable, in graphs.pttdom]
terms.e.X [variable, in graphs.ptt]
term_of_nterm [definition, in graphs.pttdom]
term_of_eq [lemma, in graphs.extraction_def]
term_of_rec_eq [lemma, in graphs.extraction_def]
term_of [definition, in graphs.extraction_def]
term_of_rec [definition, in graphs.extraction_def]
term_of_measure [definition, in graphs.extraction_def]
term_of_iso' [lemma, in graphs.extraction_top]
term_of_eq' [lemma, in graphs.extraction_top]
term_of_rec_eq' [lemma, in graphs.extraction_top]
term_of' [definition, in graphs.extraction_top]
term_of_rec' [definition, in graphs.extraction_top]
term_of_iso [lemma, in graphs.extraction_iso]
test [abbreviation, in graphs.pttdom]
test [record, in graphs.pttdom]
Test [constructor, in graphs.pttdom]
testE [projection, in graphs.pttdom]
Theory [section, in graphs.structures]
Theory.mon0 [variable, in graphs.structures]
Theory.mon2 [variable, in graphs.structures]
Theory.X [variable, in graphs.structures]
_ ⊗ _ [notation, in graphs.structures]
1 [notation, in graphs.structures]
theta [lemma, in graphs.connectivity]
theta_vertices [lemma, in graphs.connectivity]
the_uPathP [lemma, in graphs.checkpoint]
the_uPath [definition, in graphs.checkpoint]
the_uPath_proof [lemma, in graphs.checkpoint]
three_way_split [lemma, in graphs.sgraph]
tjoin [definition, in graphs.treewidth]
tlink [definition, in graphs.treewidth]
tmEs [definition, in graphs.extraction_def]
tm_pttdom [definition, in graphs.pttdom]
tm_eqv_equivalence [lemma, in graphs.pttdom]
tm_eqv [definition, in graphs.pttdom]
tm_var [constructor, in graphs.pttdom]
tm_one [constructor, in graphs.pttdom]
tm_dom [constructor, in graphs.pttdom]
tm_cnv [constructor, in graphs.pttdom]
tm_par [constructor, in graphs.pttdom]
tm_dot [constructor, in graphs.pttdom]
tm_ [definition, in graphs.extraction_def]
tm_ptt [definition, in graphs.ptt]
tm_eqv_equivalence [lemma, in graphs.ptt]
tm_eqv [definition, in graphs.ptt]
tm_var [constructor, in graphs.ptt]
tm_top [constructor, in graphs.ptt]
tm_one [constructor, in graphs.ptt]
tm_dom [constructor, in graphs.ptt]
tm_cnv [constructor, in graphs.ptt]
tm_par [constructor, in graphs.ptt]
tm_dot [constructor, in graphs.ptt]
tnth_cons [lemma, in graphs.preliminaries]
tnth_map_in [lemma, in graphs.preliminaries]
tnth_uniq [lemma, in graphs.preliminaries]
top [projection, in graphs.pttdom]
topL [lemma, in graphs.mgraph2]
topR [lemma, in graphs.mgraph2]
total_minor_map [definition, in graphs.minor]
Transfer [section, in graphs.digraph]
Transfer.D1 [variable, in graphs.digraph]
Transfer.D2 [variable, in graphs.digraph]
Transfer.e1 [variable, in graphs.digraph]
Transfer.e2 [variable, in graphs.digraph]
Transfer.Npq [variable, in graphs.digraph]
Transfer.Npq' [variable, in graphs.digraph]
Transfer.p [variable, in graphs.digraph]
Transfer.p' [variable, in graphs.digraph]
Transfer.q [variable, in graphs.digraph]
Transfer.q' [variable, in graphs.digraph]
Transfer.T [variable, in graphs.digraph]
Transfer.x [variable, in graphs.digraph]
Transfer.y [variable, in graphs.digraph]
Tree [section, in graphs.helly]
treeI [lemma, in graphs.sgraph]
treewidth [library]
treewidth_K_free [lemma, in graphs.minor]
tree_helly [lemma, in graphs.helly]
tree_I3 [lemma, in graphs.helly]
tree_connectI [lemma, in graphs.helly]
Tree.G [variable, in graphs.helly]
Tree.tree_G [variable, in graphs.helly]
trivial_connector [lemma, in graphs.connectivity]
trivIset_components [lemma, in graphs.sgraph]
trivIset3 [lemma, in graphs.preliminaries]
triv_decomp [definition, in graphs.treewidth]
triv_sdecomp [definition, in graphs.treewidth]
tstpar [lemma, in graphs.pttdom]
tstpar1 [lemma, in graphs.pttdom]
tst_dotU [lemma, in graphs.pttdom]
tst_dotC [lemma, in graphs.pttdom]
tst_dotA [lemma, in graphs.pttdom]
tst_dot_eqv [lemma, in graphs.pttdom]
tunit [definition, in graphs.sgraph]
tuple_UPath [definition, in graphs.digraph]
two_graph_swap [lemma, in graphs.mgraph]
two_graph [definition, in graphs.mgraph]
two_graph2_iso [instance, in graphs.mgraph2]
two_graph2 [definition, in graphs.mgraph2]
TW1_forest [lemma, in graphs.minor]
TW2_of_K4F [lemma, in graphs.excluded]
TW2_K4_free [lemma, in graphs.minor]
t.e [variable, in graphs.finite_quotient]
t.f [variable, in graphs.finite_quotient]
t.H [variable, in graphs.finite_quotient]
t.S [variable, in graphs.finite_quotient]
U
uncycle [lemma, in graphs.digraph]union [definition, in graphs.mgraph]
union_bij_proofR [lemma, in graphs.finite_quotient]
union_bij_proofL [lemma, in graphs.finite_quotient]
union_K_equiv [definition, in graphs.finite_quotient]
union_quot_rEl [lemma, in graphs.finite_quotient]
union_quot_rEr [lemma, in graphs.finite_quotient]
union_quot_r [definition, in graphs.finite_quotient]
union_equiv_r [definition, in graphs.finite_quotient]
union_quot_r.e [variable, in graphs.finite_quotient]
union_quot_r.T [variable, in graphs.finite_quotient]
union_quot_r.S [variable, in graphs.finite_quotient]
union_quot_r [section, in graphs.finite_quotient]
union_quot_lE' [lemma, in graphs.finite_quotient]
union_quot_lEr [lemma, in graphs.finite_quotient]
union_quot_lEl [lemma, in graphs.finite_quotient]
union_quot_l [definition, in graphs.finite_quotient]
union_equiv_l_class [lemma, in graphs.finite_quotient]
union_equiv_l_rel [definition, in graphs.finite_quotient]
union_quot_l.e [variable, in graphs.finite_quotient]
union_quot_l.T [variable, in graphs.finite_quotient]
union_quot_l.S [variable, in graphs.finite_quotient]
union_quot_l [section, in graphs.finite_quotient]
union_K_pairs [definition, in graphs.mgraph]
union_merge_rEl [lemma, in graphs.mgraph]
union_merge_rEr [lemma, in graphs.mgraph]
union_merge_r [lemma, in graphs.mgraph]
union_merge_lE' [lemma, in graphs.mgraph]
union_merge_lEr [lemma, in graphs.mgraph]
union_merge_lEl [lemma, in graphs.mgraph]
union_merge_l [definition, in graphs.mgraph]
union_equiv_l_eqv_clot [lemma, in graphs.mgraph]
union_add_vlabel_r [lemma, in graphs.mgraph]
union_add_vlabel_l [lemma, in graphs.mgraph]
union_add_edge_r [lemma, in graphs.mgraph]
union_add_edge_l [lemma, in graphs.mgraph]
union_A [lemma, in graphs.mgraph]
union_C [lemma, in graphs.mgraph]
union_iso [instance, in graphs.mgraph]
unique [definition, in graphs.preliminaries]
unique_forestT [lemma, in graphs.sgraph]
uniq_take [lemma, in graphs.preliminaries]
unit_forest [definition, in graphs.sgraph]
unit_graph_iso [instance, in graphs.mgraph]
unit_graph [definition, in graphs.mgraph]
unit_graph2_iso [instance, in graphs.mgraph2]
unit_graph2 [definition, in graphs.mgraph2]
unl [definition, in graphs.mgraph]
unr [definition, in graphs.mgraph]
UPath [abbreviation, in graphs.digraph]
UPath [record, in graphs.digraph]
upath [definition, in graphs.digraph]
uPathP [lemma, in graphs.digraph]
upathP [lemma, in graphs.digraph]
upathPR [lemma, in graphs.sgraph]
uPathRP [lemma, in graphs.sgraph]
UPathW [definition, in graphs.digraph]
upathW [lemma, in graphs.digraph]
upathWW [lemma, in graphs.digraph]
upath_sym [lemma, in graphs.sgraph]
upath_of [definition, in graphs.digraph]
upath_irred [lemma, in graphs.digraph]
UPath_finMixin [definition, in graphs.digraph]
UPath_tupleK [lemma, in graphs.digraph]
UPath_tuple [definition, in graphs.digraph]
upath_size [lemma, in graphs.digraph]
UPath_countMixin [definition, in graphs.digraph]
UPath_choiceMixin [definition, in graphs.digraph]
UPath_eqMixin [definition, in graphs.digraph]
upath_nil [lemma, in graphs.digraph]
upath_consE [lemma, in graphs.digraph]
upath_cons [lemma, in graphs.digraph]
upath_uniq [lemma, in graphs.digraph]
update [definition, in graphs.preliminaries]
update [section, in graphs.preliminaries]
updateE [definition, in graphs.preliminaries]
update_fx [lemma, in graphs.preliminaries]
update_same [lemma, in graphs.preliminaries]
update_eq [lemma, in graphs.preliminaries]
update_neq [lemma, in graphs.preliminaries]
update.aT [variable, in graphs.preliminaries]
update.f [variable, in graphs.preliminaries]
update.rT [variable, in graphs.preliminaries]
USplit [constructor, in graphs.digraph]
usplit [inductive, in graphs.digraph]
usplitP [lemma, in graphs.digraph]
uval [projection, in graphs.digraph]
V
valK' [lemma, in graphs.preliminaries]valK'' [lemma, in graphs.preliminaries]
vcover [definition, in graphs.connectivity]
vcover [section, in graphs.connectivity]
vcoverP [lemma, in graphs.connectivity]
vcover.G [variable, in graphs.connectivity]
vcover.V [variable, in graphs.connectivity]
vertex [projection, in graphs.mgraph]
vfun [abbreviation, in graphs.preliminaries]
vlabel [projection, in graphs.mgraph]
vlabel_iso' [lemma, in graphs.mgraph]
vlabel_iso [lemma, in graphs.mgraph]
vlabel_hom [projection, in graphs.mgraph]
void [inductive, in graphs.preliminaries]
void_enumP [lemma, in graphs.preliminaries]
void_countMixin [definition, in graphs.preliminaries]
void_choiceMixin [definition, in graphs.preliminaries]
void_pcancel [lemma, in graphs.preliminaries]
void_eqP [lemma, in graphs.preliminaries]
void_graph [definition, in graphs.mgraph]
vseparator [definition, in graphs.connectivity]
VSeparator [section, in graphs.connectivity]
vseparatorb [definition, in graphs.connectivity]
vseparatorNE [lemma, in graphs.connectivity]
vseparatorP [lemma, in graphs.connectivity]
vseparator_separation [lemma, in graphs.connectivity]
VSeparator.G [variable, in graphs.connectivity]
W
walk [definition, in graphs.mgraph]Walk [section, in graphs.mgraph]
walk_of_line [lemma, in graphs.mgraph]
Walk.G [variable, in graphs.mgraph]
Walk.L [variable, in graphs.mgraph]
wf_propers [lemma, in graphs.preliminaries]
wf_proper [lemma, in graphs.preliminaries]
wf_leq [lemma, in graphs.preliminaries]
width [definition, in graphs.sgraph]
width_bound [lemma, in graphs.sgraph]
width_link [lemma, in graphs.treewidth]
width_minor [lemma, in graphs.minor]
other
_ ==> _ (csignature) [notation, in graphs.structures]_ [tst _ <- _ ] (graph_scope) [notation, in graphs.mgraph]
_ ∔ _ (graph_scope) [notation, in graphs.mgraph]
_ ∔ [ _ , _ , _ ] (graph_scope) [notation, in graphs.mgraph]
_ ⊎ _ (graph_scope) [notation, in graphs.mgraph]
_ [tst _ <- _ ] (graph2_scope) [notation, in graphs.mgraph2]
_ ∔ _ (graph2_scope) [notation, in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] (graph2_scope) [notation, in graphs.mgraph2]
IPATH _ _ _ (implicit_scope) [notation, in graphs.digraph]
PATH _ _ _ (implicit_scope) [notation, in graphs.digraph]
_ -- _ :> _ (implicit_scope) [notation, in graphs.digraph]
_ ⊗ _ (labels) [notation, in graphs.structures]
1 (labels) [notation, in graphs.structures]
[ _ ] (pttdom_ops) [notation, in graphs.pttdom]
1 (pttdom_ops) [notation, in graphs.pttdom]
_ ° (pttdom_ops) [notation, in graphs.pttdom]
_ · _ (pttdom_ops) [notation, in graphs.pttdom]
_ ∥ _ (pttdom_ops) [notation, in graphs.pttdom]
_ @^-1 _ (set_scope) [notation, in graphs.preliminaries]
_ ^-1 [notation, in graphs.bij]
_ <[ _ ] _ [notation, in graphs.sgraph]
_ ≡[ _ ] _ [notation, in graphs.structures]
_ ≡' _ [notation, in graphs.structures]
_ ≡ _ [notation, in graphs.structures]
_ ⋄ _ [notation, in graphs.checkpoint]
_ [upd _ := _ ] [notation, in graphs.preliminaries]
_ == _ %[mod _ ] [notation, in graphs.finite_quotient]
_ = _ %[mod _ ] [notation, in graphs.finite_quotient]
_ -- _ [notation, in graphs.digraph]
_ .d [notation, in graphs.mgraph]
_ .e [notation, in graphs.mgraph]
_ ≃ _ [notation, in graphs.mgraph]
_ ≃2p _ [notation, in graphs.mgraph2]
_ ≃2 _ [notation, in graphs.mgraph2]
'K_ _ [notation, in graphs.sgraph]
[ disjoint3 _ & _ & _ ] [notation, in graphs.preliminaries]
\pi _ [notation, in graphs.finite_quotient]
Σ _ .. _ , _ [notation, in graphs.preliminaries]
Notation Index
C
_ ⋄ _ [in graphs.checkpoint]D
[ _ ] [in graphs.pttdom]S
_ .d [in graphs.mgraph]_ .e [in graphs.mgraph]
_ ≃ _ [in graphs.mgraph]
_ ∔ _ [in graphs.mgraph]
_ ⊎ _ [in graphs.mgraph]
_ [tst _ <- _ ] [in graphs.mgraph]
_ ∔ [ _ , _ , _ ] [in graphs.mgraph]
_ ≃2p _ [in graphs.mgraph2]
_ ≃2 _ [in graphs.mgraph2]
_ [tst _ <- _ ] [in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] [in graphs.mgraph2]
_ ∔ _ [in graphs.mgraph2]
T
_ ⊗ _ [in graphs.structures]1 [in graphs.structures]
other
_ ==> _ (csignature) [in graphs.structures]_ [tst _ <- _ ] (graph_scope) [in graphs.mgraph]
_ ∔ _ (graph_scope) [in graphs.mgraph]
_ ∔ [ _ , _ , _ ] (graph_scope) [in graphs.mgraph]
_ ⊎ _ (graph_scope) [in graphs.mgraph]
_ [tst _ <- _ ] (graph2_scope) [in graphs.mgraph2]
_ ∔ _ (graph2_scope) [in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] (graph2_scope) [in graphs.mgraph2]
IPATH _ _ _ (implicit_scope) [in graphs.digraph]
PATH _ _ _ (implicit_scope) [in graphs.digraph]
_ -- _ :> _ (implicit_scope) [in graphs.digraph]
_ ⊗ _ (labels) [in graphs.structures]
1 (labels) [in graphs.structures]
[ _ ] (pttdom_ops) [in graphs.pttdom]
1 (pttdom_ops) [in graphs.pttdom]
_ ° (pttdom_ops) [in graphs.pttdom]
_ · _ (pttdom_ops) [in graphs.pttdom]
_ ∥ _ (pttdom_ops) [in graphs.pttdom]
_ @^-1 _ (set_scope) [in graphs.preliminaries]
_ ^-1 [in graphs.bij]
_ <[ _ ] _ [in graphs.sgraph]
_ ≡[ _ ] _ [in graphs.structures]
_ ≡' _ [in graphs.structures]
_ ≡ _ [in graphs.structures]
_ ⋄ _ [in graphs.checkpoint]
_ [upd _ := _ ] [in graphs.preliminaries]
_ == _ %[mod _ ] [in graphs.finite_quotient]
_ = _ %[mod _ ] [in graphs.finite_quotient]
_ -- _ [in graphs.digraph]
_ .d [in graphs.mgraph]
_ .e [in graphs.mgraph]
_ ≃ _ [in graphs.mgraph]
_ ≃2p _ [in graphs.mgraph2]
_ ≃2 _ [in graphs.mgraph2]
'K_ _ [in graphs.sgraph]
[ disjoint3 _ & _ & _ ] [in graphs.preliminaries]
\pi _ [in graphs.finite_quotient]
Σ _ .. _ , _ [in graphs.preliminaries]
Module Index
Q
quot [in graphs.finite_quotient]QUOT [in graphs.finite_quotient]
Variable Index
A
AddEdge.discT [in graphs.treewidth]AddEdge.T [in graphs.treewidth]
AddEdge.T' [in graphs.treewidth]
AddEdge.t0 [in graphs.treewidth]
AddEdge.t1 [in graphs.treewidth]
AddNode.G [in graphs.sgraph]
AddNode.N [in graphs.sgraph]
B
BijCast.A [in graphs.finmap_plus]BijCast.A' [in graphs.finmap_plus]
BijCast.eqA [in graphs.finmap_plus]
BijCast.T [in graphs.finmap_plus]
BijD1.T [in graphs.bij]
BijD1.z [in graphs.bij]
BijT.inP [in graphs.bij]
BijT.P [in graphs.bij]
BijT.T [in graphs.bij]
Bij.g [in graphs.finmap_plus]
Bij.G [in graphs.finmap_plus]
Bij.g_inj [in graphs.finmap_plus]
Bij.T [in graphs.finmap_plus]
Bij.vset [in graphs.finmap_plus]
Bounded.aT [in graphs.bounded]
Bounded.F [in graphs.bounded]
Bounded.F_wf [in graphs.bounded]
Bounded.measure [in graphs.bounded]
Bounded.P [in graphs.bounded]
Bounded.rT [in graphs.bounded]
Bounded.x0 [in graphs.bounded]
b.e [in graphs.finite_quotient]
b.h [in graphs.finite_quotient]
b.S [in graphs.finite_quotient]
b.T [in graphs.finite_quotient]
C
CheckpointOrder.conn_io [in graphs.checkpoint]CheckpointOrder.G [in graphs.checkpoint]
CheckpointOrder.i [in graphs.checkpoint]
CheckpointOrder.o [in graphs.checkpoint]
CheckpointsAndMinors.conn_G [in graphs.cp_minor]
CheckpointsAndMinors.G [in graphs.cp_minor]
CheckPoints.G [in graphs.checkpoint]
CheckPoints.G_conn [in graphs.checkpoint]
CheckPoints.G_conn' [in graphs.checkpoint]
Cliques.G [in graphs.sgraph]
CProper.A [in graphs.structures]
CProper.B [in graphs.structures]
CProper.C [in graphs.structures]
CProper.f [in graphs.structures]
CProper.g [in graphs.structures]
CProper.Hf [in graphs.structures]
CProper.Hg [in graphs.structures]
CProper.R [in graphs.structures]
CProper.S [in graphs.structures]
CProper.T [in graphs.structures]
D
DecompTheory.B [in graphs.treewidth]DecompTheory.decD [in graphs.treewidth]
DecompTheory.G [in graphs.treewidth]
DecompTheory.T [in graphs.treewidth]
DelEdge.a [in graphs.digraph]
DelEdge.ab [in graphs.digraph]
DelEdge.b [in graphs.digraph]
DelEdge.G [in graphs.digraph]
derived.X [in graphs.pttdom]
derived.X [in graphs.ptt]
DiGraphTheory.D [in graphs.digraph]
DiGraphTheory.Fixed.p [in graphs.digraph]
DiGraphTheory.Fixed.q [in graphs.digraph]
DiGraphTheory.Fixed.x [in graphs.digraph]
DiGraphTheory.Fixed.y [in graphs.digraph]
DiGraphTheory.Fixed.z [in graphs.digraph]
DiPathTheory.Finite.x [in graphs.digraph]
DiPathTheory.Finite.y [in graphs.digraph]
DiPathTheory.G [in graphs.digraph]
DiPathTheory.IPath.x [in graphs.digraph]
DiPathTheory.IPath.y [in graphs.digraph]
Disjoint3.A [in graphs.preliminaries]
Disjoint3.B [in graphs.preliminaries]
Disjoint3.C [in graphs.preliminaries]
Disjoint3.T [in graphs.preliminaries]
E
Equivalence.e [in graphs.preliminaries]Equivalence.T [in graphs.preliminaries]
eqv_inj.f_inj [in graphs.equiv]
eqv_inj.eq2E [in graphs.equiv]
eqv_inj.eq_e [in graphs.equiv]
eqv_inj.f [in graphs.equiv]
eqv_inj.e2 [in graphs.equiv]
eqv_inj.e1 [in graphs.equiv]
eqv_inj.T2 [in graphs.equiv]
eqv_inj.T1 [in graphs.equiv]
ExtractionDef.SplitCP.CK4F_G [in graphs.extraction_def]
ExtractionDef.SplitCP.G [in graphs.extraction_def]
ExtractionDef.SplitCP.Hio [in graphs.extraction_def]
ExtractionDef.SplitCP.Hz [in graphs.extraction_def]
ExtractionDef.SplitCP.Hz' [in graphs.extraction_def]
ExtractionDef.SplitCP.z [in graphs.extraction_def]
ExtractionDef.SplitCP.Zi [in graphs.extraction_def]
ExtractionDef.SplitCP.Zo [in graphs.extraction_def]
ExtractionDef.sym [in graphs.extraction_def]
ExtractionIso.sym [in graphs.extraction_iso]
ExtractionTop.sym [in graphs.extraction_top]
F
FinEncodingModuloRel.C [in graphs.finite_quotient]FinEncodingModuloRel.CD [in graphs.finite_quotient]
FinEncodingModuloRel.D [in graphs.finite_quotient]
FinEncodingModuloRel.DC [in graphs.finite_quotient]
FinEncodingModuloRel.eD [in graphs.finite_quotient]
FinEncodingModuloRel.encD [in graphs.finite_quotient]
Foldr1.F [in graphs.preliminaries]
Foldr1.I [in graphs.preliminaries]
Foldr1.op [in graphs.preliminaries]
Foldr1.R [in graphs.preliminaries]
Forests.G [in graphs.sgraph]
Fresh2Bij.A [in graphs.finmap_plus]
Fresh2Bij.B [in graphs.finmap_plus]
Fresh2Bij.f [in graphs.finmap_plus]
Fresh2Bij.Hx [in graphs.finmap_plus]
Fresh2Bij.Hy [in graphs.finmap_plus]
Fresh2Bij.T [in graphs.finmap_plus]
Fresh2Bij.x [in graphs.finmap_plus]
Fresh2Bij.y [in graphs.finmap_plus]
fsetD_bij.E [in graphs.finmap_plus]
fsetD_bij.f [in graphs.finmap_plus]
fsetD_bij.C' [in graphs.finmap_plus]
fsetD_bij.C [in graphs.finmap_plus]
fsetD_bij.B [in graphs.finmap_plus]
fsetD_bij.A [in graphs.finmap_plus]
fsetD_bij.T [in graphs.finmap_plus]
FsetU1Fun.A [in graphs.finmap_plus]
FsetU1Fun.B [in graphs.finmap_plus]
FsetU1Fun.f [in graphs.finmap_plus]
FsetU1Fun.T [in graphs.finmap_plus]
FsetU1Fun.x [in graphs.finmap_plus]
FsetU1Fun.y [in graphs.finmap_plus]
H
h.fe [in graphs.mgraph2]h.fv [in graphs.mgraph2]
h.Hfe [in graphs.mgraph2]
h.Hfv [in graphs.mgraph2]
h.Hfvmon0 [in graphs.mgraph2]
h.Hfvmon2 [in graphs.mgraph2]
h.X [in graphs.mgraph2]
h.Y [in graphs.mgraph2]
I
InducedSubgraph.G [in graphs.sgraph]InducedSubgraph.G [in graphs.digraph]
InducedSubgraph.S [in graphs.sgraph]
InducedSubgraph.S [in graphs.digraph]
Interior.G [in graphs.digraph]
Interior.x [in graphs.digraph]
Interior.y [in graphs.digraph]
J
JoinSG.G1 [in graphs.sgraph]JoinSG.G2 [in graphs.sgraph]
JoinT.T1 [in graphs.treewidth]
JoinT.T2 [in graphs.treewidth]
L
Link.T [in graphs.treewidth]Link.U [in graphs.treewidth]
Link.U_disc [in graphs.treewidth]
M
map_equiv.e [in graphs.finite_quotient]map_equiv.h [in graphs.finite_quotient]
map_equiv.T [in graphs.finite_quotient]
map_equiv.S [in graphs.finite_quotient]
Max.split [in graphs.bounded]
Max.split_lt [in graphs.bounded]
MergeSubgraph.A [in graphs.mgraph]
MergeSubgraph.con1 [in graphs.mgraph]
MergeSubgraph.con2 [in graphs.mgraph]
MergeSubgraph.disE [in graphs.mgraph]
MergeSubgraph.eqvI [in graphs.mgraph]
MergeSubgraph.E1 [in graphs.mgraph]
MergeSubgraph.E2 [in graphs.mgraph]
MergeSubgraph.G [in graphs.mgraph]
MergeSubgraph.h [in graphs.mgraph]
MergeSubgraph.V1 [in graphs.mgraph]
MergeSubgraph.V2 [in graphs.mgraph]
N
Neighbor.G [in graphs.sgraph]P
Packaged.G [in graphs.sgraph]Packaged.Prev.p [in graphs.sgraph]
Packaged.Prev.q [in graphs.sgraph]
Packaged.Prev.x [in graphs.sgraph]
Packaged.Prev.y [in graphs.sgraph]
Packaged.Prev.z [in graphs.sgraph]
Pack.PathDef.x [in graphs.digraph]
Pack.PathDef.y [in graphs.digraph]
Pack.T [in graphs.digraph]
PathIndexing.G [in graphs.sgraph]
PathIndexing.IDX.dis_pq [in graphs.sgraph]
PathIndexing.IDX.irr_q [in graphs.sgraph]
PathIndexing.IDX.irr_p [in graphs.sgraph]
PathIndexing.IDX.irr_pq [in graphs.sgraph]
PathIndexing.IDX.p [in graphs.sgraph]
PathIndexing.IDX.q [in graphs.sgraph]
PathIndexing.IDX.x [in graphs.sgraph]
PathIndexing.IDX.y [in graphs.sgraph]
PathIndexing.IDX.z [in graphs.sgraph]
PathOps.p [in graphs.digraph]
PathOps.q [in graphs.digraph]
PathOps.T [in graphs.digraph]
PathOps.x [in graphs.digraph]
PathOps.y [in graphs.digraph]
PathOps.z [in graphs.digraph]
PathP.T [in graphs.digraph]
PathS.G [in graphs.digraph]
PathTheory.Fixed.p [in graphs.digraph]
PathTheory.Fixed.q [in graphs.digraph]
PathTheory.Fixed.x [in graphs.digraph]
PathTheory.Fixed.y [in graphs.digraph]
PathTheory.Fixed.z [in graphs.digraph]
PathTheory.G [in graphs.digraph]
Q
QuotBij.e1 [in graphs.finite_quotient]QuotBij.e2 [in graphs.finite_quotient]
QuotBij.h [in graphs.finite_quotient]
QuotBij.h_inv_can [in graphs.finite_quotient]
QuotBij.h_can [in graphs.finite_quotient]
QuotBij.h_inv_homo [in graphs.finite_quotient]
QuotBij.h_homo [in graphs.finite_quotient]
QuotBij.h_inv [in graphs.finite_quotient]
QuotBij.T1 [in graphs.finite_quotient]
QuotBij.T2 [in graphs.finite_quotient]
QuotFun.e1 [in graphs.finite_quotient]
QuotFun.e2 [in graphs.finite_quotient]
QuotFun.h1 [in graphs.finite_quotient]
QuotFun.T1 [in graphs.finite_quotient]
QuotFun.T2 [in graphs.finite_quotient]
quot_union_K.kh [in graphs.finite_quotient]
quot_union_K.k [in graphs.finite_quotient]
quot_union_K.e [in graphs.finite_quotient]
quot_union_K.K [in graphs.finite_quotient]
quot_union_K.S [in graphs.finite_quotient]
quot_id.H [in graphs.finite_quotient]
quot_id.e [in graphs.finite_quotient]
quot_id.T [in graphs.finite_quotient]
quot_quot.e' [in graphs.finite_quotient]
quot_quot.e [in graphs.finite_quotient]
quot_quot.T [in graphs.finite_quotient]
quot_kernel.Hf [in graphs.finite_quotient]
quot_kernel.Hr [in graphs.finite_quotient]
quot_kernel.f' [in graphs.finite_quotient]
quot_kernel.f [in graphs.finite_quotient]
quot_kernel.r [in graphs.finite_quotient]
quot.s.e [in graphs.finite_quotient]
quot.s.T [in graphs.finite_quotient]
S
SeparatorConnector.ConnectorTheory.A [in graphs.connectivity]SeparatorConnector.ConnectorTheory.B [in graphs.connectivity]
SeparatorConnector.ConnectorTheory.conn_p [in graphs.connectivity]
SeparatorConnector.ConnectorTheory.n [in graphs.connectivity]
SeparatorConnector.ConnectorTheory.p [in graphs.connectivity]
SeparatorConnector.G [in graphs.connectivity]
SetTac.A [in graphs.set_tac]
SetTac.B [in graphs.set_tac]
SetTac.C [in graphs.set_tac]
SetTac.T [in graphs.set_tac]
sig_sum_bij.NonDisjoint.eqvI [in graphs.finite_quotient]
sig_sum_bij.NonDisjoint.e [in graphs.finite_quotient]
sig_sum_bij.Disjoint.disUV [in graphs.finite_quotient]
sig_sum_bij.V [in graphs.finite_quotient]
sig_sum_bij.U [in graphs.finite_quotient]
sig_sum_bij.T [in graphs.finite_quotient]
SimplePaths.G [in graphs.sgraph]
Skeleton.L [in graphs.skeleton]
SSkeleton.IsoComponents.C [in graphs.skeleton]
SSkeleton.IsoComponents.comp_C [in graphs.skeleton]
SSkeleton.IsoComponents.G [in graphs.skeleton]
SSkeleton.IsoComponents.G1 [in graphs.skeleton]
SSkeleton.IsoComponents.G2 [in graphs.skeleton]
SSkeleton.L [in graphs.skeleton]
Subalgebra.L [in graphs.mgraph2_tw2]
Subalgebra.Quotients.G1 [in graphs.mgraph2_tw2]
Subalgebra.Quotients.G2 [in graphs.mgraph2_tw2]
Subalgebra.Quotients.P [in graphs.mgraph2_tw2]
s.A [in graphs.mgraph2_tw2]
s.Edges.G [in graphs.mgraph]
s.graph_of_term [in graphs.mgraph2_tw2]
s.h_merge_nothing'.H [in graphs.mgraph]
s.h_merge_nothing'.r [in graphs.mgraph]
s.h_merge_nothing'.F [in graphs.mgraph]
s.L [in graphs.mgraph]
s.L [in graphs.mgraph2]
s.merge_union_K.ke [in graphs.mgraph]
s.merge_union_K.kh [in graphs.mgraph]
s.merge_union_K.kv [in graphs.mgraph]
s.merge_union_K.k [in graphs.mgraph]
s.merge_union_K.h [in graphs.mgraph]
s.merge_union_K.K [in graphs.mgraph]
s.merge_union_K.F [in graphs.mgraph]
s.merge_merge_seq.kk' [in graphs.mgraph]
s.merge_merge_seq.k' [in graphs.mgraph]
s.merge_merge_seq.k [in graphs.mgraph]
s.merge_merge_seq.h [in graphs.mgraph]
s.merge_merge_seq.F [in graphs.mgraph]
s.merge_nothing.H [in graphs.mgraph]
s.merge_nothing.h [in graphs.mgraph]
s.merge_nothing.F [in graphs.mgraph]
s.merge_same.H [in graphs.mgraph]
s.merge_same.k [in graphs.mgraph]
s.merge_same.h [in graphs.mgraph]
s.merge_same.F [in graphs.mgraph]
s.merge_same'.H [in graphs.mgraph]
s.merge_same'.k [in graphs.mgraph]
s.merge_same'.h [in graphs.mgraph]
s.merge_same'.F [in graphs.mgraph]
s.merge_merge.e' [in graphs.mgraph]
s.merge_merge.e [in graphs.mgraph]
s.merge_merge.F [in graphs.mgraph]
s.merge_surj.Hvlabel [in graphs.mgraph]
s.merge_surj.Helabel [in graphs.mgraph]
s.merge_surj.Hendpoints [in graphs.mgraph]
s.merge_surj.Hsurj [in graphs.mgraph]
s.merge_surj.Hr [in graphs.mgraph]
s.merge_surj.fe [in graphs.mgraph]
s.merge_surj.fv' [in graphs.mgraph]
s.merge_surj.fv [in graphs.mgraph]
s.merge_surj.H [in graphs.mgraph]
s.merge_surj.r [in graphs.mgraph]
s.merge_surj.G [in graphs.mgraph]
s.merge.F [in graphs.mgraph]
s.merge.G [in graphs.mgraph]
s.merge.h [in graphs.mgraph]
s.merge.l [in graphs.mgraph]
s.Subgraphs.E [in graphs.mgraph]
s.Subgraphs.G [in graphs.mgraph]
s.Subgraphs.in_V [in graphs.mgraph]
s.Subgraphs.V [in graphs.mgraph]
s.union_merge_r.l [in graphs.mgraph]
s.union_merge_r.G [in graphs.mgraph]
s.union_merge_r.F [in graphs.mgraph]
s.union_merge_l.l [in graphs.mgraph]
s.union_merge_l.G [in graphs.mgraph]
s.union_merge_l.F [in graphs.mgraph]
T
terms.A [in graphs.pttdom]terms.A [in graphs.ptt]
terms.e.f [in graphs.pttdom]
terms.e.f [in graphs.ptt]
terms.e.X [in graphs.pttdom]
terms.e.X [in graphs.ptt]
Theory.mon0 [in graphs.structures]
Theory.mon2 [in graphs.structures]
Theory.X [in graphs.structures]
Transfer.D1 [in graphs.digraph]
Transfer.D2 [in graphs.digraph]
Transfer.e1 [in graphs.digraph]
Transfer.e2 [in graphs.digraph]
Transfer.Npq [in graphs.digraph]
Transfer.Npq' [in graphs.digraph]
Transfer.p [in graphs.digraph]
Transfer.p' [in graphs.digraph]
Transfer.q [in graphs.digraph]
Transfer.q' [in graphs.digraph]
Transfer.T [in graphs.digraph]
Transfer.x [in graphs.digraph]
Transfer.y [in graphs.digraph]
Tree.G [in graphs.helly]
Tree.tree_G [in graphs.helly]
t.e [in graphs.finite_quotient]
t.f [in graphs.finite_quotient]
t.H [in graphs.finite_quotient]
t.S [in graphs.finite_quotient]
U
union_quot_r.e [in graphs.finite_quotient]union_quot_r.T [in graphs.finite_quotient]
union_quot_r.S [in graphs.finite_quotient]
union_quot_l.e [in graphs.finite_quotient]
union_quot_l.T [in graphs.finite_quotient]
union_quot_l.S [in graphs.finite_quotient]
update.aT [in graphs.preliminaries]
update.f [in graphs.preliminaries]
update.rT [in graphs.preliminaries]
V
vcover.G [in graphs.connectivity]vcover.V [in graphs.connectivity]
VSeparator.G [in graphs.connectivity]
W
Walk.G [in graphs.mgraph]Walk.L [in graphs.mgraph]
Library Index
B
bijbounded
C
checkpointconnectivity
cp_minor
D
digraphE
edoneequiv
excluded
extraction_iso
extraction_top
extraction_def
F
finite_quotientfinmap_plus
H
hellyM
mgraphmgraph2
mgraph2_tw2
minor
P
preliminariesptt
pttdom
S
set_tacsgraph
skeleton
structures
T
treewidthLemma Index
A
above_largest [in graphs.preliminaries]add_edge_induced_iso [in graphs.cp_minor]
add_edge_split_disjoint [in graphs.excluded]
add_edge_split_connected [in graphs.excluded]
add_edge_separation [in graphs.excluded]
add_node_complete [in graphs.sgraph]
add_node_lift_Path [in graphs.sgraph]
add_node_irrefl [in graphs.sgraph]
add_node_sym [in graphs.sgraph]
add_edge_keep_connected_l [in graphs.sgraph]
add_edge_avoid [in graphs.sgraph]
add_edge_pathC [in graphs.sgraph]
add_edge_connected_sym [in graphs.sgraph]
add_edge_sym [in graphs.sgraph]
add_edgeC [in graphs.sgraph]
add_edge_connected [in graphs.sgraph]
add_edge_Path [in graphs.sgraph]
add_edge_irrefl_ [in graphs.sgraph]
add_edge_sym_ [in graphs.sgraph]
add_edge_is_forest [in graphs.treewidth]
add_edge_break [in graphs.treewidth]
add_vlabel_edge [in graphs.mgraph]
add_vlabel_two [in graphs.mgraph]
add_vlabel_mon0 [in graphs.mgraph]
add_vlabel_unit [in graphs.mgraph]
add_vlabel_C [in graphs.mgraph]
add_vlabel_iso [in graphs.mgraph]
add_vlabel_iso' [in graphs.mgraph]
add_vlabel_iso'' [in graphs.mgraph]
add_edge_vlabel [in graphs.mgraph]
add_edge_rev [in graphs.mgraph]
add_edge_C [in graphs.mgraph]
add_edge_iso [in graphs.mgraph]
add_edge_iso' [in graphs.mgraph]
add_edge_iso'' [in graphs.mgraph]
add_vlabel2_mon0 [in graphs.mgraph2]
add_vlabel2_edge [in graphs.mgraph2]
add_vlabel2_two [in graphs.mgraph2]
add_vlabel2_unit' [in graphs.mgraph2]
add_vlabel2_unit [in graphs.mgraph2]
add_vlabel2_C [in graphs.mgraph2]
add_vlabel2_iso [in graphs.mgraph2]
add_vlabel2_iso' [in graphs.mgraph2]
add_vlabel2_iso'' [in graphs.mgraph2]
add_edge2_vlabel [in graphs.mgraph2]
add_edge2_rev [in graphs.mgraph2]
add_edge2_C [in graphs.mgraph2]
add_edge2_iso [in graphs.mgraph2]
add_edge2_iso' [in graphs.mgraph2]
add_edge2_iso'' [in graphs.mgraph2]
add_node_minor [in graphs.minor]
adjacentI [in graphs.skeleton]
adjacentP [in graphs.skeleton]
adjacent_induced [in graphs.skeleton]
adjacent_edge [in graphs.skeleton]
adjacent_sym [in graphs.skeleton]
admissible_eqv_clot [in graphs.mgraph2_tw2]
all_cons [in graphs.preliminaries]
avoid_nonseperator [in graphs.connectivity]
A13_ [in graphs.ptt]
A14_ [in graphs.ptt]
B
bagP [in graphs.checkpoint]bagPn [in graphs.checkpoint]
bag_interval_cap [in graphs.checkpoint]
bag_cp [in graphs.checkpoint]
bag_disj [in graphs.checkpoint]
bag_exit_edge [in graphs.checkpoint]
bag_exit' [in graphs.checkpoint]
bag_exit [in graphs.checkpoint]
bag_sub_sinterval [in graphs.checkpoint]
bag_nontrivial [in graphs.checkpoint]
bag_id [in graphs.checkpoint]
bag_edges_disj [in graphs.skeleton]
below_smallest [in graphs.preliminaries]
bgraph_eq_io [in graphs.skeleton]
bigcup_set1 [in graphs.preliminaries]
bigD1 [in graphs.structures]
bigID [in graphs.structures]
big_unit [in graphs.structures]
big_sum [in graphs.structures]
big_pred1 [in graphs.structures]
big_pred1_eq [in graphs.structures]
big_seq1 [in graphs.structures]
big_split [in graphs.structures]
big_cat [in graphs.structures]
big_mkcond [in graphs.structures]
bij_perm_enum [in graphs.bij]
bij_same [in graphs.bij]
bij_sumA [in graphs.bij]
bij_sumC [in graphs.bij]
bij_eqLR [in graphs.bij]
bij_imsetC [in graphs.bij]
bij_mem_imset [in graphs.bij]
bij_injective' [in graphs.bij]
bij_injective [in graphs.bij]
bij_bijective' [in graphs.bij]
bij_bijective [in graphs.bij]
bij_castE [in graphs.finmap_plus]
bij_surj [in graphs.preliminaries]
bij_card_eq [in graphs.preliminaries]
bij_quotE' [in graphs.finite_quotient]
bij_quotE [in graphs.finite_quotient]
bip_separation_vcover [in graphs.connectivity]
bool_two [in graphs.bij]
C
can_bijD1_bwd [in graphs.bij]can_bijD1_fwd [in graphs.bij]
can_vset' [in graphs.finmap_plus]
can_vset [in graphs.finmap_plus]
can_irred_of [in graphs.digraph]
cardsCT [in graphs.preliminaries]
cardsDsub [in graphs.finmap_plus]
cardsI [in graphs.preliminaries]
cardsIsub [in graphs.finmap_plus]
cards2P [in graphs.preliminaries]
cards3 [in graphs.preliminaries]
card_matching_of [in graphs.connectivity]
card_dimatching_of [in graphs.connectivity]
card_bij [in graphs.bij]
card_void [in graphs.preliminaries]
card_le1P [in graphs.preliminaries]
card_gt2P [in graphs.preliminaries]
card_gt1P [in graphs.preliminaries]
card_gtnP [in graphs.preliminaries]
card_le1 [in graphs.preliminaries]
card_ltnT [in graphs.preliminaries]
card_val [in graphs.skeleton]
card_del_edge [in graphs.digraph]
card1P [in graphs.preliminaries]
card12 [in graphs.preliminaries]
cases_without_edge [in graphs.excluded]
cast_proof [in graphs.finmap_plus]
CK4F_lens_rest [in graphs.extraction_def]
CK4F_remove_loops [in graphs.extraction_def]
CK4F_remove_edges [in graphs.extraction_def]
CK4F_split_cpM [in graphs.extraction_def]
CK4F_split_cpR [in graphs.extraction_def]
CK4F_split_cpL [in graphs.extraction_def]
CK4F_lens [in graphs.extraction_def]
CK4F_redirect [in graphs.extraction_def]
CK4F_one [in graphs.extraction_def]
CK4F_remove_component [in graphs.extraction_def]
CK4F_induced2 [in graphs.extraction_def]
CK4F_sub [in graphs.extraction_def]
CK4F_igraph [in graphs.extraction_def]
CK4F_component [in graphs.extraction_top]
cliqueP [in graphs.sgraph]
cliquePn [in graphs.sgraph]
clique1 [in graphs.sgraph]
clique2 [in graphs.sgraph]
cnvtop [in graphs.ptt]
cnvtst [in graphs.pttdom]
cnv_test [in graphs.pttdom]
cnv_inj [in graphs.pttdom]
cnv1 [in graphs.pttdom]
cnv2dot [in graphs.mgraph2]
cnv2I [in graphs.mgraph2]
cnv2par [in graphs.mgraph2]
codom_Some [in graphs.preliminaries]
collapse_bags [in graphs.cp_minor]
complete_irrefl [in graphs.sgraph]
complete_sym [in graphs.sgraph]
componentless_top [in graphs.extraction_iso]
componentless_one [in graphs.extraction_iso]
components_subset [in graphs.sgraph]
components_nonempty [in graphs.sgraph]
components_pblockP [in graphs.sgraph]
component_exchange [in graphs.sgraph]
component_of_components [in graphs.sgraph]
component_exit [in graphs.sgraph]
component_induced [in graphs.extraction_top]
component_hom [in graphs.skeleton]
component_can_e' [in graphs.skeleton]
component_can_e [in graphs.skeleton]
component_can_v' [in graphs.skeleton]
component_can_v [in graphs.skeleton]
comp_dom2_redirect [in graphs.extraction_iso]
comp_exit [in graphs.extraction_iso]
connectedI_clique [in graphs.excluded]
connectedP [in graphs.sgraph]
connectedTE [in graphs.sgraph]
connectedTI [in graphs.sgraph]
connectedU_edge [in graphs.sgraph]
connectedU_common_point [in graphs.sgraph]
connected_component_set [in graphs.extraction_def]
connected_induced [in graphs.extraction_def]
connected_interiorR [in graphs.sgraph]
connected_interior [in graphs.sgraph]
connected_add_node [in graphs.sgraph]
connected_component_of [in graphs.sgraph]
connected_one_component [in graphs.sgraph]
connected_in_components [in graphs.sgraph]
connected_card_gt1 [in graphs.sgraph]
connected_induced [in graphs.sgraph]
connected_in_subgraph [in graphs.sgraph]
connected_path [in graphs.sgraph]
connected_center [in graphs.sgraph]
connected_restrict_in [in graphs.sgraph]
connected_restrict [in graphs.sgraph]
connected_bag [in graphs.checkpoint]
connected_interval [in graphs.checkpoint]
connected_CP_closed [in graphs.checkpoint]
connected_cp_closed [in graphs.checkpoint]
connected_igraph [in graphs.skeleton]
connected_bgraph [in graphs.skeleton]
connected_skeleton [in graphs.skeleton]
connected_skeleton' [in graphs.skeleton]
connected0 [in graphs.sgraph]
connected1 [in graphs.sgraph]
connected2 [in graphs.sgraph]
connectorC_edge [in graphs.connectivity]
connector_dimatching [in graphs.connectivity]
connector_nodes [in graphs.connectivity]
connector_cat [in graphs.connectivity]
connector_sep [in graphs.connectivity]
connector_extend [in graphs.connectivity]
connector_eq [in graphs.connectivity]
connector_right [in graphs.connectivity]
connector_left [in graphs.connectivity]
connector_lst [in graphs.connectivity]
connector_fst [in graphs.connectivity]
connectRI [in graphs.sgraph]
connectUP [in graphs.preliminaries]
connect_range [in graphs.sgraph]
connect_restrict_case [in graphs.sgraph]
connect_img [in graphs.preliminaries]
connect_symI [in graphs.preliminaries]
connect_restrict_mono [in graphs.preliminaries]
connect_mono [in graphs.preliminaries]
consistentT [in graphs.mgraph]
consistentTT [in graphs.mgraph]
consistentU [in graphs.mgraph]
consistent_setD [in graphs.skeleton]
consistent_del1 [in graphs.mgraph]
const0_eq [in graphs.bounded]
contraNnot [in graphs.preliminaries]
contraPeq [in graphs.preliminaries]
contraPN [in graphs.preliminaries]
contraPneq [in graphs.preliminaries]
contraPT [in graphs.preliminaries]
contraTnot [in graphs.preliminaries]
contra_notT [in graphs.preliminaries]
cover_matching [in graphs.connectivity]
cpNI [in graphs.checkpoint]
cpN_trans [in graphs.checkpoint]
cpo_cp [in graphs.checkpoint]
cpo_max [in graphs.checkpoint]
cpo_min [in graphs.checkpoint]
cpo_order [in graphs.checkpoint]
cpo_antisym [in graphs.checkpoint]
cpo_total [in graphs.checkpoint]
cpo_trans [in graphs.checkpoint]
cpo_refl [in graphs.checkpoint]
cpP [in graphs.checkpoint]
cpPn [in graphs.checkpoint]
CProper1 [in graphs.structures]
CProper2 [in graphs.structures]
cpTI [in graphs.checkpoint]
cpxx [in graphs.checkpoint]
CP_tree_sinterval [in graphs.checkpoint]
cp_sub_interval [in graphs.checkpoint]
CP_tree_paths [in graphs.checkpoint]
CP_path [in graphs.checkpoint]
CP_base [in graphs.checkpoint]
CP_closed [in graphs.checkpoint]
CP_mono [in graphs.checkpoint]
CP_extensive [in graphs.checkpoint]
CP_set2 [in graphs.checkpoint]
cp_neighbours [in graphs.checkpoint]
cp_tighten [in graphs.checkpoint]
cp_tightenR [in graphs.checkpoint]
cp_widen [in graphs.checkpoint]
cp_widenR [in graphs.checkpoint]
cp_mid [in graphs.checkpoint]
cp_triangle [in graphs.checkpoint]
cp_sym [in graphs.checkpoint]
crK [in graphs.preliminaries]
D
decC [in graphs.skeleton]decE [in graphs.skeleton]
decomp_dom [in graphs.mgraph2_tw2]
decomp_cnv [in graphs.mgraph2_tw2]
decomp_dot2 [in graphs.mgraph2_tw2]
decomp_par2 [in graphs.mgraph2_tw2]
decomp_quot [in graphs.mgraph2_tw2]
decomp_clique [in graphs.treewidth]
decomp_link [in graphs.treewidth]
decomp_small [in graphs.treewidth]
decomp_iso [in graphs.treewidth]
decomp_iso2 [in graphs.skeleton]
del_edge_connector [in graphs.connectivity]
del_edge_lift_proof [in graphs.digraph]
del_edge_path_case [in graphs.digraph]
dhom_comp [in graphs.digraph]
dhom_id [in graphs.digraph]
diHall [in graphs.connectivity]
disconnectedE [in graphs.sgraph]
disjointE [in graphs.preliminaries]
disjointFl [in graphs.preliminaries]
disjointFr [in graphs.preliminaries]
disjointNI [in graphs.preliminaries]
disjointP [in graphs.preliminaries]
disjointsU [in graphs.preliminaries]
disjoints1 [in graphs.preliminaries]
disjointW [in graphs.preliminaries]
disjoint_transR [in graphs.preliminaries]
disjoint_exists [in graphs.preliminaries]
disjoint_part [in graphs.digraph]
disjoint3P [in graphs.preliminaries]
Diso' [in graphs.digraph]
Diso'' [in graphs.digraph]
domtst [in graphs.pttdom]
dom_tst [in graphs.pttdom]
dom_test [in graphs.pttdom]
dom2E [in graphs.mgraph2]
dotcnv [in graphs.pttdom]
dot_test [in graphs.pttdom]
dot1x [in graphs.pttdom]
dot2A [in graphs.mgraph2]
dot2Aflat [in graphs.mgraph2]
dot2one [in graphs.mgraph2]
dot2one' [in graphs.mgraph2]
dot2unit_l [in graphs.mgraph2]
dot2unit_r' [in graphs.mgraph2]
dot2unit_r [in graphs.mgraph2]
E
edgeless_bag [in graphs.extraction_def]edgeLP [in graphs.digraph]
edgep_proof [in graphs.digraph]
edgesP [in graphs.connectivity]
edges_at_iso [in graphs.mgraph]
edges_in1 [in graphs.mgraph]
edge_comp [in graphs.skeleton]
edge_setN [in graphs.skeleton]
edge_set_component [in graphs.skeleton]
edge_component [in graphs.skeleton]
edge_set_adj [in graphs.skeleton]
edge_diso' [in graphs.digraph]
edge_diso [in graphs.digraph]
edge_in_set [in graphs.mgraph]
edge_set1 [in graphs.mgraph]
elabel_iso' [in graphs.mgraph]
elabel_iso [in graphs.mgraph]
empty_uniqe [in graphs.preliminaries]
endpoint_iso' [in graphs.mgraph]
endpoint_iso [in graphs.mgraph]
enum_unit [in graphs.preliminaries]
enum_sum [in graphs.preliminaries]
eqb_negR [in graphs.preliminaries]
eqmodE [in graphs.finite_quotient]
equivalence_partition_gt1P [in graphs.preliminaries]
equivalence_rel_of_sym [in graphs.preliminaries]
equiv_of_sym [in graphs.preliminaries]
equiv_comp_pi [in graphs.finite_quotient]
equiv_compE [in graphs.finite_quotient]
equiv_of_fn [in graphs.equiv]
equiv_of_nn [in graphs.equiv]
equiv_of_ff [in graphs.equiv]
equiv_of_sub' [in graphs.equiv]
equiv_of_sub [in graphs.equiv]
equiv_of_transfer [in graphs.equiv]
equiv_ofE [in graphs.equiv]
equiv_of_class [in graphs.equiv]
equiv_clot_Kl [in graphs.mgraph]
eqvbN [in graphs.pttdom]
eqvbT [in graphs.pttdom]
eqvb_neq [in graphs.pttdom]
eqvb_par1 [in graphs.pttdom]
eqvb_transL [in graphs.structures]
eqvb_transR [in graphs.structures]
eqvb_trans [in graphs.structures]
eqvxx [in graphs.structures]
eqv_test_equiv [in graphs.pttdom]
eqv_update [in graphs.finmap_plus]
eqv_big [in graphs.structures]
eqv_bigl [in graphs.structures]
eqv_bigr [in graphs.structures]
eqv_big_bij [in graphs.structures]
eqv_map [in graphs.structures]
eqv_clot_LR [in graphs.equiv]
eqv_clot_injR [in graphs.equiv]
eqv_clot_injL [in graphs.equiv]
eqv_clot1E [in graphs.equiv]
eqv_clot_cat [in graphs.equiv]
eqv_clot_map_eq [in graphs.equiv]
eqv_clot_mapF [in graphs.equiv]
eqv_clot_map [in graphs.equiv]
eqv_clot_nothing' [in graphs.equiv]
eqv_clot_nothing [in graphs.equiv]
eqv_clot_eq [in graphs.equiv]
eqv_clot_subrel [in graphs.equiv]
eqv_clot_tl [in graphs.equiv]
eqv_clot_hd' [in graphs.equiv]
eqv_clot_hd [in graphs.equiv]
eqv_clot_trans [in graphs.equiv]
eqv_clot_iso [in graphs.equiv]
eqv_clot_map' [in graphs.equiv]
eqv_clot_subset [in graphs.equiv]
eqv_clot_pair [in graphs.equiv]
eqv_clotE [in graphs.equiv]
eqv_clot_union_rel [in graphs.mgraph]
eqv_clot_map_lr [in graphs.mgraph]
eqv'_sym [in graphs.pttdom]
eqv01 [in graphs.pttdom]
eqv10 [in graphs.structures]
eqv11 [in graphs.pttdom]
eq_connected [in graphs.sgraph]
eq_diso [in graphs.sgraph]
eq_unit [in graphs.structures]
eq_set1P [in graphs.preliminaries]
eq_quot_finMixin [in graphs.finite_quotient]
eq_equiv_class [in graphs.equiv]
eq_equiv [in graphs.equiv]
eq_eqv [in graphs.mgraph]
eval_TW2 [in graphs.mgraph2_tw2]
excluded_minor_TW2 [in graphs.excluded]
existsb_case [in graphs.preliminaries]
existsb_eq [in graphs.preliminaries]
existsPn [in graphs.preliminaries]
exists_inPn [in graphs.preliminaries]
ex_smallest [in graphs.preliminaries]
F
Fix_eq [in graphs.bounded]flesh_out [in graphs.skeleton]
foldr1_set_default [in graphs.preliminaries]
foo_eq [in graphs.bounded]
ForallE [in graphs.equiv]
forallPn [in graphs.preliminaries]
forall_inPn [in graphs.preliminaries]
forestI [in graphs.sgraph]
forestP [in graphs.sgraph]
forestT_unique [in graphs.sgraph]
forest_TW1 [in graphs.treewidth]
forest_vseparator [in graphs.treewidth]
forest3 [in graphs.sgraph]
fresh_bijE' [in graphs.finmap_plus]
fresh_bij' [in graphs.finmap_plus]
fresh_bijE [in graphs.finmap_plus]
fresh_bij [in graphs.finmap_plus]
fsetDDD [in graphs.finmap_plus]
fsetDEl [in graphs.finmap_plus]
fsetDl [in graphs.finmap_plus]
fsetD_bijE [in graphs.finmap_plus]
fsetD_bij_can_bwd [in graphs.finmap_plus]
fsetD_bij_can_fwd [in graphs.finmap_plus]
fsetD_bij_bwd_proof [in graphs.finmap_plus]
fsetD_bij_fwd_proof [in graphs.finmap_plus]
fsetUDU [in graphs.finmap_plus]
fsetU1_fun_can [in graphs.finmap_plus]
fset01 [in graphs.finmap_plus]
fset1D [in graphs.finmap_plus]
fset1UE [in graphs.finmap_plus]
fset1U0 [in graphs.finmap_plus]
fset2_maxn_neq [in graphs.finmap_plus]
fset2_cases [in graphs.finmap_plus]
fset2_inv [in graphs.finmap_plus]
fst_inj [in graphs.connectivity]
fst_lst_eq [in graphs.connectivity]
fst_idp [in graphs.connectivity]
fst_mem [in graphs.digraph]
fsvalK [in graphs.finmap_plus]
fsval_eqF [in graphs.finmap_plus]
fun_decompose [in graphs.preliminaries]
F_rec_narrow [in graphs.bounded]
G
get_edge [in graphs.extraction_def]graph_of_TW2 [in graphs.mgraph2_tw2]
graph_minor_TW2 [in graphs.extraction_top]
g2_A12 [in graphs.mgraph2]
g2_A12' [in graphs.mgraph2]
g2_A11 [in graphs.mgraph2]
g2_A10 [in graphs.mgraph2]
H
Hall [in graphs.connectivity]has_edge [in graphs.skeleton]
helly3_lifting [in graphs.helly]
hom_eqL [in graphs.mgraph2_tw2]
hom_skel [in graphs.skeleton]
hom_merge_union_K [in graphs.mgraph]
hom_union_merge_l [in graphs.mgraph]
hom_merge_merge [in graphs.mgraph]
hom_sym [in graphs.mgraph]
hom_comp [in graphs.mgraph]
hom_id [in graphs.mgraph]
hom2_sskel [in graphs.skeleton]
h_mergeE [in graphs.mgraph]
I
idxR [in graphs.sgraph]idx_swap [in graphs.sgraph]
idx_swap_aux [in graphs.sgraph]
idx_srev [in graphs.sgraph]
idx_nLR [in graphs.sgraph]
idx_inj [in graphs.sgraph]
idx_catR [in graphs.sgraph]
idx_catL [in graphs.sgraph]
idx_end [in graphs.sgraph]
idx_start [in graphs.sgraph]
idx_mem [in graphs.sgraph]
id_surj [in graphs.preliminaries]
id_bij [in graphs.preliminaries]
igraph_K4F_add_node [in graphs.cp_minor]
igraph_K4F [in graphs.cp_minor]
igraph_proof [in graphs.skeleton]
imfsetU [in graphs.finmap_plus]
imfset_bij_bwdE [in graphs.finmap_plus]
imfset_inv [in graphs.finmap_plus]
imfset_comp [in graphs.finmap_plus]
imfset_sep [in graphs.finmap_plus]
imfset0 [in graphs.finmap_plus]
imfset1 [in graphs.finmap_plus]
imfset1U [in graphs.finmap_plus]
imset_valT [in graphs.preliminaries]
imset_pre_val [in graphs.preliminaries]
incident_iso [in graphs.mgraph]
inD [in graphs.set_tac]
independent_walks [in graphs.connectivity]
independent_nodes [in graphs.digraph]
independent_sym [in graphs.digraph]
index_rev [in graphs.sgraph]
index_rcons [in graphs.sgraph]
induced_K4_free [in graphs.extraction_def]
induced_forest [in graphs.sgraph]
induced_path [in graphs.sgraph]
induced_sub [in graphs.sgraph]
induced_irrefl [in graphs.sgraph]
induced_sym [in graphs.sgraph]
induced_path [in graphs.digraph]
induced_sub [in graphs.mgraph]
induced_minor [in graphs.minor]
induced2_induced [in graphs.extraction_def]
induced2_compN_small [in graphs.extraction_top]
inD_debug [in graphs.set_tac]
infer_testE [in graphs.pttdom]
inj_imset [in graphs.preliminaries]
inj_card_onto_pred [in graphs.preliminaries]
inj_omap [in graphs.preliminaries]
inj_card_leq [in graphs.preliminaries]
inl_codom_inr [in graphs.preliminaries]
inl_inj [in graphs.preliminaries]
inl_eqE [in graphs.preliminaries]
inr_codom_inl [in graphs.preliminaries]
inr_inj [in graphs.preliminaries]
inr_eqE [in graphs.preliminaries]
interiorN [in graphs.digraph]
interiorW [in graphs.digraph]
interior_rev [in graphs.sgraph]
interior_idp [in graphs.sgraph]
interior_eq_nodes [in graphs.digraph]
interior_edgep [in graphs.digraph]
interior0E [in graphs.digraph]
intervalI_cp [in graphs.checkpoint]
intervalL [in graphs.checkpoint]
intervalR [in graphs.checkpoint]
interval_interval_cap [in graphs.checkpoint]
interval_edge_cp [in graphs.checkpoint]
interval_cp_cover [in graphs.checkpoint]
interval_bag_disj [in graphs.checkpoint]
interval_sym [in graphs.checkpoint]
interval_cp_edge_cover [in graphs.skeleton]
interval_bag_edge_cover [in graphs.skeleton]
interval_edges_disj_cp [in graphs.skeleton]
interval_bag_edges_disj [in graphs.skeleton]
interval_edges_sym [in graphs.skeleton]
in_component_of [in graphs.sgraph]
in_eqv_update [in graphs.finmap_plus]
in_fsep [in graphs.finmap_plus]
in_imfsetT [in graphs.finmap_plus]
in_tail [in graphs.digraph]
irredE [in graphs.digraph]
irredxx [in graphs.digraph]
irred_in_sinterval [in graphs.cp_minor]
irred_edge [in graphs.sgraph]
irred_rev [in graphs.sgraph]
irred_eq_nodes [in graphs.digraph]
irred_upath [in graphs.digraph]
irred_is_edge [in graphs.digraph]
irred_catE [in graphs.digraph]
irred_catI [in graphs.digraph]
irred_cat [in graphs.digraph]
irred_catD [in graphs.digraph]
irred_ind [in graphs.digraph]
irred_edgeR [in graphs.digraph]
irred_edgeL [in graphs.digraph]
irred_edge [in graphs.digraph]
irred_idp [in graphs.digraph]
irreflexive_restrict [in graphs.sgraph]
iso_connected [in graphs.sgraph]
iso_subgraph [in graphs.sgraph]
iso_disconnected_io [in graphs.extraction_top]
iso_pointxx [in graphs.skeleton]
iso_split_par2 [in graphs.extraction_iso]
iso_one [in graphs.extraction_iso]
iso_top [in graphs.extraction_iso]
iso_iso2' [in graphs.mgraph2]
iso_iso2 [in graphs.mgraph2]
iso_K4_free [in graphs.minor]
iso_strict_minor [in graphs.minor]
iso2_disconnected_component [in graphs.extraction_top]
iso2_GTG [in graphs.extraction_top]
iso2_TGT [in graphs.extraction_top]
iso2_subgraph_forT [in graphs.mgraph2]
isplitP [in graphs.digraph]
is_test_alt [in graphs.pttdom]
is_forestPn [in graphs.sgraph]
is_forestP [in graphs.sgraph]
J
join_disc [in graphs.sgraph]join_rel_irrefl [in graphs.sgraph]
join_rel_sym [in graphs.sgraph]
join_width [in graphs.treewidth]
join_decomp [in graphs.treewidth]
join_is_forest [in graphs.treewidth]
K
kernelP [in graphs.finite_quotient]kernel_equivalence [in graphs.finite_quotient]
kernel_eqv_clot [in graphs.equiv]
Km_width [in graphs.treewidth]
Km_bag [in graphs.treewidth]
Kn_clique [in graphs.minor]
Konig [in graphs.connectivity]
K3_free_forest [in graphs.minor]
K4_free_add_edge_sep_size2 [in graphs.excluded]
K4_of_vseparators [in graphs.excluded]
K4_of_paths [in graphs.excluded]
L
last_rev_belast [in graphs.sgraph]last_belast_eq [in graphs.preliminaries]
last_take [in graphs.preliminaries]
lens_components [in graphs.extraction_def]
lens_sinterval [in graphs.extraction_def]
lens_io_set [in graphs.extraction_def]
leq_subn [in graphs.preliminaries]
lift_Path [in graphs.sgraph]
lift_Path_on [in graphs.sgraph]
lift_equiv [in graphs.preliminaries]
lift_path [in graphs.preliminaries]
lift_upath [in graphs.digraph]
lift_upath_on [in graphs.digraph]
lift_pathp [in graphs.digraph]
lift_pathp_on [in graphs.digraph]
line_of_walk [in graphs.mgraph]
link_rel_sep2 [in graphs.cp_minor]
link_is_forest [in graphs.treewidth]
link_has_None [in graphs.treewidth]
link_unique_None [in graphs.treewidth]
link_bypass [in graphs.treewidth]
link_unique_lift [in graphs.treewidth]
link_path_cp [in graphs.checkpoint]
link_seq_cp [in graphs.checkpoint]
link_avoid [in graphs.checkpoint]
link_irrefl [in graphs.checkpoint]
link_sym [in graphs.checkpoint]
lst_inj [in graphs.connectivity]
lst_idp [in graphs.connectivity]
lst_mem [in graphs.digraph]
ltn_subn [in graphs.helly]
M
map_equivE [in graphs.finite_quotient]map_equiv_class [in graphs.finite_quotient]
map_pairs_id [in graphs.mgraph]
map_map_pairs [in graphs.mgraph]
map_of_total [in graphs.minor]
matching_cover_map [in graphs.connectivity]
matching_of_dimatching [in graphs.connectivity]
maxnP [in graphs.preliminaries]
maxn_fsetD [in graphs.finmap_plus]
maxn_fset2 [in graphs.finmap_plus]
maxn_eq [in graphs.preliminaries]
max_mono [in graphs.preliminaries]
measure_lens_rest [in graphs.extraction_def]
measure_remove_edges [in graphs.extraction_def]
measure_split_cpM [in graphs.extraction_def]
measure_split_cpR [in graphs.extraction_def]
measure_split_cpL [in graphs.extraction_def]
measure_lens [in graphs.extraction_def]
measure_redirect [in graphs.extraction_def]
measure_remove_component [in graphs.extraction_def]
measure_igraph [in graphs.extraction_def]
measure_node [in graphs.extraction_def]
measure_subgraph [in graphs.extraction_def]
measure_io [in graphs.extraction_def]
measure_card [in graphs.extraction_def]
memKset [in graphs.preliminaries]
mem_component [in graphs.sgraph]
mem_prev [in graphs.sgraph]
mem_maxn [in graphs.finmap_plus]
mem_cpl [in graphs.checkpoint]
mem_cover [in graphs.preliminaries]
mem_preim [in graphs.preliminaries]
mem_catD [in graphs.preliminaries]
mem_tail [in graphs.preliminaries]
mem_del_edge_liftS [in graphs.digraph]
mem_eq_nodes [in graphs.digraph]
mem_pcat_edgeR [in graphs.digraph]
mem_pcat_edgeL [in graphs.digraph]
mem_edgep [in graphs.digraph]
mem_idp [in graphs.digraph]
mem_pcat [in graphs.digraph]
mem_pcatT [in graphs.digraph]
mem_path [in graphs.digraph]
mem_bigcup [in graphs.minor]
Menger [in graphs.connectivity]
merge_unionE [in graphs.finite_quotient]
merge_union_bwd_hom [in graphs.finite_quotient]
merge_union_fwd_hom [in graphs.finite_quotient]
merge_union_can' [in graphs.finite_quotient]
merge_union_can [in graphs.finite_quotient]
merge_disjoint_union_can' [in graphs.finite_quotient]
merge_disjoint_union_can [in graphs.finite_quotient]
merge_union_bwdP [in graphs.finite_quotient]
merge_subgraph_par [in graphs.extraction_iso]
merge_subgraph_dot [in graphs.extraction_iso]
merge_subgraph_isoE [in graphs.mgraph]
merge_subgraph_hom [in graphs.mgraph]
merge_union_KE [in graphs.mgraph]
merge_add_vlabelE [in graphs.mgraph]
merge_add_vlabel [in graphs.mgraph]
merge_add_edgeE [in graphs.mgraph]
merge_add_edge [in graphs.mgraph]
merge_merge_seqE [in graphs.mgraph]
merge_nothingE [in graphs.mgraph]
merge_same'E [in graphs.mgraph]
merge_same'_hom [in graphs.mgraph]
merge_isoE [in graphs.mgraph]
merge_hom [in graphs.mgraph]
merge_mergeE [in graphs.mgraph]
merge_merge [in graphs.mgraph]
merge_nothing'E [in graphs.mgraph]
merge_nothing' [in graphs.mgraph]
merge_surjE [in graphs.mgraph]
merge_surj [in graphs.mgraph]
merge_union_K_l [in graphs.mgraph2]
merge_merge [in graphs.mgraph2]
merge_nothing [in graphs.mgraph2]
merge_same' [in graphs.mgraph2]
merge_same [in graphs.mgraph2]
merge_iso2 [in graphs.mgraph2]
merge2_add_vlabel [in graphs.mgraph2]
merge2_add_edge [in graphs.mgraph2]
merge2_merge [in graphs.mgraph2]
merge2_nothing [in graphs.mgraph2]
merge2_same' [in graphs.mgraph2]
merge2_same [in graphs.mgraph2]
merge2_surj [in graphs.mgraph2]
merge2_iso2 [in graphs.mgraph2]
minimal_separation [in graphs.connectivity]
minorRE [in graphs.minor]
minor_exclusion_2p [in graphs.extraction_top]
minor_rmapI [in graphs.minor]
minor_with [in graphs.minor]
minor_induced_add_node [in graphs.minor]
minor_K4_free [in graphs.minor]
minor_of_clique [in graphs.minor]
minor_trans [in graphs.minor]
minor_map_comp [in graphs.minor]
minor_rmap_comp [in graphs.minor]
minor_of_rmap [in graphs.minor]
minor_of_map [in graphs.minor]
minor_rmap_map [in graphs.minor]
minor_map_rmap [in graphs.minor]
min_vcover_matching [in graphs.connectivity]
min_max_cover [in graphs.connectivity]
monUl [in graphs.structures]
N
nat_size_ind [in graphs.preliminaries]ncpP [in graphs.checkpoint]
ncp_interval [in graphs.checkpoint]
ncp_bag [in graphs.checkpoint]
ncp_CP [in graphs.checkpoint]
ncp0 [in graphs.checkpoint]
neighborC [in graphs.sgraph]
neighborP [in graphs.sgraph]
neighborUl [in graphs.sgraph]
neighborUr [in graphs.sgraph]
neighborW [in graphs.sgraph]
neighbor_interiorL [in graphs.sgraph]
neighbor_split [in graphs.sgraph]
neighbor_add_edge [in graphs.sgraph]
neighbor_del_edge1 [in graphs.sgraph]
neighbor_del_edge2 [in graphs.sgraph]
neighbor_del_edgeR [in graphs.sgraph]
neighbor_add_edgeC [in graphs.sgraph]
neighbor_connected [in graphs.sgraph]
nodesE [in graphs.digraph]
nodes_prev [in graphs.sgraph]
nodes_pcat [in graphs.digraph]
nodes_eqE [in graphs.digraph]
non_forerst_K3 [in graphs.minor]
notinD [in graphs.set_tac]
notinD_debug [in graphs.set_tac]
notin_tail [in graphs.preliminaries]
no_K4_smallest_vseparator [in graphs.excluded]
nt_correct [in graphs.pttdom]
O
one_test [in graphs.pttdom]option_sum_unit [in graphs.bij]
orb_sum [in graphs.preliminaries]
ord_fresh [in graphs.preliminaries]
ord_size_enum [in graphs.preliminaries]
ord3P [in graphs.helly]
P
paratst [in graphs.pttdom]pardot [in graphs.pttdom]
partition_components [in graphs.sgraph]
partition_big [in graphs.structures]
partition0 [in graphs.sgraph]
partopx [in graphs.ptt]
partst [in graphs.pttdom]
parxtop [in graphs.ptt]
par_nontest [in graphs.pttdom]
par_tst_cnv [in graphs.pttdom]
par_test [in graphs.pttdom]
par_component [in graphs.extraction_top]
par1tst [in graphs.pttdom]
par2A [in graphs.mgraph2]
par2C [in graphs.mgraph2]
par2dot [in graphs.mgraph2]
par2edgeunit [in graphs.mgraph2]
par2oneone [in graphs.mgraph2]
par2top [in graphs.mgraph2]
par2unitunit [in graphs.mgraph2]
pathpP [in graphs.digraph]
pathpW [in graphs.digraph]
pathpxx [in graphs.digraph]
pathp_rev [in graphs.sgraph]
pathp_shorten [in graphs.digraph]
pathp_rcons [in graphs.digraph]
pathp_cons [in graphs.digraph]
pathp_nil [in graphs.digraph]
pathp_concat [in graphs.digraph]
pathp_cat [in graphs.digraph]
pathp_last [in graphs.digraph]
PathRP [in graphs.sgraph]
pathS_eta [in graphs.digraph]
path_neighborR [in graphs.sgraph]
path_neighborL [in graphs.sgraph]
path_in_connected [in graphs.sgraph]
Path_from_induced [in graphs.sgraph]
Path_to_induced [in graphs.sgraph]
path_to_induced [in graphs.sgraph]
path_srev [in graphs.sgraph]
path_return [in graphs.treewidth]
path_restrict [in graphs.preliminaries]
Path_from_induced [in graphs.digraph]
Path_to_induced [in graphs.digraph]
path_to_induced [in graphs.digraph]
Path_connect [in graphs.digraph]
path_closed [in graphs.digraph]
Path_ind [in graphs.digraph]
path_begin [in graphs.digraph]
path_end [in graphs.digraph]
path_last [in graphs.digraph]
pblock_eqvE [in graphs.preliminaries]
pcatA [in graphs.digraph]
pcatSE [in graphs.digraph]
pcat_subset [in graphs.digraph]
pcat_idR [in graphs.digraph]
pcat_idL [in graphs.digraph]
perm_index_enum [in graphs.bij]
perm_big [in graphs.structures]
picksP [in graphs.preliminaries]
piK [in graphs.finite_quotient]
piK' [in graphs.finite_quotient]
pimsetP [in graphs.preliminaries]
pimset_card [in graphs.preliminaries]
piP [in graphs.finite_quotient]
pi_hom [in graphs.skeleton]
pi_surj [in graphs.finite_quotient]
ppsplitP [in graphs.digraph]
predIpcatR [in graphs.excluded]
preim_omap_None [in graphs.preliminaries]
preim_omap_Some [in graphs.preliminaries]
prevK [in graphs.sgraph]
prev_edge [in graphs.sgraph]
prev_edge_proof [in graphs.sgraph]
prev_irred [in graphs.sgraph]
prev_cat [in graphs.sgraph]
prev_inj [in graphs.sgraph]
project_path [in graphs.preliminaries]
propers_ind [in graphs.preliminaries]
proper_separation_symmetry [in graphs.connectivity]
proper_vseparator [in graphs.connectivity]
proper_ind [in graphs.preliminaries]
psplitP [in graphs.digraph]
Q
quot_union_KE [in graphs.finite_quotient]quot_idE [in graphs.finite_quotient]
quot_quotE [in graphs.finite_quotient]
quot_bijE' [in graphs.finite_quotient]
quot_bijE [in graphs.finite_quotient]
quot_kernelE' [in graphs.finite_quotient]
quot_kernelE [in graphs.finite_quotient]
quot_kernel_can' [in graphs.finite_quotient]
quot_kernel_can [in graphs.finite_quotient]
quot_sameE' [in graphs.finite_quotient]
quot_sameE [in graphs.finite_quotient]
quot_fun_can [in graphs.finite_quotient]
quot.eqquotP [in graphs.finite_quotient]
quot.reprK [in graphs.finite_quotient]
R
rcons_pathp [in graphs.digraph]rec_bag [in graphs.extraction_def]
redirect_output_proof [in graphs.extraction_def]
redirect_consistent [in graphs.extraction_def]
redirect_proof1 [in graphs.extraction_def]
reduce_shuffle [in graphs.pttdom]
reindex [in graphs.structures]
reindex_onto [in graphs.structures]
relabel_edge [in graphs.mgraph2]
relabel_two [in graphs.mgraph2]
relabel_unit [in graphs.mgraph2]
relabel_add_edge [in graphs.mgraph2]
relabel_merge [in graphs.mgraph2]
relabel_union [in graphs.mgraph2]
relabel2_var [in graphs.mgraph2]
relabel2_top [in graphs.mgraph2]
relabel2_one [in graphs.mgraph2]
relabel2_dom [in graphs.mgraph2]
relabel2_cnv [in graphs.mgraph2]
relabel2_par [in graphs.mgraph2]
relabel2_dot [in graphs.mgraph2]
relU_sym' [in graphs.preliminaries]
rel_of_pairs_mapE [in graphs.equiv]
rel_of_pairs_map_eq [in graphs.equiv]
rel_of_pairs_mono [in graphs.equiv]
rel0_sym [in graphs.preliminaries]
rel0_irrefl [in graphs.preliminaries]
remove_component [in graphs.sgraph]
remove_edges_restrict [in graphs.skeleton]
remove_edges_cross [in graphs.skeleton]
remove_edges_connected [in graphs.skeleton]
remove_loops [in graphs.skeleton]
remove_edge_add [in graphs.skeleton]
remove_edges_sub [in graphs.mgraph]
rename_width [in graphs.treewidth]
rename_decomp [in graphs.treewidth]
rename_sdecomp [in graphs.minor]
restrictE [in graphs.preliminaries]
restrict_upath [in graphs.sgraph]
restrict_path [in graphs.preliminaries]
restrict_mono [in graphs.preliminaries]
rev_upath [in graphs.sgraph]
rev_inj [in graphs.preliminaries]
rmap_disjE [in graphs.excluded]
rmap_add_edge_sym [in graphs.minor]
rwT [in graphs.pttdom]
S
same_component [in graphs.sgraph]sconnect_sym [in graphs.sgraph]
sc_eq [in graphs.preliminaries]
sc_sym [in graphs.preliminaries]
sdecomp_sskel [in graphs.mgraph2_tw2]
sdecomp_tree_subrel [in graphs.treewidth]
sdecomp_subrel [in graphs.treewidth]
sedge_equiv_in [in graphs.sgraph]
sedge_in_equiv [in graphs.sgraph]
sedge_equiv [in graphs.sgraph]
separatesI [in graphs.connectivity]
separatesNE [in graphs.connectivity]
separatesNeq [in graphs.connectivity]
separatesP [in graphs.connectivity]
separates0P [in graphs.connectivity]
separate_nonadjacent [in graphs.connectivity]
separation_K4side [in graphs.excluded]
separation_connected_same_component [in graphs.connectivity]
separation_sym [in graphs.connectivity]
separation_separates [in graphs.connectivity]
separation_decomp [in graphs.treewidth]
separatorI [in graphs.connectivity]
separatorP [in graphs.connectivity]
separatorPn [in graphs.connectivity]
separator_min [in graphs.connectivity]
separator_cap [in graphs.connectivity]
sepatates_cp [in graphs.cp_minor]
sep_inL [in graphs.connectivity]
sep_inR [in graphs.connectivity]
setIPn [in graphs.set_tac]
setN01E [in graphs.preliminaries]
setT_bij_hom [in graphs.mgraph]
setUPn [in graphs.set_tac]
setU_dec [in graphs.finite_quotient]
setU1_neq [in graphs.preliminaries]
setU1_mem [in graphs.preliminaries]
set_pred0 [in graphs.cp_minor]
set_tac_subIl [in graphs.set_tac]
set_tac_subIr [in graphs.set_tac]
set_tac_subUl [in graphs.set_tac]
set1_inj [in graphs.preliminaries]
set10 [in graphs.preliminaries]
set2C [in graphs.preliminaries]
sg_edgeNeq [in graphs.sgraph]
sintervalP2 [in graphs.checkpoint]
sinterval_cp_cover [in graphs.checkpoint]
sinterval_bag_cover [in graphs.checkpoint]
sinterval_components [in graphs.checkpoint]
sinterval_connectedL [in graphs.checkpoint]
sinterval_connectL [in graphs.checkpoint]
sinterval_noedge_cp [in graphs.checkpoint]
sinterval_disj_cp [in graphs.checkpoint]
sinterval_outside [in graphs.checkpoint]
sinterval_exit [in graphs.checkpoint]
sinterval_sub [in graphs.checkpoint]
sinterval_bounds [in graphs.checkpoint]
sinterval_sym [in graphs.checkpoint]
skelP [in graphs.skeleton]
skel_K4_free [in graphs.mgraph2_tw2]
skel_union_join [in graphs.mgraph2_tw2]
skel_sub [in graphs.skeleton]
sk_rel_mergeE [in graphs.skeleton]
sk_rel_irrefl [in graphs.skeleton]
sk_rel_sym [in graphs.skeleton]
small_clique [in graphs.sgraph]
small_K_free [in graphs.minor]
Some_eqE [in graphs.preliminaries]
splitL [in graphs.digraph]
splitR [in graphs.digraph]
split_K4_nontrivial [in graphs.extraction_def]
split_at_last [in graphs.sgraph]
split_io_loop [in graphs.extraction_iso]
split_io_edge_lens [in graphs.extraction_iso]
split_io_edge [in graphs.extraction_iso]
split_io_edge_aux [in graphs.extraction_iso]
split_component [in graphs.extraction_iso]
split_cp [in graphs.extraction_iso]
split_pip [in graphs.extraction_iso]
split_at_first [in graphs.digraph]
split_at_first_aux [in graphs.digraph]
srestrict_sym [in graphs.sgraph]
srevK [in graphs.sgraph]
srev_nodes [in graphs.sgraph]
srev_rcons [in graphs.sgraph]
sskeleton_add [in graphs.extraction_def]
sskeleton_remove_io [in graphs.skeleton]
sskeleton_adjacent [in graphs.skeleton]
sskeleton_subgraph_for [in graphs.skeleton]
sskelP [in graphs.skeleton]
sskel_K4_free [in graphs.mgraph2_tw2]
ssplit_K4_nontrivial [in graphs.cp_minor]
ssplit_disconnected [in graphs.sgraph]
strict_is_minor [in graphs.minor]
subcp [in graphs.checkpoint]
subgraph_sub [in graphs.mgraph]
subgraph_for_iso [in graphs.mgraph2]
subgraph_K4_free [in graphs.minor]
subrelP [in graphs.preliminaries]
subrel_restrict [in graphs.preliminaries]
subrel_pathp [in graphs.digraph]
subsetIlP1 [in graphs.excluded]
subset_seqL [in graphs.preliminaries]
subset_seqR [in graphs.preliminaries]
subset_cons [in graphs.preliminaries]
subset_tl [in graphs.equiv]
subset_catR [in graphs.equiv]
subset_catL [in graphs.equiv]
subset_pcatR [in graphs.digraph]
subset_pcatL [in graphs.digraph]
subtree_cut [in graphs.helly]
sub_connector [in graphs.connectivity]
sub_forest [in graphs.sgraph]
sub_inr [in graphs.treewidth]
sub_inl [in graphs.treewidth]
sub_equiv_of [in graphs.preliminaries]
sub_restrict_connect [in graphs.preliminaries]
sub_trans [in graphs.preliminaries]
sub_connect [in graphs.preliminaries]
sub_in11W [in graphs.preliminaries]
sub_val_eq [in graphs.preliminaries]
sub_sub [in graphs.skeleton]
sub_pointxx [in graphs.skeleton]
sub_minor [in graphs.minor]
sumUx [in graphs.bij]
sumxU [in graphs.bij]
sum_option_r [in graphs.bij]
sum_option_l [in graphs.bij]
surj_repr_pi [in graphs.finite_quotient]
svseparator_uniq [in graphs.connectivity]
svseparator_neighbours [in graphs.connectivity]
svseparator_connected [in graphs.connectivity]
symmetric_restrict_sedge [in graphs.sgraph]
symmetric_restrict [in graphs.preliminaries]
T
tailW [in graphs.digraph]take_find [in graphs.preliminaries]
term_of_eq [in graphs.extraction_def]
term_of_rec_eq [in graphs.extraction_def]
term_of_iso' [in graphs.extraction_top]
term_of_eq' [in graphs.extraction_top]
term_of_rec_eq' [in graphs.extraction_top]
term_of_iso [in graphs.extraction_iso]
theta [in graphs.connectivity]
theta_vertices [in graphs.connectivity]
the_uPathP [in graphs.checkpoint]
the_uPath_proof [in graphs.checkpoint]
three_way_split [in graphs.sgraph]
tm_eqv_equivalence [in graphs.pttdom]
tm_eqv_equivalence [in graphs.ptt]
tnth_cons [in graphs.preliminaries]
tnth_map_in [in graphs.preliminaries]
tnth_uniq [in graphs.preliminaries]
topL [in graphs.mgraph2]
topR [in graphs.mgraph2]
treeI [in graphs.sgraph]
treewidth_K_free [in graphs.minor]
tree_helly [in graphs.helly]
tree_I3 [in graphs.helly]
tree_connectI [in graphs.helly]
trivial_connector [in graphs.connectivity]
trivIset_components [in graphs.sgraph]
trivIset3 [in graphs.preliminaries]
tstpar [in graphs.pttdom]
tstpar1 [in graphs.pttdom]
tst_dotU [in graphs.pttdom]
tst_dotC [in graphs.pttdom]
tst_dotA [in graphs.pttdom]
tst_dot_eqv [in graphs.pttdom]
two_graph_swap [in graphs.mgraph]
TW1_forest [in graphs.minor]
TW2_of_K4F [in graphs.excluded]
TW2_K4_free [in graphs.minor]
U
uncycle [in graphs.digraph]union_bij_proofR [in graphs.finite_quotient]
union_bij_proofL [in graphs.finite_quotient]
union_quot_rEl [in graphs.finite_quotient]
union_quot_rEr [in graphs.finite_quotient]
union_quot_lE' [in graphs.finite_quotient]
union_quot_lEr [in graphs.finite_quotient]
union_quot_lEl [in graphs.finite_quotient]
union_equiv_l_class [in graphs.finite_quotient]
union_merge_rEl [in graphs.mgraph]
union_merge_rEr [in graphs.mgraph]
union_merge_r [in graphs.mgraph]
union_merge_lE' [in graphs.mgraph]
union_merge_lEr [in graphs.mgraph]
union_merge_lEl [in graphs.mgraph]
union_equiv_l_eqv_clot [in graphs.mgraph]
union_add_vlabel_r [in graphs.mgraph]
union_add_vlabel_l [in graphs.mgraph]
union_add_edge_r [in graphs.mgraph]
union_add_edge_l [in graphs.mgraph]
union_A [in graphs.mgraph]
union_C [in graphs.mgraph]
unique_forestT [in graphs.sgraph]
uniq_take [in graphs.preliminaries]
uPathP [in graphs.digraph]
upathP [in graphs.digraph]
upathPR [in graphs.sgraph]
uPathRP [in graphs.sgraph]
upathW [in graphs.digraph]
upathWW [in graphs.digraph]
upath_sym [in graphs.sgraph]
upath_irred [in graphs.digraph]
UPath_tupleK [in graphs.digraph]
upath_size [in graphs.digraph]
upath_nil [in graphs.digraph]
upath_consE [in graphs.digraph]
upath_cons [in graphs.digraph]
upath_uniq [in graphs.digraph]
update_fx [in graphs.preliminaries]
update_same [in graphs.preliminaries]
update_eq [in graphs.preliminaries]
update_neq [in graphs.preliminaries]
usplitP [in graphs.digraph]
V
valK' [in graphs.preliminaries]valK'' [in graphs.preliminaries]
vcoverP [in graphs.connectivity]
vlabel_iso' [in graphs.mgraph]
vlabel_iso [in graphs.mgraph]
void_enumP [in graphs.preliminaries]
void_pcancel [in graphs.preliminaries]
void_eqP [in graphs.preliminaries]
vseparatorNE [in graphs.connectivity]
vseparatorP [in graphs.connectivity]
vseparator_separation [in graphs.connectivity]
W
walk_of_line [in graphs.mgraph]wf_propers [in graphs.preliminaries]
wf_proper [in graphs.preliminaries]
wf_leq [in graphs.preliminaries]
width_bound [in graphs.sgraph]
width_link [in graphs.treewidth]
width_minor [in graphs.minor]
Constructor Index
B
Bij [in graphs.bij]D
Diso [in graphs.digraph]Dis3In1 [in graphs.preliminaries]
Dis3In2 [in graphs.preliminaries]
Dis3In3 [in graphs.preliminaries]
Dis3Notin [in graphs.preliminaries]
F
Forest [in graphs.sgraph]G
Graph [in graphs.mgraph]Graph2 [in graphs.mgraph2]
H
Hom [in graphs.mgraph]I
Iso [in graphs.mgraph]Iso2 [in graphs.mgraph2]
ISplit [in graphs.digraph]
L
Labels [in graphs.structures]M
MaxnL [in graphs.preliminaries]MaxnR [in graphs.preliminaries]
merge_union_bwdR [in graphs.finite_quotient]
merge_union_bwdL [in graphs.finite_quotient]
MonoidLaws [in graphs.structures]
N
Nopicks [in graphs.preliminaries]nt_conn [in graphs.pttdom]
nt_test [in graphs.pttdom]
P
Picks [in graphs.preliminaries]PiSpec [in graphs.finite_quotient]
PPSplit [in graphs.digraph]
PSplit [in graphs.digraph]
R
RelType [in graphs.digraph]S
SDecomp [in graphs.treewidth]SetBox [in graphs.set_tac]
Setoid [in graphs.structures]
SGraph [in graphs.sgraph]
T
Test [in graphs.pttdom]tm_var [in graphs.pttdom]
tm_one [in graphs.pttdom]
tm_dom [in graphs.pttdom]
tm_cnv [in graphs.pttdom]
tm_par [in graphs.pttdom]
tm_dot [in graphs.pttdom]
tm_var [in graphs.ptt]
tm_top [in graphs.ptt]
tm_one [in graphs.ptt]
tm_dom [in graphs.ptt]
tm_cnv [in graphs.ptt]
tm_par [in graphs.ptt]
tm_dot [in graphs.ptt]
U
USplit [in graphs.digraph]Axiom Index
A
admitted_case [in graphs.preliminaries]Q
QUOT.eqquotP [in graphs.finite_quotient]QUOT.pi [in graphs.finite_quotient]
QUOT.quot [in graphs.finite_quotient]
QUOT.repr [in graphs.finite_quotient]
QUOT.reprK [in graphs.finite_quotient]
Inductive Index
D
disjoint3_cases [in graphs.preliminaries]I
isplit [in graphs.digraph]M
maxn_cases [in graphs.preliminaries]merge_union_bwd_spec [in graphs.finite_quotient]
N
nterm [in graphs.pttdom]P
pathp_split [in graphs.digraph]picks_spec [in graphs.preliminaries]
pi_spec [in graphs.finite_quotient]
psplit [in graphs.digraph]
T
term [in graphs.pttdom]term [in graphs.ptt]
U
usplit [in graphs.digraph]V
void [in graphs.preliminaries]Projection Index
A
A10 [in graphs.pttdom]A10_ [in graphs.ptt]
A11 [in graphs.ptt]
A12 [in graphs.ptt]
A13 [in graphs.pttdom]
A14 [in graphs.pttdom]
B
bijK [in graphs.bij]bijK' [in graphs.bij]
bij_bwd [in graphs.bij]
bij_fwd [in graphs.bij]
C
car [in graphs.structures]cnv [in graphs.pttdom]
cnvdot [in graphs.pttdom]
cnvdot_ [in graphs.ptt]
cnvI [in graphs.pttdom]
cnvI_ [in graphs.ptt]
cnvpar [in graphs.pttdom]
cnvpar_ [in graphs.ptt]
cnv_eqv [in graphs.pttdom]
cnv_eqv_ [in graphs.ptt]
conn_disjoint [in graphs.connectivity]
conn_end [in graphs.connectivity]
conn_begin [in graphs.connectivity]
conn_irred [in graphs.connectivity]
D
diso_hom' [in graphs.digraph]diso_hom [in graphs.digraph]
diso_v [in graphs.digraph]
dom [in graphs.pttdom]
domE [in graphs.ptt]
dom_eqv [in graphs.pttdom]
dot [in graphs.pttdom]
dotA [in graphs.pttdom]
dotA_ [in graphs.ptt]
dotx1 [in graphs.pttdom]
dotx1_ [in graphs.ptt]
dot_eqv [in graphs.pttdom]
dot_eqv_ [in graphs.ptt]
E
edge [in graphs.mgraph]edge_rel [in graphs.digraph]
elabel [in graphs.mgraph]
elabel_hom [in graphs.mgraph]
elem_of [in graphs.pttdom]
endpoint [in graphs.mgraph]
endpoint_hom [in graphs.mgraph]
Eqv [in graphs.structures]
eqv [in graphs.structures]
eqv' [in graphs.structures]
Eqv'_sym [in graphs.structures]
eqv01 [in graphs.structures]
eqv11 [in graphs.structures]
F
forest_is_forest [in graphs.sgraph]G
graph_of [in graphs.mgraph2]I
input [in graphs.mgraph2]iso_hom [in graphs.mgraph]
iso_d [in graphs.mgraph]
iso_e [in graphs.mgraph]
iso_v [in graphs.mgraph]
iso2_output [in graphs.mgraph2]
iso2_input [in graphs.mgraph2]
iso2_iso [in graphs.mgraph2]
ival [in graphs.digraph]
ivalP [in graphs.digraph]
L
le [in graphs.structures]lv [in graphs.structures]
lv_monoid [in graphs.structures]
M
monA [in graphs.structures]monC [in graphs.structures]
monU [in graphs.structures]
mon_eqv [in graphs.structures]
mon0 [in graphs.structures]
mon2 [in graphs.structures]
O
one [in graphs.pttdom]ops [in graphs.pttdom]
ops [in graphs.ptt]
output [in graphs.mgraph2]
P
par [in graphs.pttdom]parA [in graphs.pttdom]
parA_ [in graphs.ptt]
parC [in graphs.pttdom]
parC_ [in graphs.ptt]
par_eqv [in graphs.pttdom]
par_eqv_ [in graphs.ptt]
par11 [in graphs.pttdom]
par11_ [in graphs.ptt]
pval [in graphs.digraph]
R
rel_car [in graphs.digraph]S
sbag_conn [in graphs.treewidth]sbag_edge [in graphs.treewidth]
sbag_cover [in graphs.treewidth]
sedge [in graphs.sgraph]
setBoxed [in graphs.set_tac]
setoid_of_ops [in graphs.pttdom]
sgraph_of_forest [in graphs.sgraph]
sg_irrefl' [in graphs.sgraph]
sg_sym' [in graphs.sgraph]
svertex [in graphs.sgraph]
T
testE [in graphs.pttdom]top [in graphs.pttdom]
U
uval [in graphs.digraph]V
vertex [in graphs.mgraph]vlabel [in graphs.mgraph]
vlabel_hom [in graphs.mgraph]
Section Index
A
AddEdge [in graphs.treewidth]AddNode [in graphs.sgraph]
B
b [in graphs.finite_quotient]Bij [in graphs.finmap_plus]
BijCast [in graphs.finmap_plus]
BijD1 [in graphs.bij]
BijT [in graphs.bij]
Bounded [in graphs.bounded]
C
CheckpointOrder [in graphs.checkpoint]CheckPoints [in graphs.checkpoint]
CheckpointsAndMinors [in graphs.cp_minor]
Cliques [in graphs.sgraph]
CProper [in graphs.structures]
D
DecompTheory [in graphs.treewidth]DelEdge [in graphs.digraph]
derived [in graphs.pttdom]
derived [in graphs.ptt]
DiGraphTheory [in graphs.digraph]
DiGraphTheory.Fixed [in graphs.digraph]
DiPathTheory [in graphs.digraph]
DiPathTheory.Finite [in graphs.digraph]
DiPathTheory.IPath [in graphs.digraph]
Disjoint3 [in graphs.preliminaries]
E
Equivalence [in graphs.preliminaries]eqv_inj [in graphs.equiv]
ExtractionDef [in graphs.extraction_def]
ExtractionDef.SplitCP [in graphs.extraction_def]
ExtractionIso [in graphs.extraction_iso]
ExtractionTop [in graphs.extraction_top]
F
FinEncodingModuloRel [in graphs.finite_quotient]Foldr1 [in graphs.preliminaries]
Forests [in graphs.sgraph]
Fresh2Bij [in graphs.finmap_plus]
fsetD_bij [in graphs.finmap_plus]
FsetU1Fun [in graphs.finmap_plus]
H
h [in graphs.mgraph2]I
InducedSubgraph [in graphs.sgraph]InducedSubgraph [in graphs.digraph]
Interior [in graphs.digraph]
J
JoinSG [in graphs.sgraph]JoinT [in graphs.treewidth]
L
Link [in graphs.treewidth]M
map_equiv [in graphs.finite_quotient]Max [in graphs.bounded]
MergeSubgraph [in graphs.mgraph]
N
Neighbor [in graphs.sgraph]P
Pack [in graphs.digraph]Packaged [in graphs.sgraph]
Packaged.Prev [in graphs.sgraph]
Pack.PathDef [in graphs.digraph]
PathIndexing [in graphs.sgraph]
PathIndexing.IDX [in graphs.sgraph]
PathOps [in graphs.digraph]
PathP [in graphs.digraph]
PathS [in graphs.digraph]
PathTheory [in graphs.digraph]
PathTheory.Fixed [in graphs.digraph]
Q
QuotBij [in graphs.finite_quotient]QuotFun [in graphs.finite_quotient]
quot_union_K [in graphs.finite_quotient]
quot_id [in graphs.finite_quotient]
quot_quot [in graphs.finite_quotient]
quot_kernel [in graphs.finite_quotient]
quot.s [in graphs.finite_quotient]
S
s [in graphs.mgraph2_tw2]s [in graphs.mgraph]
s [in graphs.mgraph2]
SeparatorConnector [in graphs.connectivity]
SeparatorConnector.ConnectorTheory [in graphs.connectivity]
SetTac [in graphs.set_tac]
sig_sum_bij.NonDisjoint [in graphs.finite_quotient]
sig_sum_bij.Disjoint [in graphs.finite_quotient]
sig_sum_bij [in graphs.finite_quotient]
SimplePaths [in graphs.sgraph]
Skeleton [in graphs.skeleton]
SSkeleton [in graphs.skeleton]
SSkeleton.IsoComponents [in graphs.skeleton]
Subalgebra [in graphs.mgraph2_tw2]
Subalgebra.Quotients [in graphs.mgraph2_tw2]
s.Edges [in graphs.mgraph]
s.h_merge_nothing' [in graphs.mgraph]
s.merge [in graphs.mgraph]
s.merge_union_K [in graphs.mgraph]
s.merge_merge_seq [in graphs.mgraph]
s.merge_nothing [in graphs.mgraph]
s.merge_same [in graphs.mgraph]
s.merge_same' [in graphs.mgraph]
s.merge_merge [in graphs.mgraph]
s.merge_surj [in graphs.mgraph]
s.Subgraphs [in graphs.mgraph]
s.union_merge_r [in graphs.mgraph]
s.union_merge_l [in graphs.mgraph]
T
t [in graphs.finite_quotient]terms [in graphs.pttdom]
terms [in graphs.ptt]
terms.e [in graphs.pttdom]
terms.e [in graphs.ptt]
Theory [in graphs.structures]
Transfer [in graphs.digraph]
Tree [in graphs.helly]
U
union_quot_r [in graphs.finite_quotient]union_quot_l [in graphs.finite_quotient]
update [in graphs.preliminaries]
V
vcover [in graphs.connectivity]VSeparator [in graphs.connectivity]
W
Walk [in graphs.mgraph]Instance Index
A
add_vertex_iso [in graphs.mgraph]add_vertex2_iso [in graphs.mgraph2]
B
bij_Equivalence [in graphs.bij]C
cnv_iso2 [in graphs.mgraph2]D
diso_Equivalence [in graphs.digraph]dom_eqv_ [in graphs.ptt]
dom_iso2 [in graphs.mgraph2]
dot_iso2 [in graphs.mgraph2]
E
edge_graph2_iso [in graphs.mgraph2]equiv_rel_Equivalence [in graphs.equiv]
eqv_morphim [in graphs.structures]
eqv_sym [in graphs.structures]
ex2_iff_morphism [in graphs.preliminaries]
I
iso_Equivalence [in graphs.mgraph]iso2prop_Equivalence [in graphs.mgraph2]
iso2_Equivalence [in graphs.mgraph2]
P
par_iso2 [in graphs.mgraph2]R
relabel_iso [in graphs.mgraph2]relabel2_iso [in graphs.mgraph2]
S
skel_iso [in graphs.skeleton]sskel_iso2 [in graphs.skeleton]
sum_bij [in graphs.bij]
T
two_graph2_iso [in graphs.mgraph2]U
union_iso [in graphs.mgraph]unit_graph_iso [in graphs.mgraph]
unit_graph2_iso [in graphs.mgraph2]
Abbreviation Index
A
add_test_cong [in graphs.mgraph2]add_test [in graphs.mgraph2]
C
CEquivalence [in graphs.structures]conn [in graphs.excluded]
conn [in graphs.excluded]
CProper [in graphs.structures]
D
DiGraph [in graphs.digraph]diGraph [in graphs.digraph]
di_edge [in graphs.digraph]
E
eC [in graphs.finite_quotient]ereprK [in graphs.finite_quotient]
G
graph [in graphs.mgraph2_tw2]graph [in graphs.extraction_def]
graph [in graphs.extraction_top]
graph [in graphs.skeleton]
graph [in graphs.skeleton]
graph [in graphs.extraction_iso]
graph [in graphs.mgraph]
graph [in graphs.mgraph2]
graph2 [in graphs.mgraph2_tw2]
graph2 [in graphs.extraction_def]
graph2 [in graphs.extraction_top]
graph2 [in graphs.skeleton]
graph2 [in graphs.extraction_iso]
G1 [in graphs.mgraph]
G12 [in graphs.mgraph]
G2 [in graphs.mgraph]
I
i [in graphs.structures]induced2 [in graphs.extraction_top]
IO [in graphs.mgraph2]
L
Le [in graphs.mgraph]Le [in graphs.mgraph2]
link_rel [in graphs.extraction_def]
Lv [in graphs.mgraph]
Lv [in graphs.mgraph2]
M
measure [in graphs.extraction_def]merge_seq [in graphs.mgraph]
merge_seq [in graphs.mgraph]
merge2_seq [in graphs.mgraph2]
merge2_seq [in graphs.mgraph2]
N
NB [in graphs.excluded]NB [in graphs.excluded]
P
Path [in graphs.treewidth]point [in graphs.mgraph2]
point [in graphs.mgraph2]
pos [in graphs.set_tac]
R
rel0 [in graphs.preliminaries]S
sig [in graphs.finite_quotient]sigraph [in graphs.extraction_def]
source [in graphs.mgraph]
source [in graphs.mgraph]
T
target [in graphs.mgraph]target [in graphs.mgraph]
test [in graphs.pttdom]
U
UPath [in graphs.digraph]V
vfun [in graphs.preliminaries]Definition Index
A
add_node [in graphs.sgraph]add_node_rel [in graphs.sgraph]
add_edge [in graphs.sgraph]
add_edge_rel [in graphs.sgraph]
add_vertex [in graphs.mgraph]
add_vlabel [in graphs.mgraph]
add_edge [in graphs.mgraph]
add_vlabel2 [in graphs.mgraph2]
add_edge2 [in graphs.mgraph2]
add_vertex2 [in graphs.mgraph2]
adjacent [in graphs.skeleton]
admissible [in graphs.mgraph2_tw2]
B
bag [in graphs.checkpoint]bgraph [in graphs.skeleton]
bijD1 [in graphs.bij]
bijD1_bwd [in graphs.bij]
bijD1_fwd [in graphs.bij]
bij_comp [in graphs.bij]
bij_sym [in graphs.bij]
bij_id [in graphs.bij]
bij_cast [in graphs.finmap_plus]
bij_setD [in graphs.finmap_plus]
bij_quot [in graphs.finite_quotient]
bipartition [in graphs.connectivity]
bool_option_unit [in graphs.bij]
bool_swap [in graphs.bij]
C
castL [in graphs.digraph]CK4F [in graphs.extraction_def]
clique [in graphs.sgraph]
cliqueb [in graphs.sgraph]
compatible [in graphs.mgraph2_tw2]
complete [in graphs.sgraph]
complete_rel [in graphs.sgraph]
component [in graphs.extraction_def]
components [in graphs.sgraph]
component_in [in graphs.excluded]
component_of [in graphs.sgraph]
component_e' [in graphs.skeleton]
component_e [in graphs.skeleton]
component_v' [in graphs.skeleton]
component_v [in graphs.skeleton]
component1 [in graphs.extraction_top]
connected [in graphs.sgraph]
connectedb [in graphs.sgraph]
consistent [in graphs.mgraph]
const0 [in graphs.bounded]
const0_rec [in graphs.bounded]
CP [in graphs.checkpoint]
cp [in graphs.checkpoint]
cpo [in graphs.checkpoint]
cr [in graphs.preliminaries]
C3 [in graphs.sgraph]
D
decompL [in graphs.treewidth]decompU [in graphs.treewidth]
del_edge_liftS [in graphs.digraph]
del_edge [in graphs.digraph]
del_rel [in graphs.digraph]
digraph_of [in graphs.mgraph]
dimatching [in graphs.connectivity]
dimatching_of [in graphs.connectivity]
disconnected [in graphs.sgraph]
disjoint_transL [in graphs.preliminaries]
diso_comp [in graphs.digraph]
diso_sym [in graphs.digraph]
diso_id [in graphs.digraph]
E
edgep [in graphs.digraph]edges [in graphs.connectivity]
edges [in graphs.mgraph]
edges_in [in graphs.mgraph]
edges_at [in graphs.mgraph]
edge_set [in graphs.mgraph]
edge_graph [in graphs.mgraph]
edge_graph2 [in graphs.mgraph2]
edge_surjective [in graphs.minor]
equiv_of_trans [in graphs.preliminaries]
equiv_of_refl [in graphs.preliminaries]
equiv_of [in graphs.preliminaries]
equiv_comp [in graphs.finite_quotient]
eqv_test [in graphs.pttdom]
eqv_ [in graphs.structures]
eqv_clot [in graphs.equiv]
eqv' [in graphs.pttdom]
eq_setoid [in graphs.structures]
eseparates [in graphs.mgraph]
eval [in graphs.pttdom]
eval [in graphs.ptt]
F
Fix [in graphs.bounded]flat_labels [in graphs.structures]
flesh_out_graph [in graphs.skeleton]
foldr1 [in graphs.preliminaries]
foo [in graphs.bounded]
foo_rec [in graphs.bounded]
fresh2_bij [in graphs.finmap_plus]
fsetD_bij [in graphs.finmap_plus]
fsetD_bij_bwd [in graphs.finmap_plus]
fsetD_bij_fwd [in graphs.finmap_plus]
fsetU1_fun [in graphs.finmap_plus]
fst [in graphs.digraph]
F_rec [in graphs.bounded]
G
graph_of_term [in graphs.extraction_def]g2_pttdom [in graphs.mgraph2]
g2_ptt [in graphs.mgraph2]
g2_var [in graphs.mgraph2]
g2_top [in graphs.mgraph2]
g2_one [in graphs.mgraph2]
g2_dom [in graphs.mgraph2]
g2_cnv [in graphs.mgraph2]
g2_dot [in graphs.mgraph2]
g2_par [in graphs.mgraph2]
H
hom_s [in graphs.sgraph]h_merge_union_Ke [in graphs.mgraph]
h_merge_union_Ke1 [in graphs.mgraph]
h_merge_union_K [in graphs.mgraph]
h_union_merge_l [in graphs.mgraph]
h_merge [in graphs.mgraph]
h' [in graphs.mgraph]
I
idp [in graphs.digraph]idx [in graphs.sgraph]
iend [in graphs.cp_minor]
igraph [in graphs.cp_minor]
igraph [in graphs.skeleton]
imfset_bij [in graphs.finmap_plus]
imfset_bij_bwd [in graphs.finmap_plus]
imfset_bij_fwd [in graphs.finmap_plus]
incident [in graphs.mgraph]
independent [in graphs.digraph]
induced [in graphs.sgraph]
induced [in graphs.digraph]
induced [in graphs.mgraph]
induced_rel [in graphs.sgraph]
induced_type [in graphs.sgraph]
induced_rel [in graphs.digraph]
induced_type [in graphs.digraph]
induced_proof [in graphs.mgraph]
induced2 [in graphs.extraction_def]
inE [in graphs.sgraph]
inE [in graphs.digraph]
infer_test [in graphs.pttdom]
interior [in graphs.digraph]
interval [in graphs.checkpoint]
interval_edges [in graphs.skeleton]
in_pathS [in graphs.digraph]
in_ipath [in graphs.digraph]
in_nodes [in graphs.digraph]
IPath_finMixin [in graphs.digraph]
IPath_countMixin [in graphs.digraph]
IPath_choiceMixin [in graphs.digraph]
IPath_eqMixin [in graphs.digraph]
irred [in graphs.digraph]
irred_of [in graphs.digraph]
iso_component [in graphs.skeleton]
iso_subgraph_forT [in graphs.mgraph]
iso_comp [in graphs.mgraph]
iso_sym [in graphs.mgraph]
iso_id [in graphs.mgraph]
Iso' [in graphs.mgraph]
iso2prop [in graphs.mgraph2]
iso2_comp [in graphs.mgraph2]
iso2_sym [in graphs.mgraph2]
iso2_id [in graphs.mgraph2]
istart [in graphs.cp_minor]
is_test [in graphs.pttdom]
is_forestb [in graphs.sgraph]
is_tree [in graphs.sgraph]
is_forest [in graphs.sgraph]
is_dhom [in graphs.digraph]
J
join_rel [in graphs.sgraph]K
kernel [in graphs.finite_quotient]kernelb [in graphs.finite_quotient]
K4 [in graphs.sgraph]
K4_free [in graphs.minor]
L
largest [in graphs.preliminaries]lens [in graphs.extraction_def]
line_graph [in graphs.mgraph]
link [in graphs.treewidth]
link_graph [in graphs.checkpoint]
link_rel [in graphs.checkpoint]
lst [in graphs.digraph]
M
map_equiv_rel [in graphs.finite_quotient]map_pairs [in graphs.equiv]
matching [in graphs.connectivity]
matching_of [in graphs.connectivity]
merge [in graphs.mgraph]
merge_union [in graphs.finite_quotient]
merge_union_rel [in graphs.finite_quotient]
merge_disjoint_union [in graphs.finite_quotient]
merge_union_bwdEr [in graphs.finite_quotient]
merge_union_bwdEl [in graphs.finite_quotient]
merge_union_bwd [in graphs.finite_quotient]
merge_union_fwd [in graphs.finite_quotient]
merge_subgraph_iso [in graphs.mgraph]
merge_subgraph_e [in graphs.mgraph]
merge_subgraph_v [in graphs.mgraph]
merge_union_K [in graphs.mgraph]
merge_merge_seq [in graphs.mgraph]
merge_nothing [in graphs.mgraph]
merge_sameE [in graphs.mgraph]
merge_same [in graphs.mgraph]
merge_same' [in graphs.mgraph]
merge_iso [in graphs.mgraph]
merge2 [in graphs.mgraph2]
mgraph_rel [in graphs.mgraph]
minor [in graphs.minor]
minor_rmap [in graphs.minor]
minor_map [in graphs.minor]
N
N [in graphs.connectivity]ncp [in graphs.checkpoint]
neighbor [in graphs.sgraph]
neighbours [in graphs.cp_minor]
nodes [in graphs.digraph]
nt [in graphs.pttdom]
nt_par [in graphs.pttdom]
nt_dot [in graphs.pttdom]
nt_dom [in graphs.pttdom]
nt_cnv [in graphs.pttdom]
nt_var [in graphs.pttdom]
nt_one [in graphs.pttdom]
num_edges [in graphs.digraph]
O
option_void [in graphs.bij]option_bij [in graphs.bij]
option2x [in graphs.bij]
option2_swap [in graphs.bij]
ord1 [in graphs.preliminaries]
ord2 [in graphs.preliminaries]
ord3 [in graphs.preliminaries]
P
pairs [in graphs.equiv]pathp [in graphs.digraph]
PathS [in graphs.digraph]
pathS [in graphs.digraph]
path_of_ipath [in graphs.digraph]
Path_countMixin [in graphs.digraph]
Path_choiceMixin [in graphs.digraph]
Path_eqMixin [in graphs.digraph]
pcat [in graphs.digraph]
pcatS [in graphs.digraph]
pcat_proof [in graphs.digraph]
pe_partition [in graphs.preliminaries]
pimset [in graphs.preliminaries]
prev [in graphs.sgraph]
prev_proof [in graphs.sgraph]
proper_separation [in graphs.connectivity]
Q
quot_union_K [in graphs.finite_quotient]quot_id [in graphs.finite_quotient]
quot_quot [in graphs.finite_quotient]
quot_bij [in graphs.finite_quotient]
quot_kernel [in graphs.finite_quotient]
quot_same [in graphs.finite_quotient]
quot_fun [in graphs.finite_quotient]
quot.pi [in graphs.finite_quotient]
quot.quot [in graphs.finite_quotient]
quot.repr [in graphs.finite_quotient]
R
redirect [in graphs.extraction_def]redirect_to [in graphs.extraction_def]
relabel [in graphs.mgraph2]
relabel2 [in graphs.mgraph2]
rel_of_pairs [in graphs.equiv]
remove_vertex [in graphs.mgraph]
remove_edges [in graphs.mgraph]
rename [in graphs.sgraph]
restrict [in graphs.preliminaries]
S
sc [in graphs.preliminaries]separates [in graphs.connectivity]
separatesb [in graphs.connectivity]
separation [in graphs.connectivity]
separator [in graphs.connectivity]
separatorb [in graphs.connectivity]
setT_bij [in graphs.bij]
sgP [in graphs.sgraph]
sg_irrefl [in graphs.sgraph]
sg_sym [in graphs.sgraph]
simple_check_point_wf [in graphs.extraction_def]
simple_check_point_term [in graphs.extraction_def]
sinterval [in graphs.checkpoint]
size_ind [in graphs.preliminaries]
sjoin [in graphs.sgraph]
skeleton [in graphs.skeleton]
sk_rel [in graphs.skeleton]
smallest [in graphs.preliminaries]
srestrict [in graphs.sgraph]
srev [in graphs.sgraph]
sskeleton [in graphs.skeleton]
strict_minor [in graphs.minor]
subgraph [in graphs.sgraph]
subgraph [in graphs.mgraph]
subgraph_for [in graphs.mgraph]
subrel_del_edge [in graphs.digraph]
subT_bij [in graphs.bij]
sub_edge [in graphs.mgraph]
sub_vertex [in graphs.mgraph]
sumA [in graphs.bij]
sumA' [in graphs.bij]
sumC [in graphs.bij]
sumf [in graphs.bij]
sum_eqE [in graphs.preliminaries]
sum_left [in graphs.finite_quotient]
sunit [in graphs.sgraph]
surjective [in graphs.preliminaries]
T
tail [in graphs.digraph]term_of_nterm [in graphs.pttdom]
term_of [in graphs.extraction_def]
term_of_rec [in graphs.extraction_def]
term_of_measure [in graphs.extraction_def]
term_of' [in graphs.extraction_top]
term_of_rec' [in graphs.extraction_top]
the_uPath [in graphs.checkpoint]
tjoin [in graphs.treewidth]
tlink [in graphs.treewidth]
tmEs [in graphs.extraction_def]
tm_pttdom [in graphs.pttdom]
tm_eqv [in graphs.pttdom]
tm_ [in graphs.extraction_def]
tm_ptt [in graphs.ptt]
tm_eqv [in graphs.ptt]
total_minor_map [in graphs.minor]
triv_decomp [in graphs.treewidth]
triv_sdecomp [in graphs.treewidth]
tunit [in graphs.sgraph]
tuple_UPath [in graphs.digraph]
two_graph [in graphs.mgraph]
two_graph2 [in graphs.mgraph2]
U
union [in graphs.mgraph]union_K_equiv [in graphs.finite_quotient]
union_quot_r [in graphs.finite_quotient]
union_equiv_r [in graphs.finite_quotient]
union_quot_l [in graphs.finite_quotient]
union_equiv_l_rel [in graphs.finite_quotient]
union_K_pairs [in graphs.mgraph]
union_merge_l [in graphs.mgraph]
unique [in graphs.preliminaries]
unit_forest [in graphs.sgraph]
unit_graph [in graphs.mgraph]
unit_graph2 [in graphs.mgraph2]
unl [in graphs.mgraph]
unr [in graphs.mgraph]
upath [in graphs.digraph]
UPathW [in graphs.digraph]
upath_of [in graphs.digraph]
UPath_finMixin [in graphs.digraph]
UPath_tuple [in graphs.digraph]
UPath_countMixin [in graphs.digraph]
UPath_choiceMixin [in graphs.digraph]
UPath_eqMixin [in graphs.digraph]
update [in graphs.preliminaries]
updateE [in graphs.preliminaries]
V
vcover [in graphs.connectivity]void_countMixin [in graphs.preliminaries]
void_choiceMixin [in graphs.preliminaries]
void_graph [in graphs.mgraph]
vseparator [in graphs.connectivity]
vseparatorb [in graphs.connectivity]
W
walk [in graphs.mgraph]width [in graphs.sgraph]
Record Index
B
bij [in graphs.bij]C
connector [in graphs.connectivity]D
diso [in graphs.digraph]F
forest [in graphs.sgraph]G
graph [in graphs.mgraph]graph2 [in graphs.mgraph2]
I
IPath [in graphs.digraph]iso [in graphs.mgraph]
iso2 [in graphs.mgraph2]
is_hom [in graphs.mgraph]
L
labels [in graphs.structures]M
monoidLaws [in graphs.structures]O
ops_ [in graphs.pttdom]P
Path [in graphs.digraph]ptt [in graphs.ptt]
pttdom [in graphs.pttdom]
R
relType [in graphs.digraph]S
sdecomp [in graphs.treewidth]setBox [in graphs.set_tac]
setoid [in graphs.structures]
sgraph [in graphs.sgraph]
T
test [in graphs.pttdom]U
UPath [in graphs.digraph]| 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 | (2340 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 | (54 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (365 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 | (27 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 | (1162 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 | (46 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 | (6 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (102 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 | (106 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 | (26 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 | (56 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 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 | (23 entries) |