| 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 | (989 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 | (12 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 | (92 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 | (14 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 | (585 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 | (20 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 | (7 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 | (20 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 | (4 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 | (28 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 | (10 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 | (189 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 | (8 entries) |
Global Index
A
AddNode [section, in TwoPoint.minor]AddNode.G [variable, in TwoPoint.minor]
AddNode.N [variable, in TwoPoint.minor]
add_edge_induced_iso [lemma, in TwoPoint.cp_minor]
add_edge_swap [lemma, in TwoPoint.cp_minor]
add_node_minor [lemma, in TwoPoint.minor]
add_node_complete [lemma, in TwoPoint.minor]
add_node_lift_Path [lemma, in TwoPoint.minor]
add_node [definition, in TwoPoint.minor]
add_node_irrefl [lemma, in TwoPoint.minor]
add_node_sym [lemma, in TwoPoint.minor]
add_node_rel [definition, in TwoPoint.minor]
add_edge_connected [lemma, in TwoPoint.sgraph]
add_edge_Path [lemma, in TwoPoint.sgraph]
add_edge [definition, in TwoPoint.sgraph]
add_edge_irrefl [lemma, in TwoPoint.sgraph]
add_edge_sym [lemma, in TwoPoint.sgraph]
add_edge_rel [definition, in TwoPoint.sgraph]
adjacent [definition, in TwoPoint.skeleton]
adjacentI [lemma, in TwoPoint.skeleton]
adjacentP [lemma, in TwoPoint.skeleton]
adjacent_induced [lemma, in TwoPoint.skeleton]
adjacent_edge [lemma, in TwoPoint.skeleton]
adjacent_sym [lemma, in TwoPoint.skeleton]
admissible [definition, in TwoPoint.subalgebra]
all_cons [lemma, in TwoPoint.preliminaries]
B
bag [definition, in TwoPoint.checkpoint]bagP [lemma, in TwoPoint.checkpoint]
bagPn [lemma, in TwoPoint.checkpoint]
bags_in_out [lemma, in TwoPoint.checkpoint]
bag_cp [lemma, in TwoPoint.checkpoint]
bag_disj [lemma, in TwoPoint.checkpoint]
bag_extension [lemma, in TwoPoint.checkpoint]
bag_in_out [lemma, in TwoPoint.checkpoint]
bag_exit_edge [lemma, in TwoPoint.checkpoint]
bag_exit' [lemma, in TwoPoint.checkpoint]
bag_exit [lemma, in TwoPoint.checkpoint]
bag_sub_sinterval [lemma, in TwoPoint.checkpoint]
bag_nontrivial [lemma, in TwoPoint.checkpoint]
bag_id [lemma, in TwoPoint.checkpoint]
bag_edges_disj [lemma, in TwoPoint.skeleton]
bgraph [definition, in TwoPoint.skeleton]
bgraph_eq_io [lemma, in TwoPoint.skeleton]
bigcup_set1 [lemma, in TwoPoint.preliminaries]
big_par2_congr' [definition, in TwoPoint.tm_iso]
big_iso_congr [lemma, in TwoPoint.tm_iso]
big_seq2_maps [lemma, in TwoPoint.tm_iso]
big_seq2_map [lemma, in TwoPoint.tm_iso]
big_seq2_congrs [lemma, in TwoPoint.tm_iso]
big_seq2_congr [lemma, in TwoPoint.tm_iso]
big_seq2_cons [lemma, in TwoPoint.tm_iso]
big_seq2 [definition, in TwoPoint.tm_iso]
big_par2_congrs [lemma, in TwoPoint.tm_iso]
big_par2_congr [lemma, in TwoPoint.tm_iso]
big_par2_cat [lemma, in TwoPoint.tm_iso]
big_par2_map [lemma, in TwoPoint.tm_iso]
big_par2_1 [lemma, in TwoPoint.tm_iso]
big_par2_cons [lemma, in TwoPoint.tm_iso]
big_par2 [definition, in TwoPoint.tm_iso]
big_tmI [definition, in TwoPoint.tm_iso]
big_enum_in [lemma, in TwoPoint.preliminaries]
bijective2 [definition, in TwoPoint.multigraph]
bij_surj [lemma, in TwoPoint.preliminaries]
Bounded [section, in TwoPoint.bounded]
bounded [library]
Bounded.aT [variable, in TwoPoint.bounded]
Bounded.F [variable, in TwoPoint.bounded]
Bounded.F_wf [variable, in TwoPoint.bounded]
Bounded.measure [variable, in TwoPoint.bounded]
Bounded.P [variable, in TwoPoint.bounded]
Bounded.rT [variable, in TwoPoint.bounded]
Bounded.x0 [variable, in TwoPoint.bounded]
C
can_irred_of [lemma, in TwoPoint.sgraph]cardsCT [lemma, in TwoPoint.preliminaries]
cardsI [lemma, in TwoPoint.preliminaries]
cards3 [lemma, in TwoPoint.preliminaries]
card_void [lemma, in TwoPoint.preliminaries]
card_le1P [lemma, in TwoPoint.preliminaries]
card_gt1P [lemma, in TwoPoint.preliminaries]
card_le1 [lemma, in TwoPoint.preliminaries]
card_ltnT [lemma, in TwoPoint.preliminaries]
card_val [lemma, in TwoPoint.skeleton]
card1P [lemma, in TwoPoint.preliminaries]
card12 [lemma, in TwoPoint.preliminaries]
checkpoint [library]
CheckpointOrder [section, in TwoPoint.checkpoint]
CheckpointOrder.conn_io [variable, in TwoPoint.checkpoint]
CheckpointOrder.G [variable, in TwoPoint.checkpoint]
CheckpointOrder.i [variable, in TwoPoint.checkpoint]
CheckpointOrder.o [variable, in TwoPoint.checkpoint]
CheckPoints [section, in TwoPoint.checkpoint]
CheckpointsAndMinors [section, in TwoPoint.cp_minor]
CheckpointsAndMinors.conn_G [variable, in TwoPoint.cp_minor]
CheckpointsAndMinors.G [variable, in TwoPoint.cp_minor]
CheckPoints.G [variable, in TwoPoint.checkpoint]
CheckPoints.G_conn [variable, in TwoPoint.checkpoint]
CheckPoints.G_conn' [variable, in TwoPoint.checkpoint]
_ ⋄ _ [notation, in TwoPoint.checkpoint]
CK4F [definition, in TwoPoint.extraction_def]
CK4F_lens_rest [lemma, in TwoPoint.extraction_def]
CK4F_remove_loops [lemma, in TwoPoint.extraction_def]
CK4F_remove_edges [lemma, in TwoPoint.extraction_def]
CK4F_split_cpM [lemma, in TwoPoint.extraction_def]
CK4F_split_cpR [lemma, in TwoPoint.extraction_def]
CK4F_split_cpL [lemma, in TwoPoint.extraction_def]
CK4F_lens [lemma, in TwoPoint.extraction_def]
CK4F_redirect [lemma, in TwoPoint.extraction_def]
CK4F_one [lemma, in TwoPoint.extraction_def]
CK4F_remove_component [lemma, in TwoPoint.extraction_def]
CK4F_induced2 [lemma, in TwoPoint.extraction_def]
CK4F_sub [lemma, in TwoPoint.extraction_def]
CK4F_igraph [lemma, in TwoPoint.extraction_def]
clique [definition, in TwoPoint.sgraph]
clique1 [lemma, in TwoPoint.sgraph]
clique2 [lemma, in TwoPoint.sgraph]
cnv2 [definition, in TwoPoint.subalgebra]
codom_Some [lemma, in TwoPoint.preliminaries]
collapse_bags [lemma, in TwoPoint.cp_minor]
compatible [definition, in TwoPoint.subalgebra]
complete [definition, in TwoPoint.minor]
complete_irrefl [lemma, in TwoPoint.minor]
complete_sym [lemma, in TwoPoint.minor]
complete_rel [definition, in TwoPoint.minor]
component [definition, in TwoPoint.extraction_def]
componentless_top [lemma, in TwoPoint.extraction_iso]
componentless_one [lemma, in TwoPoint.extraction_iso]
components [definition, in TwoPoint.sgraph]
components_pblockP [lemma, in TwoPoint.sgraph]
component_exit [lemma, in TwoPoint.sgraph]
comp_dom2_redirect [lemma, in TwoPoint.extraction_iso]
comp_exit [lemma, in TwoPoint.extraction_iso]
connected [definition, in TwoPoint.sgraph]
connectedb [definition, in TwoPoint.sgraph]
connectedP [lemma, in TwoPoint.sgraph]
connectedTE [lemma, in TwoPoint.sgraph]
connectedTI [lemma, in TwoPoint.sgraph]
connectedU_edge [lemma, in TwoPoint.sgraph]
connected_remove_triv_bag2 [lemma, in TwoPoint.cp_minor]
connected_bag [lemma, in TwoPoint.checkpoint]
connected_interval [lemma, in TwoPoint.checkpoint]
connected_CP_closed [lemma, in TwoPoint.checkpoint]
connected_cp_closed [lemma, in TwoPoint.checkpoint]
connected_igraph [lemma, in TwoPoint.skeleton]
connected_bgraph [lemma, in TwoPoint.skeleton]
connected_skeleton [lemma, in TwoPoint.skeleton]
connected_skeleton' [lemma, in TwoPoint.skeleton]
connected_add_node [lemma, in TwoPoint.minor]
connected_in_components [lemma, in TwoPoint.sgraph]
connected_center [lemma, in TwoPoint.sgraph]
connected_card_gt1 [lemma, in TwoPoint.sgraph]
connected_induced [lemma, in TwoPoint.sgraph]
connected_in_subgraph [lemma, in TwoPoint.sgraph]
connected_path [lemma, in TwoPoint.sgraph]
connected_restrict [lemma, in TwoPoint.sgraph]
connected_component_set [lemma, in TwoPoint.extraction_def]
connected_induced [lemma, in TwoPoint.extraction_def]
connected1 [lemma, in TwoPoint.sgraph]
connected2 [lemma, in TwoPoint.sgraph]
connectRI [lemma, in TwoPoint.sgraph]
connectUP [lemma, in TwoPoint.preliminaries]
connect_img [lemma, in TwoPoint.preliminaries]
connect_symI [lemma, in TwoPoint.preliminaries]
connect_mono [lemma, in TwoPoint.preliminaries]
connect_restrict_case [lemma, in TwoPoint.sgraph]
consistent [definition, in TwoPoint.multigraph]
consistentT [lemma, in TwoPoint.extraction_def]
consistent_setD [lemma, in TwoPoint.skeleton]
const0 [definition, in TwoPoint.bounded]
const0_eq [lemma, in TwoPoint.bounded]
const0_rec [definition, in TwoPoint.bounded]
CP [definition, in TwoPoint.checkpoint]
cp [definition, in TwoPoint.checkpoint]
cpNI [lemma, in TwoPoint.checkpoint]
cpN_trans [lemma, in TwoPoint.checkpoint]
cpo [definition, in TwoPoint.checkpoint]
cpo_cp [lemma, in TwoPoint.checkpoint]
cpo_max [lemma, in TwoPoint.checkpoint]
cpo_min [lemma, in TwoPoint.checkpoint]
cpo_order [lemma, in TwoPoint.checkpoint]
cpo_antisym [lemma, in TwoPoint.checkpoint]
cpo_total [lemma, in TwoPoint.checkpoint]
cpo_trans [lemma, in TwoPoint.checkpoint]
cpo_refl [lemma, in TwoPoint.checkpoint]
cpP [lemma, in TwoPoint.checkpoint]
cpPn [lemma, in TwoPoint.checkpoint]
cpTI [lemma, in TwoPoint.checkpoint]
cpxx [lemma, in TwoPoint.checkpoint]
CP_tree [lemma, in TwoPoint.cp_minor]
CP_treeI [lemma, in TwoPoint.checkpoint]
CP_triangle_bags [lemma, in TwoPoint.checkpoint]
CP_bags [lemma, in TwoPoint.checkpoint]
CP_tree_sinterval [lemma, in TwoPoint.checkpoint]
cp_sub_interval [lemma, in TwoPoint.checkpoint]
CP_tree_paths [lemma, in TwoPoint.checkpoint]
CP_connected [lemma, in TwoPoint.checkpoint]
CP_path [lemma, in TwoPoint.checkpoint]
CP_clique [lemma, in TwoPoint.checkpoint]
CP_base [lemma, in TwoPoint.checkpoint]
CP_closed [lemma, in TwoPoint.checkpoint]
CP_mono [lemma, in TwoPoint.checkpoint]
CP_extensive [lemma, in TwoPoint.checkpoint]
CP_set2 [lemma, in TwoPoint.checkpoint]
cp_neighbours [lemma, in TwoPoint.checkpoint]
cp_tighten [lemma, in TwoPoint.checkpoint]
cp_tightenR [lemma, in TwoPoint.checkpoint]
cp_widen [lemma, in TwoPoint.checkpoint]
cp_widenR [lemma, in TwoPoint.checkpoint]
cp_mid [lemma, in TwoPoint.checkpoint]
cp_triangle [lemma, in TwoPoint.checkpoint]
cp_sym [lemma, in TwoPoint.checkpoint]
cp_minor [library]
cr [definition, in TwoPoint.preliminaries]
crK [lemma, in TwoPoint.preliminaries]
cycle_clique [lemma, in TwoPoint.checkpoint]
C3 [definition, in TwoPoint.minor]
C3_of_triangle [lemma, in TwoPoint.cp_minor]
D
decompL [definition, in TwoPoint.subalgebra]DecompTheory [section, in TwoPoint.minor]
DecompTheory.B [variable, in TwoPoint.minor]
DecompTheory.decD [variable, in TwoPoint.minor]
DecompTheory.G [variable, in TwoPoint.minor]
DecompTheory.T [variable, in TwoPoint.minor]
decompU [definition, in TwoPoint.subalgebra]
decomp_small [lemma, in TwoPoint.subalgebra]
decomp_dom [lemma, in TwoPoint.subalgebra]
decomp_cnv [lemma, in TwoPoint.subalgebra]
decomp_seq2 [lemma, in TwoPoint.subalgebra]
decomp_par2 [lemma, in TwoPoint.subalgebra]
decomp_quot [lemma, in TwoPoint.subalgebra]
decomp_link [lemma, in TwoPoint.subalgebra]
decomp_clique [lemma, in TwoPoint.minor]
disconnected [definition, in TwoPoint.sgraph]
disconnectedE [lemma, in TwoPoint.sgraph]
disjointE [lemma, in TwoPoint.preliminaries]
disjointFl [lemma, in TwoPoint.preliminaries]
disjointFr [lemma, in TwoPoint.preliminaries]
disjointNI [lemma, in TwoPoint.preliminaries]
disjoint_transR [lemma, in TwoPoint.preliminaries]
disjoint_transL [definition, in TwoPoint.preliminaries]
disjoint_edgep [lemma, in TwoPoint.sgraph]
Disjoint3 [section, in TwoPoint.preliminaries]
disjoint3P [lemma, in TwoPoint.preliminaries]
disjoint3_cases [inductive, in TwoPoint.preliminaries]
Disjoint3.A [variable, in TwoPoint.preliminaries]
Disjoint3.B [variable, in TwoPoint.preliminaries]
Disjoint3.C [variable, in TwoPoint.preliminaries]
Disjoint3.T [variable, in TwoPoint.preliminaries]
Dis3In1 [constructor, in TwoPoint.preliminaries]
Dis3In2 [constructor, in TwoPoint.preliminaries]
Dis3In3 [constructor, in TwoPoint.preliminaries]
Dis3Notin [constructor, in TwoPoint.preliminaries]
dom2 [definition, in TwoPoint.subalgebra]
dom2_morphism [instance, in TwoPoint.tm_iso]
E
eC [abbreviation, in TwoPoint.finite_quotient]edge [projection, in TwoPoint.multigraph]
edgeless_bag [lemma, in TwoPoint.extraction_def]
edgep [definition, in TwoPoint.sgraph]
edgep_proof [lemma, in TwoPoint.sgraph]
edges [definition, in TwoPoint.multigraph]
edges_st [lemma, in TwoPoint.extraction_iso]
edges2 [definition, in TwoPoint.extraction_iso]
edges2_graph_of [lemma, in TwoPoint.extraction_iso]
edges2_big [lemma, in TwoPoint.extraction_iso]
edges2_cons [lemma, in TwoPoint.extraction_iso]
edges2_nil [lemma, in TwoPoint.extraction_iso]
edges2_graph [definition, in TwoPoint.extraction_iso]
edge_in_set [lemma, in TwoPoint.multigraph]
edge_set1 [lemma, in TwoPoint.multigraph]
edge_set [definition, in TwoPoint.multigraph]
edge_graph [definition, in TwoPoint.subalgebra]
edge_set_adj [lemma, in TwoPoint.skeleton]
edge_surjective [definition, in TwoPoint.minor]
edone [library]
emb_surj [lemma, in TwoPoint.preliminaries]
empty_uniqe [lemma, in TwoPoint.preliminaries]
Equivalence [section, in TwoPoint.preliminaries]
equivalence_partition_gt1P [lemma, in TwoPoint.preliminaries]
equivalence_rel_of_sym [lemma, in TwoPoint.preliminaries]
Equivalence.e [variable, in TwoPoint.preliminaries]
Equivalence.T [variable, in TwoPoint.preliminaries]
equiv_of_trans [definition, in TwoPoint.preliminaries]
equiv_of_sym [lemma, in TwoPoint.preliminaries]
equiv_of_refl [definition, in TwoPoint.preliminaries]
equiv_of [definition, in TwoPoint.preliminaries]
eq_set1P [lemma, in TwoPoint.preliminaries]
eq_quot_finMixin [lemma, in TwoPoint.finite_quotient]
ereprK [abbreviation, in TwoPoint.finite_quotient]
extraction_iso [library]
extraction_def [library]
F
FinEncodingModuloRel [section, in TwoPoint.finite_quotient]FinEncodingModuloRel.C [variable, in TwoPoint.finite_quotient]
FinEncodingModuloRel.CD [variable, in TwoPoint.finite_quotient]
FinEncodingModuloRel.D [variable, in TwoPoint.finite_quotient]
FinEncodingModuloRel.DC [variable, in TwoPoint.finite_quotient]
FinEncodingModuloRel.eD [variable, in TwoPoint.finite_quotient]
FinEncodingModuloRel.encD [variable, in TwoPoint.finite_quotient]
finite_quotient [library]
Fix [definition, in TwoPoint.bounded]
Fix_eq [lemma, in TwoPoint.bounded]
flesh_out [lemma, in TwoPoint.skeleton]
flesh_out_graph [definition, in TwoPoint.skeleton]
Foldr1 [section, in TwoPoint.preliminaries]
foldr1 [definition, in TwoPoint.preliminaries]
foldr1_set_default [lemma, in TwoPoint.preliminaries]
Foldr1.F [variable, in TwoPoint.preliminaries]
Foldr1.I [variable, in TwoPoint.preliminaries]
Foldr1.op [variable, in TwoPoint.preliminaries]
Foldr1.R [variable, in TwoPoint.preliminaries]
foo [definition, in TwoPoint.bounded]
foo_eq [lemma, in TwoPoint.bounded]
foo_rec [definition, in TwoPoint.bounded]
forest [record, in TwoPoint.sgraph]
Forest [constructor, in TwoPoint.sgraph]
forestI [lemma, in TwoPoint.sgraph]
forestP [lemma, in TwoPoint.sgraph]
Forests [section, in TwoPoint.sgraph]
Forests.G [variable, in TwoPoint.sgraph]
forestT_unique [lemma, in TwoPoint.sgraph]
forest_is_forest [projection, in TwoPoint.sgraph]
funU [definition, in TwoPoint.multigraph]
fun_decompose [lemma, in TwoPoint.preliminaries]
F_rec_narrow [lemma, in TwoPoint.bounded]
F_rec [definition, in TwoPoint.bounded]
G
get_edge [lemma, in TwoPoint.extraction_def]graph [record, in TwoPoint.multigraph]
Graph [constructor, in TwoPoint.multigraph]
graph_of_big_tmIs [lemma, in TwoPoint.tm_iso]
graph_of_big_tmI [lemma, in TwoPoint.tm_iso]
graph_of [projection, in TwoPoint.multigraph]
graph_minor_TW2 [lemma, in TwoPoint.extraction_iso]
graph_of_TW2 [lemma, in TwoPoint.subalgebra]
graph_of_term [definition, in TwoPoint.subalgebra]
graph2 [record, in TwoPoint.multigraph]
Graph2 [constructor, in TwoPoint.multigraph]
g_out [projection, in TwoPoint.multigraph]
g_in [projection, in TwoPoint.multigraph]
H
has_edge [lemma, in TwoPoint.skeleton]hom_of_surj [lemma, in TwoPoint.multigraph]
hom_of [definition, in TwoPoint.multigraph]
hom_gI [lemma, in TwoPoint.multigraph]
hom_g2 [definition, in TwoPoint.multigraph]
hom_g [definition, in TwoPoint.multigraph]
hom_eqL [lemma, in TwoPoint.subalgebra]
hom_s [definition, in TwoPoint.sgraph]
hom2_sskel [lemma, in TwoPoint.skeleton]
h_ty [definition, in TwoPoint.multigraph]
I
idp [definition, in TwoPoint.sgraph]idx [definition, in TwoPoint.sgraph]
idxR [lemma, in TwoPoint.sgraph]
idx_swap [lemma, in TwoPoint.sgraph]
idx_srev [lemma, in TwoPoint.sgraph]
idx_nLR [lemma, in TwoPoint.sgraph]
idx_inj [lemma, in TwoPoint.sgraph]
idx_catR [lemma, in TwoPoint.sgraph]
idx_catL [lemma, in TwoPoint.sgraph]
idx_end [lemma, in TwoPoint.sgraph]
idx_start [lemma, in TwoPoint.sgraph]
idx_mem [lemma, in TwoPoint.sgraph]
id_surj [lemma, in TwoPoint.preliminaries]
id_bij [lemma, in TwoPoint.preliminaries]
iend [definition, in TwoPoint.cp_minor]
igraph [definition, in TwoPoint.cp_minor]
igraph [definition, in TwoPoint.skeleton]
igraph_K4F_add_node [lemma, in TwoPoint.cp_minor]
igraph_K4F [lemma, in TwoPoint.cp_minor]
igraph_proof [lemma, in TwoPoint.skeleton]
imset_valT [lemma, in TwoPoint.preliminaries]
imset_pre_val [lemma, in TwoPoint.preliminaries]
index_rev [lemma, in TwoPoint.sgraph]
index_rcons [lemma, in TwoPoint.sgraph]
induced [definition, in TwoPoint.multigraph]
induced [definition, in TwoPoint.sgraph]
InducedSubgraph [section, in TwoPoint.sgraph]
InducedSubgraph.G [variable, in TwoPoint.sgraph]
InducedSubgraph.S [variable, in TwoPoint.sgraph]
induced_sub [lemma, in TwoPoint.multigraph]
induced_proof [definition, in TwoPoint.multigraph]
induced_minor [lemma, in TwoPoint.minor]
induced_path [lemma, in TwoPoint.sgraph]
induced_sub [lemma, in TwoPoint.sgraph]
induced_irrefl [lemma, in TwoPoint.sgraph]
induced_sym [lemma, in TwoPoint.sgraph]
induced_rel [definition, in TwoPoint.sgraph]
induced_type [definition, in TwoPoint.sgraph]
induced_K4_free [lemma, in TwoPoint.extraction_def]
induced2 [definition, in TwoPoint.multigraph]
induced2_induced [lemma, in TwoPoint.multigraph]
injective2 [definition, in TwoPoint.multigraph]
inj_imset [lemma, in TwoPoint.preliminaries]
inj_omap [lemma, in TwoPoint.preliminaries]
inl_codom_inr [lemma, in TwoPoint.preliminaries]
inl_inj [lemma, in TwoPoint.preliminaries]
inl_eqE [lemma, in TwoPoint.preliminaries]
inr_codom_inl [lemma, in TwoPoint.preliminaries]
inr_inj [lemma, in TwoPoint.preliminaries]
inr_eqE [lemma, in TwoPoint.preliminaries]
ins [lemma, in TwoPoint.cp_minor]
interval [definition, in TwoPoint.checkpoint]
intervalI_cp [lemma, in TwoPoint.checkpoint]
intervalL [lemma, in TwoPoint.checkpoint]
intervalR [lemma, in TwoPoint.checkpoint]
interval_edge_cp [lemma, in TwoPoint.checkpoint]
interval_cp_cover [lemma, in TwoPoint.checkpoint]
interval_bag_disj [lemma, in TwoPoint.checkpoint]
interval_sym [lemma, in TwoPoint.checkpoint]
interval_cp_edge_cover [lemma, in TwoPoint.skeleton]
interval_bag_edge_cover [lemma, in TwoPoint.skeleton]
interval_edges_disj_cp [lemma, in TwoPoint.skeleton]
interval_bag_edges_disj [lemma, in TwoPoint.skeleton]
interval_edges_sym [lemma, in TwoPoint.skeleton]
interval_edges [definition, in TwoPoint.skeleton]
in_tail [lemma, in TwoPoint.sgraph]
in_nodes [definition, in TwoPoint.sgraph]
IO [abbreviation, in TwoPoint.tm_iso]
IO [abbreviation, in TwoPoint.extraction_def]
IPath [record, in TwoPoint.sgraph]
IPath_finMixin [definition, in TwoPoint.sgraph]
IPath_countMixin [definition, in TwoPoint.sgraph]
IPath_choiceMixin [definition, in TwoPoint.sgraph]
IPath_eqMixin [definition, in TwoPoint.sgraph]
irred [definition, in TwoPoint.sgraph]
irredE [lemma, in TwoPoint.sgraph]
irredxx [lemma, in TwoPoint.sgraph]
irred_ind [lemma, in TwoPoint.sgraph]
irred_edgeL [lemma, in TwoPoint.sgraph]
irred_edge [lemma, in TwoPoint.sgraph]
irred_id [lemma, in TwoPoint.sgraph]
irred_rev [lemma, in TwoPoint.sgraph]
irred_cat' [lemma, in TwoPoint.sgraph]
irred_cat [lemma, in TwoPoint.sgraph]
irred_nodes [lemma, in TwoPoint.sgraph]
irred_of [definition, in TwoPoint.sgraph]
irred_upath [lemma, in TwoPoint.sgraph]
irreflexive_restrict [lemma, in TwoPoint.sgraph]
iso [definition, in TwoPoint.multigraph]
iso_one [lemma, in TwoPoint.tm_iso]
iso_top [lemma, in TwoPoint.tm_iso]
iso_split_par2 [lemma, in TwoPoint.tm_iso]
iso_of_iso2 [lemma, in TwoPoint.multigraph]
iso_pointxx [lemma, in TwoPoint.skeleton]
iso_K4_free [lemma, in TwoPoint.minor]
iso_strict_minor [lemma, in TwoPoint.minor]
iso_connected [lemma, in TwoPoint.sgraph]
iso_subgraph [lemma, in TwoPoint.sgraph]
iso2 [definition, in TwoPoint.multigraph]
iso2_congruence [definition, in TwoPoint.tm_iso]
iso2_Equivalence [instance, in TwoPoint.multigraph]
iso2_union [lemma, in TwoPoint.multigraph]
iso2_point [lemma, in TwoPoint.multigraph]
iso2_inv_out [lemma, in TwoPoint.multigraph]
iso2_inv_in [lemma, in TwoPoint.multigraph]
iso2_refl [lemma, in TwoPoint.multigraph]
iso2_sym [lemma, in TwoPoint.multigraph]
iso2_inv [lemma, in TwoPoint.multigraph]
iso2_trans [lemma, in TwoPoint.multigraph]
iso2_of_iso [lemma, in TwoPoint.multigraph]
iso2_decomp [lemma, in TwoPoint.skeleton]
iso2_sskel [lemma, in TwoPoint.skeleton]
iso2_skel [lemma, in TwoPoint.skeleton]
ISplit [constructor, in TwoPoint.sgraph]
isplit [inductive, in TwoPoint.sgraph]
isplitP [lemma, in TwoPoint.sgraph]
istart [definition, in TwoPoint.cp_minor]
is_forestP [lemma, in TwoPoint.sgraph]
is_forestb [definition, in TwoPoint.sgraph]
is_tree [definition, in TwoPoint.sgraph]
is_forest [definition, in TwoPoint.sgraph]
ival [projection, in TwoPoint.sgraph]
J
JoinSG [section, in TwoPoint.sgraph]JoinSG.G1 [variable, in TwoPoint.sgraph]
JoinSG.G2 [variable, in TwoPoint.sgraph]
JoinT [section, in TwoPoint.subalgebra]
JoinT.T1 [variable, in TwoPoint.subalgebra]
JoinT.T2 [variable, in TwoPoint.subalgebra]
join_width [lemma, in TwoPoint.subalgebra]
join_decomp [lemma, in TwoPoint.subalgebra]
join_is_forest [lemma, in TwoPoint.subalgebra]
join_disc [lemma, in TwoPoint.sgraph]
join_rel_irrefl [lemma, in TwoPoint.sgraph]
join_rel_sym [lemma, in TwoPoint.sgraph]
join_rel [definition, in TwoPoint.sgraph]
K
K4 [definition, in TwoPoint.minor]K4_of_triangle [lemma, in TwoPoint.cp_minor]
K4_free [definition, in TwoPoint.minor]
K4_width [lemma, in TwoPoint.minor]
K4_bag [lemma, in TwoPoint.minor]
L
label [projection, in TwoPoint.multigraph]last_belast_eq [lemma, in TwoPoint.preliminaries]
last_take [lemma, in TwoPoint.preliminaries]
last_rev_belast [lemma, in TwoPoint.sgraph]
lens [definition, in TwoPoint.extraction_def]
lens_components [lemma, in TwoPoint.extraction_def]
lens_sinterval [lemma, in TwoPoint.extraction_def]
lens_io_set [lemma, in TwoPoint.extraction_def]
leq_subn [lemma, in TwoPoint.preliminaries]
lift_equiv [lemma, in TwoPoint.preliminaries]
lift_path [lemma, in TwoPoint.preliminaries]
lift_Path [lemma, in TwoPoint.sgraph]
lift_upath [lemma, in TwoPoint.sgraph]
lift_spath [lemma, in TwoPoint.sgraph]
link [definition, in TwoPoint.subalgebra]
Link [section, in TwoPoint.subalgebra]
linkNeq [lemma, in TwoPoint.cp_minor]
link_is_forest [lemma, in TwoPoint.subalgebra]
link_has_None [lemma, in TwoPoint.subalgebra]
link_unique_None [lemma, in TwoPoint.subalgebra]
link_bypass [lemma, in TwoPoint.subalgebra]
link_unique_lift [lemma, in TwoPoint.subalgebra]
link_cycle [lemma, in TwoPoint.checkpoint]
link_path_cp [lemma, in TwoPoint.checkpoint]
link_seq_cp [lemma, in TwoPoint.checkpoint]
link_avoid [lemma, in TwoPoint.checkpoint]
link_cpN [lemma, in TwoPoint.checkpoint]
link_graph [definition, in TwoPoint.checkpoint]
link_irrefl [lemma, in TwoPoint.checkpoint]
link_sym [lemma, in TwoPoint.checkpoint]
link_rel [definition, in TwoPoint.checkpoint]
link_rel [abbreviation, in TwoPoint.extraction_def]
Link.T [variable, in TwoPoint.subalgebra]
Link.U [variable, in TwoPoint.subalgebra]
Link.U_disc [variable, in TwoPoint.subalgebra]
M
map_of_total [lemma, in TwoPoint.minor]Max [section, in TwoPoint.bounded]
max_mono [lemma, in TwoPoint.preliminaries]
Max.split [variable, in TwoPoint.bounded]
Max.split_lt [variable, in TwoPoint.bounded]
measure [abbreviation, in TwoPoint.extraction_def]
measure_lens_rest [lemma, in TwoPoint.extraction_def]
measure_remove_edges [lemma, in TwoPoint.extraction_def]
measure_split_cpM [lemma, in TwoPoint.extraction_def]
measure_split_cpR [lemma, in TwoPoint.extraction_def]
measure_split_cpL [lemma, in TwoPoint.extraction_def]
measure_lens [lemma, in TwoPoint.extraction_def]
measure_redirect [lemma, in TwoPoint.extraction_def]
measure_remove_component [lemma, in TwoPoint.extraction_def]
measure_igraph [lemma, in TwoPoint.extraction_def]
measure_node [lemma, in TwoPoint.extraction_def]
measure_subgraph [lemma, in TwoPoint.extraction_def]
measure_io [lemma, in TwoPoint.extraction_def]
measure_card [lemma, in TwoPoint.extraction_def]
memKset [lemma, in TwoPoint.preliminaries]
mem_cover [lemma, in TwoPoint.preliminaries]
mem_preim [lemma, in TwoPoint.preliminaries]
mem_catD [lemma, in TwoPoint.preliminaries]
mem_tail [lemma, in TwoPoint.preliminaries]
mem_cpl [lemma, in TwoPoint.checkpoint]
mem_edgep [lemma, in TwoPoint.sgraph]
mem_idp [lemma, in TwoPoint.sgraph]
mem_prev [lemma, in TwoPoint.sgraph]
mem_pcat [lemma, in TwoPoint.sgraph]
mem_pcatT [lemma, in TwoPoint.sgraph]
mem_path [lemma, in TwoPoint.sgraph]
merge [abbreviation, in TwoPoint.multigraph]
merge_congr [lemma, in TwoPoint.multigraph]
merge_def [definition, in TwoPoint.multigraph]
minor [definition, in TwoPoint.minor]
minor [library]
minor_exclusion_2p [lemma, in TwoPoint.extraction_iso]
minor_with [lemma, in TwoPoint.minor]
minor_induced_add_node [lemma, in TwoPoint.minor]
minor_K4_free [lemma, in TwoPoint.minor]
minor_trans [lemma, in TwoPoint.minor]
minor_map_comp [lemma, in TwoPoint.minor]
minor_of_map [lemma, in TwoPoint.minor]
minor_map [definition, in TwoPoint.minor]
multigraph [library]
N
nat_size_ind [lemma, in TwoPoint.preliminaries]ncp [definition, in TwoPoint.checkpoint]
ncpP [lemma, in TwoPoint.checkpoint]
ncp_interval [lemma, in TwoPoint.checkpoint]
ncp_bag [lemma, in TwoPoint.checkpoint]
ncp_CP [lemma, in TwoPoint.checkpoint]
ncp0 [lemma, in TwoPoint.checkpoint]
neighbours [definition, in TwoPoint.cp_minor]
nodes [definition, in TwoPoint.sgraph]
nodesE [lemma, in TwoPoint.sgraph]
nodes_start [lemma, in TwoPoint.sgraph]
nodes_end [lemma, in TwoPoint.sgraph]
nodes_eqE [lemma, in TwoPoint.sgraph]
notin_tail [lemma, in TwoPoint.preliminaries]
O
one2 [definition, in TwoPoint.subalgebra]ord_0Vp [lemma, in TwoPoint.extraction_iso]
ord1 [definition, in TwoPoint.preliminaries]
ord2 [definition, in TwoPoint.preliminaries]
ord3 [definition, in TwoPoint.preliminaries]
P
Pack [section, in TwoPoint.sgraph]Pack.G [variable, in TwoPoint.sgraph]
Pack.IPath [section, in TwoPoint.sgraph]
Pack.IPath.x [variable, in TwoPoint.sgraph]
Pack.IPath.y [variable, in TwoPoint.sgraph]
Pack.PathDef [section, in TwoPoint.sgraph]
Pack.PathDef.x [variable, in TwoPoint.sgraph]
Pack.PathDef.y [variable, in TwoPoint.sgraph]
Pack.PathTheory [section, in TwoPoint.sgraph]
Pack.PathTheory.p [variable, in TwoPoint.sgraph]
Pack.PathTheory.q [variable, in TwoPoint.sgraph]
Pack.PathTheory.x [variable, in TwoPoint.sgraph]
Pack.PathTheory.y [variable, in TwoPoint.sgraph]
Pack.PathTheory.z [variable, in TwoPoint.sgraph]
Pack.Primitives [section, in TwoPoint.sgraph]
Pack.Primitives.p [variable, in TwoPoint.sgraph]
Pack.Primitives.q [variable, in TwoPoint.sgraph]
Pack.Primitives.x [variable, in TwoPoint.sgraph]
Pack.Primitives.y [variable, in TwoPoint.sgraph]
Pack.Primitives.z [variable, in TwoPoint.sgraph]
partition_components [lemma, in TwoPoint.sgraph]
par2 [definition, in TwoPoint.subalgebra]
par2_assoc [lemma, in TwoPoint.tm_iso]
par2_idL [lemma, in TwoPoint.tm_iso]
par2_idR [lemma, in TwoPoint.tm_iso]
par2_injR [lemma, in TwoPoint.tm_iso]
par2_injL [lemma, in TwoPoint.tm_iso]
par2_LR [lemma, in TwoPoint.tm_iso]
par2_morphisem [instance, in TwoPoint.tm_iso]
par2_congr [lemma, in TwoPoint.tm_iso]
par2_eqvP [lemma, in TwoPoint.subalgebra]
par2_eqv_oo [lemma, in TwoPoint.subalgebra]
par2_eqv_ii [lemma, in TwoPoint.subalgebra]
par2_equiv_of [lemma, in TwoPoint.subalgebra]
par2_eq [definition, in TwoPoint.subalgebra]
par2_eqv_io [lemma, in TwoPoint.subalgebra]
par2_eqv_trans [definition, in TwoPoint.subalgebra]
par2_eqv_sym [lemma, in TwoPoint.subalgebra]
par2_eqv_refl [definition, in TwoPoint.subalgebra]
par2_eqv [definition, in TwoPoint.subalgebra]
Path [record, in TwoPoint.sgraph]
PathIndexing [section, in TwoPoint.sgraph]
PathIndexing.G [variable, in TwoPoint.sgraph]
PathIndexing.IDX [section, in TwoPoint.sgraph]
PathIndexing.IDX.dis_pq [variable, in TwoPoint.sgraph]
PathIndexing.IDX.irr_q [variable, in TwoPoint.sgraph]
PathIndexing.IDX.irr_p [variable, in TwoPoint.sgraph]
PathIndexing.IDX.irr_pq [variable, in TwoPoint.sgraph]
PathIndexing.IDX.p [variable, in TwoPoint.sgraph]
PathIndexing.IDX.q [variable, in TwoPoint.sgraph]
PathIndexing.IDX.x [variable, in TwoPoint.sgraph]
PathIndexing.IDX.y [variable, in TwoPoint.sgraph]
PathIndexing.IDX.z [variable, in TwoPoint.sgraph]
PathRP [lemma, in TwoPoint.sgraph]
path_restrict [lemma, in TwoPoint.preliminaries]
Path_from_induced [lemma, in TwoPoint.sgraph]
Path_to_induced [lemma, in TwoPoint.sgraph]
path_to_induced [lemma, in TwoPoint.sgraph]
Path_split [lemma, in TwoPoint.sgraph]
path_closed [lemma, in TwoPoint.sgraph]
Path_ind [lemma, in TwoPoint.sgraph]
Path_connect [lemma, in TwoPoint.sgraph]
path_last [lemma, in TwoPoint.sgraph]
Path_countMixin [definition, in TwoPoint.sgraph]
Path_choiceMixin [definition, in TwoPoint.sgraph]
Path_eqMixin [definition, in TwoPoint.sgraph]
path_srev [lemma, in TwoPoint.sgraph]
pblock_eqvE [lemma, in TwoPoint.preliminaries]
pcat [definition, in TwoPoint.sgraph]
pcat_proof [definition, in TwoPoint.sgraph]
pe_partition [definition, in TwoPoint.preliminaries]
pimset [definition, in TwoPoint.preliminaries]
pimsetP [lemma, in TwoPoint.preliminaries]
pimset_card [lemma, in TwoPoint.preliminaries]
pi_hom [lemma, in TwoPoint.skeleton]
point [definition, in TwoPoint.multigraph]
point_io [lemma, in TwoPoint.multigraph]
preim_omap_None [lemma, in TwoPoint.preliminaries]
preim_omap_Some [lemma, in TwoPoint.preliminaries]
preliminaries [library]
prev [definition, in TwoPoint.sgraph]
prevK [lemma, in TwoPoint.sgraph]
prev_irred [lemma, in TwoPoint.sgraph]
prev_inj [lemma, in TwoPoint.sgraph]
prev_proof [definition, in TwoPoint.sgraph]
project_path [lemma, in TwoPoint.preliminaries]
pval [projection, in TwoPoint.sgraph]
Q
Quotients [section, in TwoPoint.subalgebra]Quotients.G1 [variable, in TwoPoint.subalgebra]
Quotients.G2 [variable, in TwoPoint.subalgebra]
Quotients.P [variable, in TwoPoint.subalgebra]
R
rcons_spath [lemma, in TwoPoint.sgraph]rec_bag [lemma, in TwoPoint.extraction_def]
redirect [definition, in TwoPoint.extraction_def]
redirect_to [definition, in TwoPoint.extraction_def]
redirect_output_proof [lemma, in TwoPoint.extraction_def]
redirect_consistent [lemma, in TwoPoint.extraction_def]
redirect_proof1 [lemma, in TwoPoint.extraction_def]
relU_sym' [lemma, in TwoPoint.preliminaries]
rel0 [abbreviation, in TwoPoint.preliminaries]
rel0_sym [lemma, in TwoPoint.preliminaries]
rel0_irrefl [lemma, in TwoPoint.preliminaries]
remove_edges_restrict [lemma, in TwoPoint.skeleton]
remove_edges_cross [lemma, in TwoPoint.skeleton]
remove_edges_connected [lemma, in TwoPoint.skeleton]
remove_loops [lemma, in TwoPoint.skeleton]
remove_edges [definition, in TwoPoint.skeleton]
remove_component [lemma, in TwoPoint.sgraph]
rename [definition, in TwoPoint.sgraph]
rename_width [lemma, in TwoPoint.subalgebra]
rename_decomp [lemma, in TwoPoint.subalgebra]
rename_sdecomp [lemma, in TwoPoint.minor]
restrict [definition, in TwoPoint.preliminaries]
restrictE [lemma, in TwoPoint.preliminaries]
restrict_path [lemma, in TwoPoint.preliminaries]
restrict_mono [lemma, in TwoPoint.preliminaries]
restrict_upath [lemma, in TwoPoint.sgraph]
rev_inj [lemma, in TwoPoint.preliminaries]
rev_upath [lemma, in TwoPoint.sgraph]
S
sbag_conn [projection, in TwoPoint.minor]sbag_edge [projection, in TwoPoint.minor]
sbag_cover [projection, in TwoPoint.minor]
sc [definition, in TwoPoint.preliminaries]
sconnect_sym [lemma, in TwoPoint.sgraph]
sc_eq [lemma, in TwoPoint.preliminaries]
sc_sym [lemma, in TwoPoint.preliminaries]
sdecomp [record, in TwoPoint.minor]
SDecomp [constructor, in TwoPoint.minor]
sdecomp_sskel [lemma, in TwoPoint.subalgebra]
sdecomp_eq [lemma, in TwoPoint.minor]
sedge [projection, in TwoPoint.sgraph]
sedge_equiv_in [lemma, in TwoPoint.sgraph]
sedge_in_equiv [lemma, in TwoPoint.sgraph]
sedge_equiv [lemma, in TwoPoint.sgraph]
seq2 [definition, in TwoPoint.subalgebra]
seq2_assoc [lemma, in TwoPoint.tm_iso]
seq2_idL [lemma, in TwoPoint.tm_iso]
seq2_idR [lemma, in TwoPoint.tm_iso]
seq2_LR [lemma, in TwoPoint.tm_iso]
seq2_injR [lemma, in TwoPoint.tm_iso]
seq2_injL [lemma, in TwoPoint.tm_iso]
seq2_morphism [instance, in TwoPoint.tm_iso]
seq2_congr [lemma, in TwoPoint.tm_iso]
seq2_eqvP [lemma, in TwoPoint.subalgebra]
seq2_equiv_of [lemma, in TwoPoint.subalgebra]
seq2_eq [definition, in TwoPoint.subalgebra]
seq2_eqv_io [lemma, in TwoPoint.subalgebra]
seq2_eqv_trans [definition, in TwoPoint.subalgebra]
seq2_eqv_sym [lemma, in TwoPoint.subalgebra]
seq2_eqv_refl [definition, in TwoPoint.subalgebra]
seq2_eqv [definition, in TwoPoint.subalgebra]
setN01E [lemma, in TwoPoint.preliminaries]
setU1_mem [lemma, in TwoPoint.preliminaries]
set1_inj [lemma, in TwoPoint.preliminaries]
set2C [lemma, in TwoPoint.preliminaries]
SgIso [constructor, in TwoPoint.sgraph]
sgP [definition, in TwoPoint.sgraph]
sgraph [record, in TwoPoint.sgraph]
SGraph [constructor, in TwoPoint.sgraph]
sgraph [library]
sgraph_of_forest [projection, in TwoPoint.sgraph]
sg_iso_decomp [lemma, in TwoPoint.minor]
sg_iso_trans [lemma, in TwoPoint.sgraph]
sg_iso_sym [lemma, in TwoPoint.sgraph]
sg_iso_refl [lemma, in TwoPoint.sgraph]
sg_iso [inductive, in TwoPoint.sgraph]
sg_edgeNeq [lemma, in TwoPoint.sgraph]
sg_irrefl [projection, in TwoPoint.sgraph]
sg_sym [projection, in TwoPoint.sgraph]
sigraph [abbreviation, in TwoPoint.extraction_def]
SimplePaths [section, in TwoPoint.sgraph]
SimplePaths.G [variable, in TwoPoint.sgraph]
simple_check_point_wf [definition, in TwoPoint.extraction_def]
simple_check_point_term [definition, in TwoPoint.extraction_def]
sinterval [definition, in TwoPoint.checkpoint]
sintervalP2 [lemma, in TwoPoint.checkpoint]
sinterval_cp_cover [lemma, in TwoPoint.checkpoint]
sinterval_bag_cover [lemma, in TwoPoint.checkpoint]
sinterval_components [lemma, in TwoPoint.checkpoint]
sinterval_connectedL [lemma, in TwoPoint.checkpoint]
sinterval_connectL [lemma, in TwoPoint.checkpoint]
sinterval_noedge_cp [lemma, in TwoPoint.checkpoint]
sinterval_disj_cp [lemma, in TwoPoint.checkpoint]
sinterval_outside [lemma, in TwoPoint.checkpoint]
sinterval_exit [lemma, in TwoPoint.checkpoint]
sinterval_sub [lemma, in TwoPoint.checkpoint]
sinterval_bounds [lemma, in TwoPoint.checkpoint]
sinterval_sym [lemma, in TwoPoint.checkpoint]
sjoin [definition, in TwoPoint.sgraph]
skeleton [definition, in TwoPoint.skeleton]
skeleton [library]
skelP [lemma, in TwoPoint.skeleton]
skel_K4_free [lemma, in TwoPoint.subalgebra]
skel_union_join [lemma, in TwoPoint.subalgebra]
skel_sub [lemma, in TwoPoint.skeleton]
sk_rel_mergeE [lemma, in TwoPoint.skeleton]
sk_rel_irrefl [lemma, in TwoPoint.skeleton]
sk_rel_sym [lemma, in TwoPoint.skeleton]
sk_rel [definition, in TwoPoint.skeleton]
Some_eqE [lemma, in TwoPoint.preliminaries]
source [projection, in TwoPoint.multigraph]
source_proof [lemma, in TwoPoint.multigraph]
spath [definition, in TwoPoint.sgraph]
spathP [lemma, in TwoPoint.sgraph]
spathW [lemma, in TwoPoint.sgraph]
spathxx [lemma, in TwoPoint.sgraph]
spath_shorten [lemma, in TwoPoint.sgraph]
spath_split [inductive, in TwoPoint.sgraph]
spath_rev [lemma, in TwoPoint.sgraph]
spath_endD [lemma, in TwoPoint.sgraph]
spath_end [lemma, in TwoPoint.sgraph]
spath_concat [lemma, in TwoPoint.sgraph]
spath_cons [lemma, in TwoPoint.sgraph]
spath_cat [lemma, in TwoPoint.sgraph]
spath_rcons [lemma, in TwoPoint.sgraph]
spath_nil [lemma, in TwoPoint.sgraph]
spath_last [lemma, in TwoPoint.sgraph]
SplitCP [section, in TwoPoint.extraction_def]
SplitCP.CK4F_G [variable, in TwoPoint.extraction_def]
SplitCP.G [variable, in TwoPoint.extraction_def]
SplitCP.Hio [variable, in TwoPoint.extraction_def]
SplitCP.Hz [variable, in TwoPoint.extraction_def]
SplitCP.Hz' [variable, in TwoPoint.extraction_def]
SplitCP.z [variable, in TwoPoint.extraction_def]
SplitCP.Zi [variable, in TwoPoint.extraction_def]
SplitCP.Zo [variable, in TwoPoint.extraction_def]
splitL [lemma, in TwoPoint.sgraph]
splitR [lemma, in TwoPoint.sgraph]
split_pip [lemma, in TwoPoint.extraction_iso]
split_io_edges [lemma, in TwoPoint.extraction_iso]
split_cp [lemma, in TwoPoint.extraction_iso]
split_component [lemma, in TwoPoint.extraction_iso]
split_at_first [lemma, in TwoPoint.sgraph]
split_at_first_aux [lemma, in TwoPoint.sgraph]
split_K4_nontrivial [lemma, in TwoPoint.extraction_def]
srestrict [definition, in TwoPoint.sgraph]
srestrict_sym [lemma, in TwoPoint.sgraph]
srev [definition, in TwoPoint.sgraph]
srevK [lemma, in TwoPoint.sgraph]
srev_nodes [lemma, in TwoPoint.sgraph]
srev_rcons [lemma, in TwoPoint.sgraph]
sskeleton [definition, in TwoPoint.skeleton]
sskeleton_remove_io [lemma, in TwoPoint.skeleton]
sskeleton_adjacent [lemma, in TwoPoint.skeleton]
sskeleton_subgraph_for [lemma, in TwoPoint.skeleton]
sskeleton_add [lemma, in TwoPoint.extraction_def]
sskelP [lemma, in TwoPoint.skeleton]
sskel_K4_free [lemma, in TwoPoint.subalgebra]
SSplit [constructor, in TwoPoint.sgraph]
ssplitP [lemma, in TwoPoint.sgraph]
ssplit_K4_nontrivial [lemma, in TwoPoint.cp_minor]
ssplit_disconnected [lemma, in TwoPoint.sgraph]
strict_is_minor [lemma, in TwoPoint.minor]
strict_minor [definition, in TwoPoint.minor]
strip [definition, in TwoPoint.extraction_iso]
subalgebra [library]
subcp [lemma, in TwoPoint.checkpoint]
subgraph [definition, in TwoPoint.multigraph]
subgraph [definition, in TwoPoint.sgraph]
Subgraphs [section, in TwoPoint.multigraph]
Subgraphs.E [variable, in TwoPoint.multigraph]
Subgraphs.G [variable, in TwoPoint.multigraph]
Subgraphs.in_V [variable, in TwoPoint.multigraph]
Subgraphs.V [variable, in TwoPoint.multigraph]
subgraph_for_iso [lemma, in TwoPoint.multigraph]
subgraph_sub [lemma, in TwoPoint.multigraph]
subgraph_for [definition, in TwoPoint.multigraph]
subgraph_K4_free [lemma, in TwoPoint.minor]
subrel_restrict [lemma, in TwoPoint.preliminaries]
subset_seqL [lemma, in TwoPoint.preliminaries]
subset_seqR [lemma, in TwoPoint.preliminaries]
subset_cons [lemma, in TwoPoint.preliminaries]
subset_pcatR [lemma, in TwoPoint.sgraph]
subset_pcatL [lemma, in TwoPoint.sgraph]
sub_equiv_of [lemma, in TwoPoint.preliminaries]
sub_restrict_connect [lemma, in TwoPoint.preliminaries]
sub_trans [lemma, in TwoPoint.preliminaries]
sub_connect [lemma, in TwoPoint.preliminaries]
sub_in11W [lemma, in TwoPoint.preliminaries]
sub_val_eq [lemma, in TwoPoint.preliminaries]
sub_edge [definition, in TwoPoint.multigraph]
sub_vertex [definition, in TwoPoint.multigraph]
sub_inr [lemma, in TwoPoint.subalgebra]
sub_inl [lemma, in TwoPoint.subalgebra]
sub_sub [lemma, in TwoPoint.skeleton]
sub_pointxx [lemma, in TwoPoint.skeleton]
sub_minor [lemma, in TwoPoint.minor]
sub_forest [lemma, in TwoPoint.sgraph]
sum_eqE [definition, in TwoPoint.preliminaries]
sunit [definition, in TwoPoint.sgraph]
surjective [definition, in TwoPoint.preliminaries]
surjective2 [definition, in TwoPoint.multigraph]
svertex [projection, in TwoPoint.sgraph]
sym [definition, in TwoPoint.multigraph]
symmetric_restrict [lemma, in TwoPoint.preliminaries]
symmetric_restrict_sedge [lemma, in TwoPoint.sgraph]
sym_eqv [lemma, in TwoPoint.extraction_iso]
sym0 [definition, in TwoPoint.multigraph]
sym2 [definition, in TwoPoint.subalgebra]
sym2b [definition, in TwoPoint.extraction_iso]
sym2b' [definition, in TwoPoint.extraction_iso]
sym2_ [definition, in TwoPoint.extraction_iso]
T
tail [definition, in TwoPoint.sgraph]tailW [lemma, in TwoPoint.sgraph]
take_find [lemma, in TwoPoint.preliminaries]
target [projection, in TwoPoint.multigraph]
target_proof [lemma, in TwoPoint.multigraph]
term [inductive, in TwoPoint.subalgebra]
term_of_iso [lemma, in TwoPoint.extraction_iso]
term_of_eq [lemma, in TwoPoint.extraction_def]
term_of_rec_eq [lemma, in TwoPoint.extraction_def]
term_of [definition, in TwoPoint.extraction_def]
term_of_rec [definition, in TwoPoint.extraction_def]
term_of_measure [definition, in TwoPoint.extraction_def]
the_uPathP [lemma, in TwoPoint.checkpoint]
the_uPath [definition, in TwoPoint.checkpoint]
the_uPath_proof [lemma, in TwoPoint.checkpoint]
three_way_split [lemma, in TwoPoint.sgraph]
tjoin [definition, in TwoPoint.subalgebra]
tlink [definition, in TwoPoint.subalgebra]
tmA [constructor, in TwoPoint.subalgebra]
tmC [constructor, in TwoPoint.subalgebra]
tmD [constructor, in TwoPoint.subalgebra]
tmEs [definition, in TwoPoint.extraction_def]
tmI [constructor, in TwoPoint.subalgebra]
tmS [constructor, in TwoPoint.subalgebra]
tmT [constructor, in TwoPoint.subalgebra]
tm_ [definition, in TwoPoint.extraction_def]
tm_iso [library]
tm1 [constructor, in TwoPoint.subalgebra]
tnth_cons [lemma, in TwoPoint.preliminaries]
tnth_map_in [lemma, in TwoPoint.preliminaries]
top2 [definition, in TwoPoint.subalgebra]
total_minor_map [definition, in TwoPoint.minor]
treeI [lemma, in TwoPoint.sgraph]
trivIset3 [lemma, in TwoPoint.preliminaries]
triv_decomp [definition, in TwoPoint.subalgebra]
triv_sdecomp [definition, in TwoPoint.minor]
tunit [definition, in TwoPoint.sgraph]
tuple_UPath [definition, in TwoPoint.sgraph]
two_graph [definition, in TwoPoint.subalgebra]
TW2_K4_free [lemma, in TwoPoint.minor]
U
uncycle [lemma, in TwoPoint.sgraph]union [definition, in TwoPoint.multigraph]
union_congr [lemma, in TwoPoint.multigraph]
unique [definition, in TwoPoint.preliminaries]
unique_forestT [lemma, in TwoPoint.sgraph]
unit_graph [definition, in TwoPoint.subalgebra]
unit_forest [definition, in TwoPoint.sgraph]
UPath [record, in TwoPoint.sgraph]
upath [definition, in TwoPoint.sgraph]
Upath [section, in TwoPoint.sgraph]
uPathP [lemma, in TwoPoint.sgraph]
upathP [lemma, in TwoPoint.sgraph]
upathPR [lemma, in TwoPoint.sgraph]
uPathRP [lemma, in TwoPoint.sgraph]
UPathW [definition, in TwoPoint.sgraph]
upathW [lemma, in TwoPoint.sgraph]
upathWW [lemma, in TwoPoint.sgraph]
UPath_from_irred [lemma, in TwoPoint.sgraph]
upath_of [definition, in TwoPoint.sgraph]
upath_irred [lemma, in TwoPoint.sgraph]
UPath_finMixin [definition, in TwoPoint.sgraph]
UPath_tupleK [lemma, in TwoPoint.sgraph]
UPath_tuple [definition, in TwoPoint.sgraph]
UPath_countMixin [definition, in TwoPoint.sgraph]
UPath_choiceMixin [definition, in TwoPoint.sgraph]
UPath_eqMixin [definition, in TwoPoint.sgraph]
upath_nil [lemma, in TwoPoint.sgraph]
upath_consE [lemma, in TwoPoint.sgraph]
upath_cons [lemma, in TwoPoint.sgraph]
upath_sym [lemma, in TwoPoint.sgraph]
upath_size [lemma, in TwoPoint.sgraph]
upath_uniq [lemma, in TwoPoint.sgraph]
Upath.G [variable, in TwoPoint.sgraph]
USplit [constructor, in TwoPoint.sgraph]
usplit [inductive, in TwoPoint.sgraph]
usplitP [lemma, in TwoPoint.sgraph]
uval [projection, in TwoPoint.sgraph]
V
vertex [projection, in TwoPoint.multigraph]vfun [abbreviation, in TwoPoint.subalgebra]
void [inductive, in TwoPoint.preliminaries]
void_enumP [lemma, in TwoPoint.preliminaries]
void_countMixin [definition, in TwoPoint.preliminaries]
void_choiceMixin [definition, in TwoPoint.preliminaries]
void_pcancel [lemma, in TwoPoint.preliminaries]
void_eqP [lemma, in TwoPoint.preliminaries]
W
wf_leq [lemma, in TwoPoint.preliminaries]width [definition, in TwoPoint.sgraph]
width_link [lemma, in TwoPoint.subalgebra]
width_minor [lemma, in TwoPoint.minor]
width_bound [lemma, in TwoPoint.sgraph]
_
_symbols [lemma, in TwoPoint.multigraph]other
_ @^-1 _ (set_scope) [notation, in TwoPoint.preliminaries]_ ≈ _ [notation, in TwoPoint.multigraph]
_ ⋄ _ [notation, in TwoPoint.checkpoint]
_ <[ _ ] _ [notation, in TwoPoint.sgraph]
_ -- _ [notation, in TwoPoint.sgraph]
_ :o: _ [notation, in TwoPoint.extraction_def]
_ :||: _ [notation, in TwoPoint.extraction_def]
'K_ _ [notation, in TwoPoint.minor]
[ disjoint3 _ & _ & _ ] [notation, in TwoPoint.preliminaries]
\pi _ [notation, in TwoPoint.tm_iso]
\pi _ [notation, in TwoPoint.extraction_iso]
Notation Index
C
_ ⋄ _ [in TwoPoint.checkpoint]other
_ @^-1 _ (set_scope) [in TwoPoint.preliminaries]_ ≈ _ [in TwoPoint.multigraph]
_ ⋄ _ [in TwoPoint.checkpoint]
_ <[ _ ] _ [in TwoPoint.sgraph]
_ -- _ [in TwoPoint.sgraph]
_ :o: _ [in TwoPoint.extraction_def]
_ :||: _ [in TwoPoint.extraction_def]
'K_ _ [in TwoPoint.minor]
[ disjoint3 _ & _ & _ ] [in TwoPoint.preliminaries]
\pi _ [in TwoPoint.tm_iso]
\pi _ [in TwoPoint.extraction_iso]
Variable Index
A
AddNode.G [in TwoPoint.minor]AddNode.N [in TwoPoint.minor]
B
Bounded.aT [in TwoPoint.bounded]Bounded.F [in TwoPoint.bounded]
Bounded.F_wf [in TwoPoint.bounded]
Bounded.measure [in TwoPoint.bounded]
Bounded.P [in TwoPoint.bounded]
Bounded.rT [in TwoPoint.bounded]
Bounded.x0 [in TwoPoint.bounded]
C
CheckpointOrder.conn_io [in TwoPoint.checkpoint]CheckpointOrder.G [in TwoPoint.checkpoint]
CheckpointOrder.i [in TwoPoint.checkpoint]
CheckpointOrder.o [in TwoPoint.checkpoint]
CheckpointsAndMinors.conn_G [in TwoPoint.cp_minor]
CheckpointsAndMinors.G [in TwoPoint.cp_minor]
CheckPoints.G [in TwoPoint.checkpoint]
CheckPoints.G_conn [in TwoPoint.checkpoint]
CheckPoints.G_conn' [in TwoPoint.checkpoint]
D
DecompTheory.B [in TwoPoint.minor]DecompTheory.decD [in TwoPoint.minor]
DecompTheory.G [in TwoPoint.minor]
DecompTheory.T [in TwoPoint.minor]
Disjoint3.A [in TwoPoint.preliminaries]
Disjoint3.B [in TwoPoint.preliminaries]
Disjoint3.C [in TwoPoint.preliminaries]
Disjoint3.T [in TwoPoint.preliminaries]
E
Equivalence.e [in TwoPoint.preliminaries]Equivalence.T [in TwoPoint.preliminaries]
F
FinEncodingModuloRel.C [in TwoPoint.finite_quotient]FinEncodingModuloRel.CD [in TwoPoint.finite_quotient]
FinEncodingModuloRel.D [in TwoPoint.finite_quotient]
FinEncodingModuloRel.DC [in TwoPoint.finite_quotient]
FinEncodingModuloRel.eD [in TwoPoint.finite_quotient]
FinEncodingModuloRel.encD [in TwoPoint.finite_quotient]
Foldr1.F [in TwoPoint.preliminaries]
Foldr1.I [in TwoPoint.preliminaries]
Foldr1.op [in TwoPoint.preliminaries]
Foldr1.R [in TwoPoint.preliminaries]
Forests.G [in TwoPoint.sgraph]
I
InducedSubgraph.G [in TwoPoint.sgraph]InducedSubgraph.S [in TwoPoint.sgraph]
J
JoinSG.G1 [in TwoPoint.sgraph]JoinSG.G2 [in TwoPoint.sgraph]
JoinT.T1 [in TwoPoint.subalgebra]
JoinT.T2 [in TwoPoint.subalgebra]
L
Link.T [in TwoPoint.subalgebra]Link.U [in TwoPoint.subalgebra]
Link.U_disc [in TwoPoint.subalgebra]
M
Max.split [in TwoPoint.bounded]Max.split_lt [in TwoPoint.bounded]
P
Pack.G [in TwoPoint.sgraph]Pack.IPath.x [in TwoPoint.sgraph]
Pack.IPath.y [in TwoPoint.sgraph]
Pack.PathDef.x [in TwoPoint.sgraph]
Pack.PathDef.y [in TwoPoint.sgraph]
Pack.PathTheory.p [in TwoPoint.sgraph]
Pack.PathTheory.q [in TwoPoint.sgraph]
Pack.PathTheory.x [in TwoPoint.sgraph]
Pack.PathTheory.y [in TwoPoint.sgraph]
Pack.PathTheory.z [in TwoPoint.sgraph]
Pack.Primitives.p [in TwoPoint.sgraph]
Pack.Primitives.q [in TwoPoint.sgraph]
Pack.Primitives.x [in TwoPoint.sgraph]
Pack.Primitives.y [in TwoPoint.sgraph]
Pack.Primitives.z [in TwoPoint.sgraph]
PathIndexing.G [in TwoPoint.sgraph]
PathIndexing.IDX.dis_pq [in TwoPoint.sgraph]
PathIndexing.IDX.irr_q [in TwoPoint.sgraph]
PathIndexing.IDX.irr_p [in TwoPoint.sgraph]
PathIndexing.IDX.irr_pq [in TwoPoint.sgraph]
PathIndexing.IDX.p [in TwoPoint.sgraph]
PathIndexing.IDX.q [in TwoPoint.sgraph]
PathIndexing.IDX.x [in TwoPoint.sgraph]
PathIndexing.IDX.y [in TwoPoint.sgraph]
PathIndexing.IDX.z [in TwoPoint.sgraph]
Q
Quotients.G1 [in TwoPoint.subalgebra]Quotients.G2 [in TwoPoint.subalgebra]
Quotients.P [in TwoPoint.subalgebra]
S
SimplePaths.G [in TwoPoint.sgraph]SplitCP.CK4F_G [in TwoPoint.extraction_def]
SplitCP.G [in TwoPoint.extraction_def]
SplitCP.Hio [in TwoPoint.extraction_def]
SplitCP.Hz [in TwoPoint.extraction_def]
SplitCP.Hz' [in TwoPoint.extraction_def]
SplitCP.z [in TwoPoint.extraction_def]
SplitCP.Zi [in TwoPoint.extraction_def]
SplitCP.Zo [in TwoPoint.extraction_def]
Subgraphs.E [in TwoPoint.multigraph]
Subgraphs.G [in TwoPoint.multigraph]
Subgraphs.in_V [in TwoPoint.multigraph]
Subgraphs.V [in TwoPoint.multigraph]
U
Upath.G [in TwoPoint.sgraph]Library Index
B
boundedC
checkpointcp_minor
E
edoneextraction_iso
extraction_def
F
finite_quotientM
minormultigraph
P
preliminariesS
sgraphskeleton
subalgebra
T
tm_isoLemma Index
A
add_edge_induced_iso [in TwoPoint.cp_minor]add_edge_swap [in TwoPoint.cp_minor]
add_node_minor [in TwoPoint.minor]
add_node_complete [in TwoPoint.minor]
add_node_lift_Path [in TwoPoint.minor]
add_node_irrefl [in TwoPoint.minor]
add_node_sym [in TwoPoint.minor]
add_edge_connected [in TwoPoint.sgraph]
add_edge_Path [in TwoPoint.sgraph]
add_edge_irrefl [in TwoPoint.sgraph]
add_edge_sym [in TwoPoint.sgraph]
adjacentI [in TwoPoint.skeleton]
adjacentP [in TwoPoint.skeleton]
adjacent_induced [in TwoPoint.skeleton]
adjacent_edge [in TwoPoint.skeleton]
adjacent_sym [in TwoPoint.skeleton]
all_cons [in TwoPoint.preliminaries]
B
bagP [in TwoPoint.checkpoint]bagPn [in TwoPoint.checkpoint]
bags_in_out [in TwoPoint.checkpoint]
bag_cp [in TwoPoint.checkpoint]
bag_disj [in TwoPoint.checkpoint]
bag_extension [in TwoPoint.checkpoint]
bag_in_out [in TwoPoint.checkpoint]
bag_exit_edge [in TwoPoint.checkpoint]
bag_exit' [in TwoPoint.checkpoint]
bag_exit [in TwoPoint.checkpoint]
bag_sub_sinterval [in TwoPoint.checkpoint]
bag_nontrivial [in TwoPoint.checkpoint]
bag_id [in TwoPoint.checkpoint]
bag_edges_disj [in TwoPoint.skeleton]
bgraph_eq_io [in TwoPoint.skeleton]
bigcup_set1 [in TwoPoint.preliminaries]
big_iso_congr [in TwoPoint.tm_iso]
big_seq2_maps [in TwoPoint.tm_iso]
big_seq2_map [in TwoPoint.tm_iso]
big_seq2_congrs [in TwoPoint.tm_iso]
big_seq2_congr [in TwoPoint.tm_iso]
big_seq2_cons [in TwoPoint.tm_iso]
big_par2_congrs [in TwoPoint.tm_iso]
big_par2_congr [in TwoPoint.tm_iso]
big_par2_cat [in TwoPoint.tm_iso]
big_par2_map [in TwoPoint.tm_iso]
big_par2_1 [in TwoPoint.tm_iso]
big_par2_cons [in TwoPoint.tm_iso]
big_enum_in [in TwoPoint.preliminaries]
bij_surj [in TwoPoint.preliminaries]
C
can_irred_of [in TwoPoint.sgraph]cardsCT [in TwoPoint.preliminaries]
cardsI [in TwoPoint.preliminaries]
cards3 [in TwoPoint.preliminaries]
card_void [in TwoPoint.preliminaries]
card_le1P [in TwoPoint.preliminaries]
card_gt1P [in TwoPoint.preliminaries]
card_le1 [in TwoPoint.preliminaries]
card_ltnT [in TwoPoint.preliminaries]
card_val [in TwoPoint.skeleton]
card1P [in TwoPoint.preliminaries]
card12 [in TwoPoint.preliminaries]
CK4F_lens_rest [in TwoPoint.extraction_def]
CK4F_remove_loops [in TwoPoint.extraction_def]
CK4F_remove_edges [in TwoPoint.extraction_def]
CK4F_split_cpM [in TwoPoint.extraction_def]
CK4F_split_cpR [in TwoPoint.extraction_def]
CK4F_split_cpL [in TwoPoint.extraction_def]
CK4F_lens [in TwoPoint.extraction_def]
CK4F_redirect [in TwoPoint.extraction_def]
CK4F_one [in TwoPoint.extraction_def]
CK4F_remove_component [in TwoPoint.extraction_def]
CK4F_induced2 [in TwoPoint.extraction_def]
CK4F_sub [in TwoPoint.extraction_def]
CK4F_igraph [in TwoPoint.extraction_def]
clique1 [in TwoPoint.sgraph]
clique2 [in TwoPoint.sgraph]
codom_Some [in TwoPoint.preliminaries]
collapse_bags [in TwoPoint.cp_minor]
complete_irrefl [in TwoPoint.minor]
complete_sym [in TwoPoint.minor]
componentless_top [in TwoPoint.extraction_iso]
componentless_one [in TwoPoint.extraction_iso]
components_pblockP [in TwoPoint.sgraph]
component_exit [in TwoPoint.sgraph]
comp_dom2_redirect [in TwoPoint.extraction_iso]
comp_exit [in TwoPoint.extraction_iso]
connectedP [in TwoPoint.sgraph]
connectedTE [in TwoPoint.sgraph]
connectedTI [in TwoPoint.sgraph]
connectedU_edge [in TwoPoint.sgraph]
connected_remove_triv_bag2 [in TwoPoint.cp_minor]
connected_bag [in TwoPoint.checkpoint]
connected_interval [in TwoPoint.checkpoint]
connected_CP_closed [in TwoPoint.checkpoint]
connected_cp_closed [in TwoPoint.checkpoint]
connected_igraph [in TwoPoint.skeleton]
connected_bgraph [in TwoPoint.skeleton]
connected_skeleton [in TwoPoint.skeleton]
connected_skeleton' [in TwoPoint.skeleton]
connected_add_node [in TwoPoint.minor]
connected_in_components [in TwoPoint.sgraph]
connected_center [in TwoPoint.sgraph]
connected_card_gt1 [in TwoPoint.sgraph]
connected_induced [in TwoPoint.sgraph]
connected_in_subgraph [in TwoPoint.sgraph]
connected_path [in TwoPoint.sgraph]
connected_restrict [in TwoPoint.sgraph]
connected_component_set [in TwoPoint.extraction_def]
connected_induced [in TwoPoint.extraction_def]
connected1 [in TwoPoint.sgraph]
connected2 [in TwoPoint.sgraph]
connectRI [in TwoPoint.sgraph]
connectUP [in TwoPoint.preliminaries]
connect_img [in TwoPoint.preliminaries]
connect_symI [in TwoPoint.preliminaries]
connect_mono [in TwoPoint.preliminaries]
connect_restrict_case [in TwoPoint.sgraph]
consistentT [in TwoPoint.extraction_def]
consistent_setD [in TwoPoint.skeleton]
const0_eq [in TwoPoint.bounded]
cpNI [in TwoPoint.checkpoint]
cpN_trans [in TwoPoint.checkpoint]
cpo_cp [in TwoPoint.checkpoint]
cpo_max [in TwoPoint.checkpoint]
cpo_min [in TwoPoint.checkpoint]
cpo_order [in TwoPoint.checkpoint]
cpo_antisym [in TwoPoint.checkpoint]
cpo_total [in TwoPoint.checkpoint]
cpo_trans [in TwoPoint.checkpoint]
cpo_refl [in TwoPoint.checkpoint]
cpP [in TwoPoint.checkpoint]
cpPn [in TwoPoint.checkpoint]
cpTI [in TwoPoint.checkpoint]
cpxx [in TwoPoint.checkpoint]
CP_tree [in TwoPoint.cp_minor]
CP_treeI [in TwoPoint.checkpoint]
CP_triangle_bags [in TwoPoint.checkpoint]
CP_bags [in TwoPoint.checkpoint]
CP_tree_sinterval [in TwoPoint.checkpoint]
cp_sub_interval [in TwoPoint.checkpoint]
CP_tree_paths [in TwoPoint.checkpoint]
CP_connected [in TwoPoint.checkpoint]
CP_path [in TwoPoint.checkpoint]
CP_clique [in TwoPoint.checkpoint]
CP_base [in TwoPoint.checkpoint]
CP_closed [in TwoPoint.checkpoint]
CP_mono [in TwoPoint.checkpoint]
CP_extensive [in TwoPoint.checkpoint]
CP_set2 [in TwoPoint.checkpoint]
cp_neighbours [in TwoPoint.checkpoint]
cp_tighten [in TwoPoint.checkpoint]
cp_tightenR [in TwoPoint.checkpoint]
cp_widen [in TwoPoint.checkpoint]
cp_widenR [in TwoPoint.checkpoint]
cp_mid [in TwoPoint.checkpoint]
cp_triangle [in TwoPoint.checkpoint]
cp_sym [in TwoPoint.checkpoint]
crK [in TwoPoint.preliminaries]
cycle_clique [in TwoPoint.checkpoint]
C3_of_triangle [in TwoPoint.cp_minor]
D
decomp_small [in TwoPoint.subalgebra]decomp_dom [in TwoPoint.subalgebra]
decomp_cnv [in TwoPoint.subalgebra]
decomp_seq2 [in TwoPoint.subalgebra]
decomp_par2 [in TwoPoint.subalgebra]
decomp_quot [in TwoPoint.subalgebra]
decomp_link [in TwoPoint.subalgebra]
decomp_clique [in TwoPoint.minor]
disconnectedE [in TwoPoint.sgraph]
disjointE [in TwoPoint.preliminaries]
disjointFl [in TwoPoint.preliminaries]
disjointFr [in TwoPoint.preliminaries]
disjointNI [in TwoPoint.preliminaries]
disjoint_transR [in TwoPoint.preliminaries]
disjoint_edgep [in TwoPoint.sgraph]
disjoint3P [in TwoPoint.preliminaries]
E
edgeless_bag [in TwoPoint.extraction_def]edgep_proof [in TwoPoint.sgraph]
edges_st [in TwoPoint.extraction_iso]
edges2_graph_of [in TwoPoint.extraction_iso]
edges2_big [in TwoPoint.extraction_iso]
edges2_cons [in TwoPoint.extraction_iso]
edges2_nil [in TwoPoint.extraction_iso]
edge_in_set [in TwoPoint.multigraph]
edge_set1 [in TwoPoint.multigraph]
edge_set_adj [in TwoPoint.skeleton]
emb_surj [in TwoPoint.preliminaries]
empty_uniqe [in TwoPoint.preliminaries]
equivalence_partition_gt1P [in TwoPoint.preliminaries]
equivalence_rel_of_sym [in TwoPoint.preliminaries]
equiv_of_sym [in TwoPoint.preliminaries]
eq_set1P [in TwoPoint.preliminaries]
eq_quot_finMixin [in TwoPoint.finite_quotient]
F
Fix_eq [in TwoPoint.bounded]flesh_out [in TwoPoint.skeleton]
foldr1_set_default [in TwoPoint.preliminaries]
foo_eq [in TwoPoint.bounded]
forestI [in TwoPoint.sgraph]
forestP [in TwoPoint.sgraph]
forestT_unique [in TwoPoint.sgraph]
fun_decompose [in TwoPoint.preliminaries]
F_rec_narrow [in TwoPoint.bounded]
G
get_edge [in TwoPoint.extraction_def]graph_of_big_tmIs [in TwoPoint.tm_iso]
graph_of_big_tmI [in TwoPoint.tm_iso]
graph_minor_TW2 [in TwoPoint.extraction_iso]
graph_of_TW2 [in TwoPoint.subalgebra]
H
has_edge [in TwoPoint.skeleton]hom_of_surj [in TwoPoint.multigraph]
hom_gI [in TwoPoint.multigraph]
hom_eqL [in TwoPoint.subalgebra]
hom2_sskel [in TwoPoint.skeleton]
I
idxR [in TwoPoint.sgraph]idx_swap [in TwoPoint.sgraph]
idx_srev [in TwoPoint.sgraph]
idx_nLR [in TwoPoint.sgraph]
idx_inj [in TwoPoint.sgraph]
idx_catR [in TwoPoint.sgraph]
idx_catL [in TwoPoint.sgraph]
idx_end [in TwoPoint.sgraph]
idx_start [in TwoPoint.sgraph]
idx_mem [in TwoPoint.sgraph]
id_surj [in TwoPoint.preliminaries]
id_bij [in TwoPoint.preliminaries]
igraph_K4F_add_node [in TwoPoint.cp_minor]
igraph_K4F [in TwoPoint.cp_minor]
igraph_proof [in TwoPoint.skeleton]
imset_valT [in TwoPoint.preliminaries]
imset_pre_val [in TwoPoint.preliminaries]
index_rev [in TwoPoint.sgraph]
index_rcons [in TwoPoint.sgraph]
induced_sub [in TwoPoint.multigraph]
induced_minor [in TwoPoint.minor]
induced_path [in TwoPoint.sgraph]
induced_sub [in TwoPoint.sgraph]
induced_irrefl [in TwoPoint.sgraph]
induced_sym [in TwoPoint.sgraph]
induced_K4_free [in TwoPoint.extraction_def]
induced2_induced [in TwoPoint.multigraph]
inj_imset [in TwoPoint.preliminaries]
inj_omap [in TwoPoint.preliminaries]
inl_codom_inr [in TwoPoint.preliminaries]
inl_inj [in TwoPoint.preliminaries]
inl_eqE [in TwoPoint.preliminaries]
inr_codom_inl [in TwoPoint.preliminaries]
inr_inj [in TwoPoint.preliminaries]
inr_eqE [in TwoPoint.preliminaries]
ins [in TwoPoint.cp_minor]
intervalI_cp [in TwoPoint.checkpoint]
intervalL [in TwoPoint.checkpoint]
intervalR [in TwoPoint.checkpoint]
interval_edge_cp [in TwoPoint.checkpoint]
interval_cp_cover [in TwoPoint.checkpoint]
interval_bag_disj [in TwoPoint.checkpoint]
interval_sym [in TwoPoint.checkpoint]
interval_cp_edge_cover [in TwoPoint.skeleton]
interval_bag_edge_cover [in TwoPoint.skeleton]
interval_edges_disj_cp [in TwoPoint.skeleton]
interval_bag_edges_disj [in TwoPoint.skeleton]
interval_edges_sym [in TwoPoint.skeleton]
in_tail [in TwoPoint.sgraph]
irredE [in TwoPoint.sgraph]
irredxx [in TwoPoint.sgraph]
irred_ind [in TwoPoint.sgraph]
irred_edgeL [in TwoPoint.sgraph]
irred_edge [in TwoPoint.sgraph]
irred_id [in TwoPoint.sgraph]
irred_rev [in TwoPoint.sgraph]
irred_cat' [in TwoPoint.sgraph]
irred_cat [in TwoPoint.sgraph]
irred_nodes [in TwoPoint.sgraph]
irred_upath [in TwoPoint.sgraph]
irreflexive_restrict [in TwoPoint.sgraph]
iso_one [in TwoPoint.tm_iso]
iso_top [in TwoPoint.tm_iso]
iso_split_par2 [in TwoPoint.tm_iso]
iso_of_iso2 [in TwoPoint.multigraph]
iso_pointxx [in TwoPoint.skeleton]
iso_K4_free [in TwoPoint.minor]
iso_strict_minor [in TwoPoint.minor]
iso_connected [in TwoPoint.sgraph]
iso_subgraph [in TwoPoint.sgraph]
iso2_union [in TwoPoint.multigraph]
iso2_point [in TwoPoint.multigraph]
iso2_inv_out [in TwoPoint.multigraph]
iso2_inv_in [in TwoPoint.multigraph]
iso2_refl [in TwoPoint.multigraph]
iso2_sym [in TwoPoint.multigraph]
iso2_inv [in TwoPoint.multigraph]
iso2_trans [in TwoPoint.multigraph]
iso2_of_iso [in TwoPoint.multigraph]
iso2_decomp [in TwoPoint.skeleton]
iso2_sskel [in TwoPoint.skeleton]
iso2_skel [in TwoPoint.skeleton]
isplitP [in TwoPoint.sgraph]
is_forestP [in TwoPoint.sgraph]
J
join_width [in TwoPoint.subalgebra]join_decomp [in TwoPoint.subalgebra]
join_is_forest [in TwoPoint.subalgebra]
join_disc [in TwoPoint.sgraph]
join_rel_irrefl [in TwoPoint.sgraph]
join_rel_sym [in TwoPoint.sgraph]
K
K4_of_triangle [in TwoPoint.cp_minor]K4_width [in TwoPoint.minor]
K4_bag [in TwoPoint.minor]
L
last_belast_eq [in TwoPoint.preliminaries]last_take [in TwoPoint.preliminaries]
last_rev_belast [in TwoPoint.sgraph]
lens_components [in TwoPoint.extraction_def]
lens_sinterval [in TwoPoint.extraction_def]
lens_io_set [in TwoPoint.extraction_def]
leq_subn [in TwoPoint.preliminaries]
lift_equiv [in TwoPoint.preliminaries]
lift_path [in TwoPoint.preliminaries]
lift_Path [in TwoPoint.sgraph]
lift_upath [in TwoPoint.sgraph]
lift_spath [in TwoPoint.sgraph]
linkNeq [in TwoPoint.cp_minor]
link_is_forest [in TwoPoint.subalgebra]
link_has_None [in TwoPoint.subalgebra]
link_unique_None [in TwoPoint.subalgebra]
link_bypass [in TwoPoint.subalgebra]
link_unique_lift [in TwoPoint.subalgebra]
link_cycle [in TwoPoint.checkpoint]
link_path_cp [in TwoPoint.checkpoint]
link_seq_cp [in TwoPoint.checkpoint]
link_avoid [in TwoPoint.checkpoint]
link_cpN [in TwoPoint.checkpoint]
link_irrefl [in TwoPoint.checkpoint]
link_sym [in TwoPoint.checkpoint]
M
map_of_total [in TwoPoint.minor]max_mono [in TwoPoint.preliminaries]
measure_lens_rest [in TwoPoint.extraction_def]
measure_remove_edges [in TwoPoint.extraction_def]
measure_split_cpM [in TwoPoint.extraction_def]
measure_split_cpR [in TwoPoint.extraction_def]
measure_split_cpL [in TwoPoint.extraction_def]
measure_lens [in TwoPoint.extraction_def]
measure_redirect [in TwoPoint.extraction_def]
measure_remove_component [in TwoPoint.extraction_def]
measure_igraph [in TwoPoint.extraction_def]
measure_node [in TwoPoint.extraction_def]
measure_subgraph [in TwoPoint.extraction_def]
measure_io [in TwoPoint.extraction_def]
measure_card [in TwoPoint.extraction_def]
memKset [in TwoPoint.preliminaries]
mem_cover [in TwoPoint.preliminaries]
mem_preim [in TwoPoint.preliminaries]
mem_catD [in TwoPoint.preliminaries]
mem_tail [in TwoPoint.preliminaries]
mem_cpl [in TwoPoint.checkpoint]
mem_edgep [in TwoPoint.sgraph]
mem_idp [in TwoPoint.sgraph]
mem_prev [in TwoPoint.sgraph]
mem_pcat [in TwoPoint.sgraph]
mem_pcatT [in TwoPoint.sgraph]
mem_path [in TwoPoint.sgraph]
merge_congr [in TwoPoint.multigraph]
minor_exclusion_2p [in TwoPoint.extraction_iso]
minor_with [in TwoPoint.minor]
minor_induced_add_node [in TwoPoint.minor]
minor_K4_free [in TwoPoint.minor]
minor_trans [in TwoPoint.minor]
minor_map_comp [in TwoPoint.minor]
minor_of_map [in TwoPoint.minor]
N
nat_size_ind [in TwoPoint.preliminaries]ncpP [in TwoPoint.checkpoint]
ncp_interval [in TwoPoint.checkpoint]
ncp_bag [in TwoPoint.checkpoint]
ncp_CP [in TwoPoint.checkpoint]
ncp0 [in TwoPoint.checkpoint]
nodesE [in TwoPoint.sgraph]
nodes_start [in TwoPoint.sgraph]
nodes_end [in TwoPoint.sgraph]
nodes_eqE [in TwoPoint.sgraph]
notin_tail [in TwoPoint.preliminaries]
O
ord_0Vp [in TwoPoint.extraction_iso]P
partition_components [in TwoPoint.sgraph]par2_assoc [in TwoPoint.tm_iso]
par2_idL [in TwoPoint.tm_iso]
par2_idR [in TwoPoint.tm_iso]
par2_injR [in TwoPoint.tm_iso]
par2_injL [in TwoPoint.tm_iso]
par2_LR [in TwoPoint.tm_iso]
par2_congr [in TwoPoint.tm_iso]
par2_eqvP [in TwoPoint.subalgebra]
par2_eqv_oo [in TwoPoint.subalgebra]
par2_eqv_ii [in TwoPoint.subalgebra]
par2_equiv_of [in TwoPoint.subalgebra]
par2_eqv_io [in TwoPoint.subalgebra]
par2_eqv_sym [in TwoPoint.subalgebra]
PathRP [in TwoPoint.sgraph]
path_restrict [in TwoPoint.preliminaries]
Path_from_induced [in TwoPoint.sgraph]
Path_to_induced [in TwoPoint.sgraph]
path_to_induced [in TwoPoint.sgraph]
Path_split [in TwoPoint.sgraph]
path_closed [in TwoPoint.sgraph]
Path_ind [in TwoPoint.sgraph]
Path_connect [in TwoPoint.sgraph]
path_last [in TwoPoint.sgraph]
path_srev [in TwoPoint.sgraph]
pblock_eqvE [in TwoPoint.preliminaries]
pimsetP [in TwoPoint.preliminaries]
pimset_card [in TwoPoint.preliminaries]
pi_hom [in TwoPoint.skeleton]
point_io [in TwoPoint.multigraph]
preim_omap_None [in TwoPoint.preliminaries]
preim_omap_Some [in TwoPoint.preliminaries]
prevK [in TwoPoint.sgraph]
prev_irred [in TwoPoint.sgraph]
prev_inj [in TwoPoint.sgraph]
project_path [in TwoPoint.preliminaries]
R
rcons_spath [in TwoPoint.sgraph]rec_bag [in TwoPoint.extraction_def]
redirect_output_proof [in TwoPoint.extraction_def]
redirect_consistent [in TwoPoint.extraction_def]
redirect_proof1 [in TwoPoint.extraction_def]
relU_sym' [in TwoPoint.preliminaries]
rel0_sym [in TwoPoint.preliminaries]
rel0_irrefl [in TwoPoint.preliminaries]
remove_edges_restrict [in TwoPoint.skeleton]
remove_edges_cross [in TwoPoint.skeleton]
remove_edges_connected [in TwoPoint.skeleton]
remove_loops [in TwoPoint.skeleton]
remove_component [in TwoPoint.sgraph]
rename_width [in TwoPoint.subalgebra]
rename_decomp [in TwoPoint.subalgebra]
rename_sdecomp [in TwoPoint.minor]
restrictE [in TwoPoint.preliminaries]
restrict_path [in TwoPoint.preliminaries]
restrict_mono [in TwoPoint.preliminaries]
restrict_upath [in TwoPoint.sgraph]
rev_inj [in TwoPoint.preliminaries]
rev_upath [in TwoPoint.sgraph]
S
sconnect_sym [in TwoPoint.sgraph]sc_eq [in TwoPoint.preliminaries]
sc_sym [in TwoPoint.preliminaries]
sdecomp_sskel [in TwoPoint.subalgebra]
sdecomp_eq [in TwoPoint.minor]
sedge_equiv_in [in TwoPoint.sgraph]
sedge_in_equiv [in TwoPoint.sgraph]
sedge_equiv [in TwoPoint.sgraph]
seq2_assoc [in TwoPoint.tm_iso]
seq2_idL [in TwoPoint.tm_iso]
seq2_idR [in TwoPoint.tm_iso]
seq2_LR [in TwoPoint.tm_iso]
seq2_injR [in TwoPoint.tm_iso]
seq2_injL [in TwoPoint.tm_iso]
seq2_congr [in TwoPoint.tm_iso]
seq2_eqvP [in TwoPoint.subalgebra]
seq2_equiv_of [in TwoPoint.subalgebra]
seq2_eqv_io [in TwoPoint.subalgebra]
seq2_eqv_sym [in TwoPoint.subalgebra]
setN01E [in TwoPoint.preliminaries]
setU1_mem [in TwoPoint.preliminaries]
set1_inj [in TwoPoint.preliminaries]
set2C [in TwoPoint.preliminaries]
sg_iso_decomp [in TwoPoint.minor]
sg_iso_trans [in TwoPoint.sgraph]
sg_iso_sym [in TwoPoint.sgraph]
sg_iso_refl [in TwoPoint.sgraph]
sg_edgeNeq [in TwoPoint.sgraph]
sintervalP2 [in TwoPoint.checkpoint]
sinterval_cp_cover [in TwoPoint.checkpoint]
sinterval_bag_cover [in TwoPoint.checkpoint]
sinterval_components [in TwoPoint.checkpoint]
sinterval_connectedL [in TwoPoint.checkpoint]
sinterval_connectL [in TwoPoint.checkpoint]
sinterval_noedge_cp [in TwoPoint.checkpoint]
sinterval_disj_cp [in TwoPoint.checkpoint]
sinterval_outside [in TwoPoint.checkpoint]
sinterval_exit [in TwoPoint.checkpoint]
sinterval_sub [in TwoPoint.checkpoint]
sinterval_bounds [in TwoPoint.checkpoint]
sinterval_sym [in TwoPoint.checkpoint]
skelP [in TwoPoint.skeleton]
skel_K4_free [in TwoPoint.subalgebra]
skel_union_join [in TwoPoint.subalgebra]
skel_sub [in TwoPoint.skeleton]
sk_rel_mergeE [in TwoPoint.skeleton]
sk_rel_irrefl [in TwoPoint.skeleton]
sk_rel_sym [in TwoPoint.skeleton]
Some_eqE [in TwoPoint.preliminaries]
source_proof [in TwoPoint.multigraph]
spathP [in TwoPoint.sgraph]
spathW [in TwoPoint.sgraph]
spathxx [in TwoPoint.sgraph]
spath_shorten [in TwoPoint.sgraph]
spath_rev [in TwoPoint.sgraph]
spath_endD [in TwoPoint.sgraph]
spath_end [in TwoPoint.sgraph]
spath_concat [in TwoPoint.sgraph]
spath_cons [in TwoPoint.sgraph]
spath_cat [in TwoPoint.sgraph]
spath_rcons [in TwoPoint.sgraph]
spath_nil [in TwoPoint.sgraph]
spath_last [in TwoPoint.sgraph]
splitL [in TwoPoint.sgraph]
splitR [in TwoPoint.sgraph]
split_pip [in TwoPoint.extraction_iso]
split_io_edges [in TwoPoint.extraction_iso]
split_cp [in TwoPoint.extraction_iso]
split_component [in TwoPoint.extraction_iso]
split_at_first [in TwoPoint.sgraph]
split_at_first_aux [in TwoPoint.sgraph]
split_K4_nontrivial [in TwoPoint.extraction_def]
srestrict_sym [in TwoPoint.sgraph]
srevK [in TwoPoint.sgraph]
srev_nodes [in TwoPoint.sgraph]
srev_rcons [in TwoPoint.sgraph]
sskeleton_remove_io [in TwoPoint.skeleton]
sskeleton_adjacent [in TwoPoint.skeleton]
sskeleton_subgraph_for [in TwoPoint.skeleton]
sskeleton_add [in TwoPoint.extraction_def]
sskelP [in TwoPoint.skeleton]
sskel_K4_free [in TwoPoint.subalgebra]
ssplitP [in TwoPoint.sgraph]
ssplit_K4_nontrivial [in TwoPoint.cp_minor]
ssplit_disconnected [in TwoPoint.sgraph]
strict_is_minor [in TwoPoint.minor]
subcp [in TwoPoint.checkpoint]
subgraph_for_iso [in TwoPoint.multigraph]
subgraph_sub [in TwoPoint.multigraph]
subgraph_K4_free [in TwoPoint.minor]
subrel_restrict [in TwoPoint.preliminaries]
subset_seqL [in TwoPoint.preliminaries]
subset_seqR [in TwoPoint.preliminaries]
subset_cons [in TwoPoint.preliminaries]
subset_pcatR [in TwoPoint.sgraph]
subset_pcatL [in TwoPoint.sgraph]
sub_equiv_of [in TwoPoint.preliminaries]
sub_restrict_connect [in TwoPoint.preliminaries]
sub_trans [in TwoPoint.preliminaries]
sub_connect [in TwoPoint.preliminaries]
sub_in11W [in TwoPoint.preliminaries]
sub_val_eq [in TwoPoint.preliminaries]
sub_inr [in TwoPoint.subalgebra]
sub_inl [in TwoPoint.subalgebra]
sub_sub [in TwoPoint.skeleton]
sub_pointxx [in TwoPoint.skeleton]
sub_minor [in TwoPoint.minor]
sub_forest [in TwoPoint.sgraph]
symmetric_restrict [in TwoPoint.preliminaries]
symmetric_restrict_sedge [in TwoPoint.sgraph]
sym_eqv [in TwoPoint.extraction_iso]
T
tailW [in TwoPoint.sgraph]take_find [in TwoPoint.preliminaries]
target_proof [in TwoPoint.multigraph]
term_of_iso [in TwoPoint.extraction_iso]
term_of_eq [in TwoPoint.extraction_def]
term_of_rec_eq [in TwoPoint.extraction_def]
the_uPathP [in TwoPoint.checkpoint]
the_uPath_proof [in TwoPoint.checkpoint]
three_way_split [in TwoPoint.sgraph]
tnth_cons [in TwoPoint.preliminaries]
tnth_map_in [in TwoPoint.preliminaries]
treeI [in TwoPoint.sgraph]
trivIset3 [in TwoPoint.preliminaries]
TW2_K4_free [in TwoPoint.minor]
U
uncycle [in TwoPoint.sgraph]union_congr [in TwoPoint.multigraph]
unique_forestT [in TwoPoint.sgraph]
uPathP [in TwoPoint.sgraph]
upathP [in TwoPoint.sgraph]
upathPR [in TwoPoint.sgraph]
uPathRP [in TwoPoint.sgraph]
upathW [in TwoPoint.sgraph]
upathWW [in TwoPoint.sgraph]
UPath_from_irred [in TwoPoint.sgraph]
upath_irred [in TwoPoint.sgraph]
UPath_tupleK [in TwoPoint.sgraph]
upath_nil [in TwoPoint.sgraph]
upath_consE [in TwoPoint.sgraph]
upath_cons [in TwoPoint.sgraph]
upath_sym [in TwoPoint.sgraph]
upath_size [in TwoPoint.sgraph]
upath_uniq [in TwoPoint.sgraph]
usplitP [in TwoPoint.sgraph]
V
void_enumP [in TwoPoint.preliminaries]void_pcancel [in TwoPoint.preliminaries]
void_eqP [in TwoPoint.preliminaries]
W
wf_leq [in TwoPoint.preliminaries]width_link [in TwoPoint.subalgebra]
width_minor [in TwoPoint.minor]
width_bound [in TwoPoint.sgraph]
_
_symbols [in TwoPoint.multigraph]Constructor Index
D
Dis3In1 [in TwoPoint.preliminaries]Dis3In2 [in TwoPoint.preliminaries]
Dis3In3 [in TwoPoint.preliminaries]
Dis3Notin [in TwoPoint.preliminaries]
F
Forest [in TwoPoint.sgraph]G
Graph [in TwoPoint.multigraph]Graph2 [in TwoPoint.multigraph]
I
ISplit [in TwoPoint.sgraph]S
SDecomp [in TwoPoint.minor]SgIso [in TwoPoint.sgraph]
SGraph [in TwoPoint.sgraph]
SSplit [in TwoPoint.sgraph]
T
tmA [in TwoPoint.subalgebra]tmC [in TwoPoint.subalgebra]
tmD [in TwoPoint.subalgebra]
tmI [in TwoPoint.subalgebra]
tmS [in TwoPoint.subalgebra]
tmT [in TwoPoint.subalgebra]
tm1 [in TwoPoint.subalgebra]
U
USplit [in TwoPoint.sgraph]Inductive Index
D
disjoint3_cases [in TwoPoint.preliminaries]I
isplit [in TwoPoint.sgraph]S
sg_iso [in TwoPoint.sgraph]spath_split [in TwoPoint.sgraph]
T
term [in TwoPoint.subalgebra]U
usplit [in TwoPoint.sgraph]V
void [in TwoPoint.preliminaries]Projection Index
E
edge [in TwoPoint.multigraph]F
forest_is_forest [in TwoPoint.sgraph]G
graph_of [in TwoPoint.multigraph]g_out [in TwoPoint.multigraph]
g_in [in TwoPoint.multigraph]
I
ival [in TwoPoint.sgraph]L
label [in TwoPoint.multigraph]P
pval [in TwoPoint.sgraph]S
sbag_conn [in TwoPoint.minor]sbag_edge [in TwoPoint.minor]
sbag_cover [in TwoPoint.minor]
sedge [in TwoPoint.sgraph]
sgraph_of_forest [in TwoPoint.sgraph]
sg_irrefl [in TwoPoint.sgraph]
sg_sym [in TwoPoint.sgraph]
source [in TwoPoint.multigraph]
svertex [in TwoPoint.sgraph]
T
target [in TwoPoint.multigraph]U
uval [in TwoPoint.sgraph]V
vertex [in TwoPoint.multigraph]Instance Index
D
dom2_morphism [in TwoPoint.tm_iso]I
iso2_Equivalence [in TwoPoint.multigraph]P
par2_morphisem [in TwoPoint.tm_iso]S
seq2_morphism [in TwoPoint.tm_iso]Section Index
A
AddNode [in TwoPoint.minor]B
Bounded [in TwoPoint.bounded]C
CheckpointOrder [in TwoPoint.checkpoint]CheckPoints [in TwoPoint.checkpoint]
CheckpointsAndMinors [in TwoPoint.cp_minor]
D
DecompTheory [in TwoPoint.minor]Disjoint3 [in TwoPoint.preliminaries]
E
Equivalence [in TwoPoint.preliminaries]F
FinEncodingModuloRel [in TwoPoint.finite_quotient]Foldr1 [in TwoPoint.preliminaries]
Forests [in TwoPoint.sgraph]
I
InducedSubgraph [in TwoPoint.sgraph]J
JoinSG [in TwoPoint.sgraph]JoinT [in TwoPoint.subalgebra]
L
Link [in TwoPoint.subalgebra]M
Max [in TwoPoint.bounded]P
Pack [in TwoPoint.sgraph]Pack.IPath [in TwoPoint.sgraph]
Pack.PathDef [in TwoPoint.sgraph]
Pack.PathTheory [in TwoPoint.sgraph]
Pack.Primitives [in TwoPoint.sgraph]
PathIndexing [in TwoPoint.sgraph]
PathIndexing.IDX [in TwoPoint.sgraph]
Q
Quotients [in TwoPoint.subalgebra]S
SimplePaths [in TwoPoint.sgraph]SplitCP [in TwoPoint.extraction_def]
Subgraphs [in TwoPoint.multigraph]
U
Upath [in TwoPoint.sgraph]Abbreviation Index
E
eC [in TwoPoint.finite_quotient]ereprK [in TwoPoint.finite_quotient]
I
IO [in TwoPoint.tm_iso]IO [in TwoPoint.extraction_def]
L
link_rel [in TwoPoint.extraction_def]M
measure [in TwoPoint.extraction_def]merge [in TwoPoint.multigraph]
R
rel0 [in TwoPoint.preliminaries]S
sigraph [in TwoPoint.extraction_def]V
vfun [in TwoPoint.subalgebra]Definition Index
A
add_node [in TwoPoint.minor]add_node_rel [in TwoPoint.minor]
add_edge [in TwoPoint.sgraph]
add_edge_rel [in TwoPoint.sgraph]
adjacent [in TwoPoint.skeleton]
admissible [in TwoPoint.subalgebra]
B
bag [in TwoPoint.checkpoint]bgraph [in TwoPoint.skeleton]
big_par2_congr' [in TwoPoint.tm_iso]
big_seq2 [in TwoPoint.tm_iso]
big_par2 [in TwoPoint.tm_iso]
big_tmI [in TwoPoint.tm_iso]
bijective2 [in TwoPoint.multigraph]
C
CK4F [in TwoPoint.extraction_def]clique [in TwoPoint.sgraph]
cnv2 [in TwoPoint.subalgebra]
compatible [in TwoPoint.subalgebra]
complete [in TwoPoint.minor]
complete_rel [in TwoPoint.minor]
component [in TwoPoint.extraction_def]
components [in TwoPoint.sgraph]
connected [in TwoPoint.sgraph]
connectedb [in TwoPoint.sgraph]
consistent [in TwoPoint.multigraph]
const0 [in TwoPoint.bounded]
const0_rec [in TwoPoint.bounded]
CP [in TwoPoint.checkpoint]
cp [in TwoPoint.checkpoint]
cpo [in TwoPoint.checkpoint]
cr [in TwoPoint.preliminaries]
C3 [in TwoPoint.minor]
D
decompL [in TwoPoint.subalgebra]decompU [in TwoPoint.subalgebra]
disconnected [in TwoPoint.sgraph]
disjoint_transL [in TwoPoint.preliminaries]
dom2 [in TwoPoint.subalgebra]
E
edgep [in TwoPoint.sgraph]edges [in TwoPoint.multigraph]
edges2 [in TwoPoint.extraction_iso]
edges2_graph [in TwoPoint.extraction_iso]
edge_set [in TwoPoint.multigraph]
edge_graph [in TwoPoint.subalgebra]
edge_surjective [in TwoPoint.minor]
equiv_of_trans [in TwoPoint.preliminaries]
equiv_of_refl [in TwoPoint.preliminaries]
equiv_of [in TwoPoint.preliminaries]
F
Fix [in TwoPoint.bounded]flesh_out_graph [in TwoPoint.skeleton]
foldr1 [in TwoPoint.preliminaries]
foo [in TwoPoint.bounded]
foo_rec [in TwoPoint.bounded]
funU [in TwoPoint.multigraph]
F_rec [in TwoPoint.bounded]
G
graph_of_term [in TwoPoint.subalgebra]H
hom_of [in TwoPoint.multigraph]hom_g2 [in TwoPoint.multigraph]
hom_g [in TwoPoint.multigraph]
hom_s [in TwoPoint.sgraph]
h_ty [in TwoPoint.multigraph]
I
idp [in TwoPoint.sgraph]idx [in TwoPoint.sgraph]
iend [in TwoPoint.cp_minor]
igraph [in TwoPoint.cp_minor]
igraph [in TwoPoint.skeleton]
induced [in TwoPoint.multigraph]
induced [in TwoPoint.sgraph]
induced_proof [in TwoPoint.multigraph]
induced_rel [in TwoPoint.sgraph]
induced_type [in TwoPoint.sgraph]
induced2 [in TwoPoint.multigraph]
injective2 [in TwoPoint.multigraph]
interval [in TwoPoint.checkpoint]
interval_edges [in TwoPoint.skeleton]
in_nodes [in TwoPoint.sgraph]
IPath_finMixin [in TwoPoint.sgraph]
IPath_countMixin [in TwoPoint.sgraph]
IPath_choiceMixin [in TwoPoint.sgraph]
IPath_eqMixin [in TwoPoint.sgraph]
irred [in TwoPoint.sgraph]
irred_of [in TwoPoint.sgraph]
iso [in TwoPoint.multigraph]
iso2 [in TwoPoint.multigraph]
iso2_congruence [in TwoPoint.tm_iso]
istart [in TwoPoint.cp_minor]
is_forestb [in TwoPoint.sgraph]
is_tree [in TwoPoint.sgraph]
is_forest [in TwoPoint.sgraph]
J
join_rel [in TwoPoint.sgraph]K
K4 [in TwoPoint.minor]K4_free [in TwoPoint.minor]
L
lens [in TwoPoint.extraction_def]link [in TwoPoint.subalgebra]
link_graph [in TwoPoint.checkpoint]
link_rel [in TwoPoint.checkpoint]
M
merge_def [in TwoPoint.multigraph]minor [in TwoPoint.minor]
minor_map [in TwoPoint.minor]
N
ncp [in TwoPoint.checkpoint]neighbours [in TwoPoint.cp_minor]
nodes [in TwoPoint.sgraph]
O
one2 [in TwoPoint.subalgebra]ord1 [in TwoPoint.preliminaries]
ord2 [in TwoPoint.preliminaries]
ord3 [in TwoPoint.preliminaries]
P
par2 [in TwoPoint.subalgebra]par2_eq [in TwoPoint.subalgebra]
par2_eqv_trans [in TwoPoint.subalgebra]
par2_eqv_refl [in TwoPoint.subalgebra]
par2_eqv [in TwoPoint.subalgebra]
Path_countMixin [in TwoPoint.sgraph]
Path_choiceMixin [in TwoPoint.sgraph]
Path_eqMixin [in TwoPoint.sgraph]
pcat [in TwoPoint.sgraph]
pcat_proof [in TwoPoint.sgraph]
pe_partition [in TwoPoint.preliminaries]
pimset [in TwoPoint.preliminaries]
point [in TwoPoint.multigraph]
prev [in TwoPoint.sgraph]
prev_proof [in TwoPoint.sgraph]
R
redirect [in TwoPoint.extraction_def]redirect_to [in TwoPoint.extraction_def]
remove_edges [in TwoPoint.skeleton]
rename [in TwoPoint.sgraph]
restrict [in TwoPoint.preliminaries]
S
sc [in TwoPoint.preliminaries]seq2 [in TwoPoint.subalgebra]
seq2_eq [in TwoPoint.subalgebra]
seq2_eqv_trans [in TwoPoint.subalgebra]
seq2_eqv_refl [in TwoPoint.subalgebra]
seq2_eqv [in TwoPoint.subalgebra]
sgP [in TwoPoint.sgraph]
simple_check_point_wf [in TwoPoint.extraction_def]
simple_check_point_term [in TwoPoint.extraction_def]
sinterval [in TwoPoint.checkpoint]
sjoin [in TwoPoint.sgraph]
skeleton [in TwoPoint.skeleton]
sk_rel [in TwoPoint.skeleton]
spath [in TwoPoint.sgraph]
srestrict [in TwoPoint.sgraph]
srev [in TwoPoint.sgraph]
sskeleton [in TwoPoint.skeleton]
strict_minor [in TwoPoint.minor]
strip [in TwoPoint.extraction_iso]
subgraph [in TwoPoint.multigraph]
subgraph [in TwoPoint.sgraph]
subgraph_for [in TwoPoint.multigraph]
sub_edge [in TwoPoint.multigraph]
sub_vertex [in TwoPoint.multigraph]
sum_eqE [in TwoPoint.preliminaries]
sunit [in TwoPoint.sgraph]
surjective [in TwoPoint.preliminaries]
surjective2 [in TwoPoint.multigraph]
sym [in TwoPoint.multigraph]
sym0 [in TwoPoint.multigraph]
sym2 [in TwoPoint.subalgebra]
sym2b [in TwoPoint.extraction_iso]
sym2b' [in TwoPoint.extraction_iso]
sym2_ [in TwoPoint.extraction_iso]
T
tail [in TwoPoint.sgraph]term_of [in TwoPoint.extraction_def]
term_of_rec [in TwoPoint.extraction_def]
term_of_measure [in TwoPoint.extraction_def]
the_uPath [in TwoPoint.checkpoint]
tjoin [in TwoPoint.subalgebra]
tlink [in TwoPoint.subalgebra]
tmEs [in TwoPoint.extraction_def]
tm_ [in TwoPoint.extraction_def]
top2 [in TwoPoint.subalgebra]
total_minor_map [in TwoPoint.minor]
triv_decomp [in TwoPoint.subalgebra]
triv_sdecomp [in TwoPoint.minor]
tunit [in TwoPoint.sgraph]
tuple_UPath [in TwoPoint.sgraph]
two_graph [in TwoPoint.subalgebra]
U
union [in TwoPoint.multigraph]unique [in TwoPoint.preliminaries]
unit_graph [in TwoPoint.subalgebra]
unit_forest [in TwoPoint.sgraph]
upath [in TwoPoint.sgraph]
UPathW [in TwoPoint.sgraph]
upath_of [in TwoPoint.sgraph]
UPath_finMixin [in TwoPoint.sgraph]
UPath_tuple [in TwoPoint.sgraph]
UPath_countMixin [in TwoPoint.sgraph]
UPath_choiceMixin [in TwoPoint.sgraph]
UPath_eqMixin [in TwoPoint.sgraph]
V
void_countMixin [in TwoPoint.preliminaries]void_choiceMixin [in TwoPoint.preliminaries]
W
width [in TwoPoint.sgraph]Record Index
F
forest [in TwoPoint.sgraph]G
graph [in TwoPoint.multigraph]graph2 [in TwoPoint.multigraph]
I
IPath [in TwoPoint.sgraph]P
Path [in TwoPoint.sgraph]S
sdecomp [in TwoPoint.minor]sgraph [in TwoPoint.sgraph]
U
UPath [in TwoPoint.sgraph]| 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 | (989 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 | (12 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 | (92 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 | (14 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 | (585 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 | (20 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 | (7 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 | (20 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 | (4 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 | (28 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 | (10 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 | (189 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 | (8 entries) |