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

digraph## E

edoneequiv

excluded

extraction_iso

extraction_top

extraction_def

## F

finite_quotientfinmap_plus

## H

helly## M

mgraphmgraph2

mgraph2_tw2

minor

## P

preliminariesptt

pttdom

## S

set_tacsgraph

skeleton

structures

## T

treewidth# Lemma 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) |