| 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 | (439 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 | (20 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 | (13 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 | (153 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 | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 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 | (36 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 | (147 entries) |
Global Index
A
Acyclic [inductive, in GraphBasics.Acyclic]ACYCLIC [section, in GraphBasics.Acyclic]
Acyclic [library]
Acyclic_no_cycle [lemma, in GraphBasics.Acyclic]
ACYCLIC_AND_DEGREES [section, in GraphBasics.Acyclic]
Acyclic_Isa_Graph [lemma, in GraphBasics.Acyclic]
Acyclic_connected_isa_tree [lemma, in GraphBasics.Trees]
AC_edge_degree_one [lemma, in GraphBasics.Acyclic]
AC_edge_pendant [lemma, in GraphBasics.Acyclic]
AC_vertex_degree_zero [lemma, in GraphBasics.Acyclic]
AC_vertex_isolated [lemma, in GraphBasics.Acyclic]
AC_ina_inv2 [lemma, in GraphBasics.Acyclic]
AC_ina_inv1 [lemma, in GraphBasics.Acyclic]
AC_eq [constructor, in GraphBasics.Acyclic]
AC_leaf [constructor, in GraphBasics.Acyclic]
AC_vertex [constructor, in GraphBasics.Acyclic]
AC_empty [constructor, in GraphBasics.Acyclic]
APPEND_WALKS.a [variable, in GraphBasics.Paths]
APPEND_WALKS.v [variable, in GraphBasics.Paths]
APPEND_WALKS [section, in GraphBasics.Paths]
Arc [inductive, in GraphBasics.Arcs]
ARC [section, in GraphBasics.Arcs]
Arcs [library]
A_union_single_inter [lemma, in GraphBasics.Graphs]
A_union_edge_edge [lemma, in GraphBasics.Edges]
A_in_union_edge [lemma, in GraphBasics.Edges]
A_not_in_union [lemma, in GraphBasics.Arcs]
A_out_neighborhood [definition, in GraphBasics.Arcs]
A_in_neighborhood [definition, in GraphBasics.Arcs]
A_single_single_disjoint [definition, in GraphBasics.Arcs]
A_single_disjoint [definition, in GraphBasics.Arcs]
A_union_inversion2 [definition, in GraphBasics.Arcs]
A_union_inversion [definition, in GraphBasics.Arcs]
A_distributivity_union_inter [definition, in GraphBasics.Arcs]
A_distributivity_inter_union [definition, in GraphBasics.Arcs]
A_union_differ_inter [definition, in GraphBasics.Arcs]
A_differ_empty [definition, in GraphBasics.Arcs]
A_differ_E_E [definition, in GraphBasics.Arcs]
A_differ [definition, in GraphBasics.Arcs]
A_inter_absorb [definition, in GraphBasics.Arcs]
A_included_inter [definition, in GraphBasics.Arcs]
A_not_inter [definition, in GraphBasics.Arcs]
A_inter_assoc [definition, in GraphBasics.Arcs]
A_inter_commut [definition, in GraphBasics.Arcs]
A_inter_neutral [definition, in GraphBasics.Arcs]
A_inter_empty [definition, in GraphBasics.Arcs]
A_inter_eq [definition, in GraphBasics.Arcs]
A_in_inter [definition, in GraphBasics.Arcs]
A_inter [definition, in GraphBasics.Arcs]
A_union_absorb [definition, in GraphBasics.Arcs]
A_included_union [definition, in GraphBasics.Arcs]
A_union_dec [definition, in GraphBasics.Arcs]
A_not_union [definition, in GraphBasics.Arcs]
A_union_assoc [definition, in GraphBasics.Arcs]
A_union_commut [definition, in GraphBasics.Arcs]
A_union_neutral [definition, in GraphBasics.Arcs]
A_union_eq [definition, in GraphBasics.Arcs]
A_in_right [definition, in GraphBasics.Arcs]
A_in_left [definition, in GraphBasics.Arcs]
A_union [definition, in GraphBasics.Arcs]
A_enumerable_sum [definition, in GraphBasics.Arcs]
A_enumerable [definition, in GraphBasics.Arcs]
A_included_single [definition, in GraphBasics.Arcs]
A_included [definition, in GraphBasics.Arcs]
A_single_equal_single [definition, in GraphBasics.Arcs]
A_single_equal [definition, in GraphBasics.Arcs]
A_in_single [definition, in GraphBasics.Arcs]
A_single [definition, in GraphBasics.Arcs]
A_empty_nothing [definition, in GraphBasics.Arcs]
A_empty [definition, in GraphBasics.Arcs]
A_set_diff_commut [definition, in GraphBasics.Arcs]
A_set_eq_commut [definition, in GraphBasics.Arcs]
A_eq_set [definition, in GraphBasics.Arcs]
A_set_diff [definition, in GraphBasics.Arcs]
A_set_eq [definition, in GraphBasics.Arcs]
A_set [definition, in GraphBasics.Arcs]
A_sum [definition, in GraphBasics.Arcs]
A_canon [definition, in GraphBasics.Arcs]
A_in_dec [definition, in GraphBasics.Arcs]
A_nil [definition, in GraphBasics.Arcs]
A_list [definition, in GraphBasics.Arcs]
A_loop [definition, in GraphBasics.Arcs]
A_head [definition, in GraphBasics.Arcs]
A_tail [definition, in GraphBasics.Arcs]
A_eq_dec [lemma, in GraphBasics.Arcs]
A_ends [constructor, in GraphBasics.Arcs]
A_included_union' [lemma, in GraphBasics.Connected]
C
cdr [definition, in GraphBasics.Paths]cdr_app [lemma, in GraphBasics.Paths]
Closed_trail [definition, in GraphBasics.Paths]
Closed_walk [definition, in GraphBasics.Paths]
Connected [inductive, in GraphBasics.Connected]
CONNECTED [section, in GraphBasics.Connected]
Connected [library]
CONNECTED_AND_ACYCLIC [section, in GraphBasics.Trees]
Connected_path [lemma, in GraphBasics.Connected]
Connected_walk [lemma, in GraphBasics.Connected]
CONNECTED_BY_EDGES [section, in GraphBasics.Connected]
Connected_Isa_Graph [lemma, in GraphBasics.Connected]
Connected_not_empty [lemma, in GraphBasics.Connected]
Cycle [definition, in GraphBasics.Paths]
Cycle_degree_one_nil [lemma, in GraphBasics.Paths]
Cycle_consx_degree_two [lemma, in GraphBasics.Paths]
Cycle_degree_two [lemma, in GraphBasics.Paths]
C_minus_pendant [lemma, in GraphBasics.Connected]
C_pendant_isolated [lemma, in GraphBasics.Connected]
C_minus_isolated_right [lemma, in GraphBasics.Connected]
C_minus_isolated_left [lemma, in GraphBasics.Connected]
C_minus_isolated [lemma, in GraphBasics.Connected]
C_ina_inv2 [lemma, in GraphBasics.Connected]
C_ina_inv1 [lemma, in GraphBasics.Connected]
C_a_dec [lemma, in GraphBasics.Connected]
C_v_dec [lemma, in GraphBasics.Connected]
C_eq [constructor, in GraphBasics.Connected]
C_edge [constructor, in GraphBasics.Connected]
C_leaf [constructor, in GraphBasics.Connected]
C_isolated [constructor, in GraphBasics.Connected]
D
DA_list [definition, in GraphBasics.Digraphs]degree [definition, in GraphBasics.Degrees]
DEGREE [section, in GraphBasics.Degrees]
Degrees [library]
Degree_not_pendant [lemma, in GraphBasics.Degrees]
Degree_not_isolated [lemma, in GraphBasics.Degrees]
Degree_pendant [lemma, in GraphBasics.Degrees]
Degree_isolated [lemma, in GraphBasics.Degrees]
Degree_neighborhood [lemma, in GraphBasics.Degrees]
Differ [inductive, in GraphBasics.Sets]
Differ_empty [lemma, in GraphBasics.Sets]
Differ_E_E [lemma, in GraphBasics.Sets]
Digraph [inductive, in GraphBasics.Digraphs]
DIGRAPH [section, in GraphBasics.Digraphs]
Digraphs [library]
Dipaths [library]
DIRECTED_PATHES.a [variable, in GraphBasics.Dipaths]
DIRECTED_PATHES.v [variable, in GraphBasics.Dipaths]
DIRECTED_PATHES [section, in GraphBasics.Dipaths]
Distributivity_union_inter [lemma, in GraphBasics.Sets]
Distributivity_inter_union [lemma, in GraphBasics.Sets]
DP_step [constructor, in GraphBasics.Dipaths]
DP_null [constructor, in GraphBasics.Dipaths]
DT_step [constructor, in GraphBasics.Dipaths]
DT_null [constructor, in GraphBasics.Dipaths]
DV_list [definition, in GraphBasics.Digraphs]
DW_step [constructor, in GraphBasics.Dipaths]
DW_null [constructor, in GraphBasics.Dipaths]
D_path_isa_trail [lemma, in GraphBasics.Dipaths]
D_trail_isa_walk [lemma, in GraphBasics.Dipaths]
D_cycle [definition, in GraphBasics.Dipaths]
D_path [inductive, in GraphBasics.Dipaths]
D_closed_trail [definition, in GraphBasics.Dipaths]
D_trail [inductive, in GraphBasics.Dipaths]
D_closed_walk [definition, in GraphBasics.Dipaths]
D_walk [inductive, in GraphBasics.Dipaths]
D_union [lemma, in GraphBasics.Digraphs]
D_a_dec [lemma, in GraphBasics.Digraphs]
D_v_dec [lemma, in GraphBasics.Digraphs]
D_size [definition, in GraphBasics.Digraphs]
D_order [definition, in GraphBasics.Digraphs]
D_eq [constructor, in GraphBasics.Digraphs]
D_arc [constructor, in GraphBasics.Digraphs]
D_vertex [constructor, in GraphBasics.Digraphs]
D_empty [constructor, in GraphBasics.Digraphs]
E
Edge [inductive, in GraphBasics.Edges]EDGE [section, in GraphBasics.Edges]
Edges [library]
Empty [inductive, in GraphBasics.Sets]
Empty_nothing [lemma, in GraphBasics.Sets]
Enumerated [library]
ENUMERATION [section, in GraphBasics.Enumerated]
ENUMERATION.f [variable, in GraphBasics.Enumerated]
ENUMERATION.U [variable, in GraphBasics.Enumerated]
ENUMERATION.U_separable [variable, in GraphBasics.Enumerated]
EXTRACTED [section, in GraphBasics.Paths]
EXTRACTED.a [variable, in GraphBasics.Paths]
EXTRACTED.v [variable, in GraphBasics.Paths]
E_eq_not_in' [lemma, in GraphBasics.Edges]
E_eq_not_in [lemma, in GraphBasics.Edges]
E_set_disjoint [lemma, in GraphBasics.Edges]
E_inter_empty [lemma, in GraphBasics.Edges]
E_union_absorb [lemma, in GraphBasics.Edges]
E_inclusion [lemma, in GraphBasics.Edges]
E_PROPERTIES [section, in GraphBasics.Edges]
E_add_edge [lemma, in GraphBasics.Edges]
E_in [definition, in GraphBasics.Edges]
E_eq_dec [lemma, in GraphBasics.Edges]
E_nil [definition, in GraphBasics.Edges]
E_list [definition, in GraphBasics.Edges]
E_rev [constructor, in GraphBasics.Edges]
E_refl [constructor, in GraphBasics.Edges]
E_eq [inductive, in GraphBasics.Edges]
E_ends [constructor, in GraphBasics.Edges]
E_not_set_eq24 [lemma, in GraphBasics.Edges]
E_not_set_eq14 [lemma, in GraphBasics.Edges]
E_not_set_eq123 [lemma, in GraphBasics.Edges]
E_set_eq_dec [lemma, in GraphBasics.Edges]
E_set_diff_eq [lemma, in GraphBasics.Edges]
E_set_eq_diff [lemma, in GraphBasics.Edges]
E_set_diff4 [lemma, in GraphBasics.Edges]
E_set_diff3 [lemma, in GraphBasics.Edges]
E_set_diff2 [lemma, in GraphBasics.Edges]
E_set_diff1 [lemma, in GraphBasics.Edges]
E_set_eq [lemma, in GraphBasics.Edges]
E_left [constructor, in GraphBasics.Edges]
E_right [constructor, in GraphBasics.Edges]
E_set [inductive, in GraphBasics.Edges]
E_reverse [definition, in GraphBasics.Paths]
E_not_eq_traversal_pendant [lemma, in GraphBasics.Connected]
E_pendant_quasi_isolated [lemma, in GraphBasics.Connected]
F
Full [inductive, in GraphBasics.Sets]G
GA_list [definition, in GraphBasics.Graphs]GE_list [definition, in GraphBasics.Graphs]
Graph [inductive, in GraphBasics.Graphs]
GRAPH [section, in GraphBasics.Graphs]
Graphs [library]
graph_isa_digraph [lemma, in GraphBasics.Graphs]
GRAPH_TO_DIGRAPH [section, in GraphBasics.Graphs]
GV_list [definition, in GraphBasics.Graphs]
G_minus_edge [lemma, in GraphBasics.Graphs]
G_minus_vertex [lemma, in GraphBasics.Graphs]
G_empty_empty [lemma, in GraphBasics.Graphs]
G_union [lemma, in GraphBasics.Graphs]
G_ina_inv2 [lemma, in GraphBasics.Graphs]
G_ina_inv1 [lemma, in GraphBasics.Graphs]
G_non_directed [lemma, in GraphBasics.Graphs]
G_a_dec [lemma, in GraphBasics.Graphs]
G_v_dec [lemma, in GraphBasics.Graphs]
G_size [definition, in GraphBasics.Graphs]
G_order [definition, in GraphBasics.Graphs]
G_eq [constructor, in GraphBasics.Graphs]
G_edge [constructor, in GraphBasics.Graphs]
G_vertex [constructor, in GraphBasics.Graphs]
G_empty [constructor, in GraphBasics.Graphs]
G_ends_in [lemma, in GraphBasics.Paths]
I
Included [definition, in GraphBasics.Sets]Included_inter [lemma, in GraphBasics.Sets]
Included_union [lemma, in GraphBasics.Sets]
Included_single [lemma, in GraphBasics.Sets]
index [constructor, in GraphBasics.Vertices]
Inter [inductive, in GraphBasics.Sets]
Inter_absorb [lemma, in GraphBasics.Sets]
Inter_assoc [lemma, in GraphBasics.Sets]
Inter_commut [lemma, in GraphBasics.Sets]
Inter_empty [lemma, in GraphBasics.Sets]
Inter_neutral [lemma, in GraphBasics.Sets]
Inter_eq [lemma, in GraphBasics.Sets]
INVERSION_GRAPH [section, in GraphBasics.Graphs]
INVERSION_CONNECTED [section, in GraphBasics.Connected]
In_differ [constructor, in GraphBasics.Sets]
In_inter [constructor, in GraphBasics.Sets]
In_right [constructor, in GraphBasics.Sets]
In_left [constructor, in GraphBasics.Sets]
In_single [constructor, in GraphBasics.Sets]
In_full [constructor, in GraphBasics.Sets]
In_degree_neighborhood [lemma, in GraphBasics.Degrees]
In_degree [definition, in GraphBasics.Degrees]
In_neighborhood [definition, in GraphBasics.Degrees]
In_and_out_neighbor [lemma, in GraphBasics.Degrees]
In_neighbor [definition, in GraphBasics.Degrees]
isolated [definition, in GraphBasics.Degrees]
L
LIST_OF_EDGES [section, in GraphBasics.Edges]N
Neighbor [definition, in GraphBasics.Degrees]NEIGHBOR [section, in GraphBasics.Degrees]
neighborhood [definition, in GraphBasics.Degrees]
neighbor_out_neighbor [lemma, in GraphBasics.Degrees]
neighbor_in_neighbor [lemma, in GraphBasics.Degrees]
NEIGHBOR.a [variable, in GraphBasics.Degrees]
NEIGHBOR.v [variable, in GraphBasics.Degrees]
Not_inter [lemma, in GraphBasics.Sets]
Not_union [lemma, in GraphBasics.Sets]
O
one_le_one [lemma, in GraphBasics.Acyclic]Out_degree_neighborhood [lemma, in GraphBasics.Degrees]
Out_degree [definition, in GraphBasics.Degrees]
Out_neighborhood [definition, in GraphBasics.Degrees]
Out_neighbor [definition, in GraphBasics.Degrees]
P
Path [inductive, in GraphBasics.Paths]PATH [section, in GraphBasics.Paths]
Paths [library]
Path_supergraph_cons_arc [lemma, in GraphBasics.Paths]
Path_supergraph_arc [lemma, in GraphBasics.Paths]
Path_supergraph_cons_vertex [lemma, in GraphBasics.Paths]
Path_supergraph_vertex [lemma, in GraphBasics.Paths]
Path_subgraph [lemma, in GraphBasics.Paths]
PATH_IN_A_SUBGRAPH [section, in GraphBasics.Paths]
Path_eq [lemma, in GraphBasics.Paths]
PATH_EQ [section, in GraphBasics.Paths]
Path_degree_zero_nil [lemma, in GraphBasics.Paths]
Path_last_step [lemma, in GraphBasics.Paths]
Path_degree_two [lemma, in GraphBasics.Paths]
Path_consx_degree_one [lemma, in GraphBasics.Paths]
Path_degree_one [lemma, in GraphBasics.Paths]
PATH_AND_DEGREE.g [variable, in GraphBasics.Paths]
PATH_AND_DEGREE.a [variable, in GraphBasics.Paths]
PATH_AND_DEGREE.v [variable, in GraphBasics.Paths]
PATH_AND_DEGREE [section, in GraphBasics.Paths]
Path_isa_trail [lemma, in GraphBasics.Paths]
PATH.a [variable, in GraphBasics.Paths]
PATH.v [variable, in GraphBasics.Paths]
pendant [definition, in GraphBasics.Degrees]
P_when_cycle [lemma, in GraphBasics.Paths]
P_extract [lemma, in GraphBasics.Paths]
P_backstep [lemma, in GraphBasics.Paths]
P_inxyel_inyvl [lemma, in GraphBasics.Paths]
P_inxyel_inxvl [lemma, in GraphBasics.Paths]
P_inel_ina [lemma, in GraphBasics.Paths]
P_invl_inv [lemma, in GraphBasics.Paths]
P_endy_inv [lemma, in GraphBasics.Paths]
P_endx_inv [lemma, in GraphBasics.Paths]
P_iny_vl [lemma, in GraphBasics.Paths]
P_step [constructor, in GraphBasics.Paths]
P_null [constructor, in GraphBasics.Paths]
R
REMARKABLE_DEGREE [section, in GraphBasics.Degrees]REVERSE_WALK.g [variable, in GraphBasics.Paths]
REVERSE_WALK.a [variable, in GraphBasics.Paths]
REVERSE_WALK.v [variable, in GraphBasics.Paths]
REVERSE_WALK [section, in GraphBasics.Paths]
S
Sets [library]Single [inductive, in GraphBasics.Sets]
Single_single_disjoint [lemma, in GraphBasics.Sets]
Single_disjoint [lemma, in GraphBasics.Sets]
Single_equal_single [lemma, in GraphBasics.Sets]
Single_equal [lemma, in GraphBasics.Sets]
T
Trail [inductive, in GraphBasics.Paths]Trail_subgraph [lemma, in GraphBasics.Paths]
Trail_eq [lemma, in GraphBasics.Paths]
Trail_isa_walk [lemma, in GraphBasics.Paths]
Tree [inductive, in GraphBasics.Trees]
TREE [section, in GraphBasics.Trees]
Trees [library]
Tree_isa_acyclic [lemma, in GraphBasics.Trees]
Tree_isa_connected [lemma, in GraphBasics.Trees]
Tree_isa_graph [lemma, in GraphBasics.Trees]
T_eq [constructor, in GraphBasics.Trees]
T_leaf [constructor, in GraphBasics.Trees]
T_root [constructor, in GraphBasics.Trees]
T_step [constructor, in GraphBasics.Paths]
T_null [constructor, in GraphBasics.Paths]
U
Union [inductive, in GraphBasics.Sets]UNION_GRAPHS [section, in GraphBasics.Graphs]
UNION_DIGRAPHS [section, in GraphBasics.Digraphs]
Union_single_single [lemma, in GraphBasics.Sets]
Union_inversion2 [lemma, in GraphBasics.Sets]
Union_inversion [lemma, in GraphBasics.Sets]
Union_differ_inter [lemma, in GraphBasics.Sets]
Union_absorb [lemma, in GraphBasics.Sets]
Union_dec [lemma, in GraphBasics.Sets]
Union_assoc [lemma, in GraphBasics.Sets]
Union_commut [lemma, in GraphBasics.Sets]
Union_neutral [lemma, in GraphBasics.Sets]
Union_eq [lemma, in GraphBasics.Sets]
U_enumerable_sum [lemma, in GraphBasics.Enumerated]
U_sum [definition, in GraphBasics.Enumerated]
U_in_dec [lemma, in GraphBasics.Enumerated]
U_canon_cons [constructor, in GraphBasics.Enumerated]
U_canon_nil [constructor, in GraphBasics.Enumerated]
U_canon [inductive, in GraphBasics.Enumerated]
U_enumerable [definition, in GraphBasics.Enumerated]
U_list [definition, in GraphBasics.Enumerated]
U_SETS.MIXED_PROPERTIES [section, in GraphBasics.Sets]
U_SETS.DIFFERENCE [section, in GraphBasics.Sets]
U_SETS.INTERSECTION [section, in GraphBasics.Sets]
U_SETS.UNION [section, in GraphBasics.Sets]
U_SETS.INCLUSION [section, in GraphBasics.Sets]
U_set_diff [lemma, in GraphBasics.Sets]
U_set_diff_commut [lemma, in GraphBasics.Sets]
U_set_eq_commut [lemma, in GraphBasics.Sets]
U_eq_set [lemma, in GraphBasics.Sets]
U_set_eq [axiom, in GraphBasics.Sets]
U_set [definition, in GraphBasics.Sets]
U_SETS.U [variable, in GraphBasics.Sets]
U_SETS [section, in GraphBasics.Sets]
V
Vertex [inductive, in GraphBasics.Vertices]VERTEX [section, in GraphBasics.Vertices]
Vertices [library]
V_union_single_inter [lemma, in GraphBasics.Graphs]
V_extract [definition, in GraphBasics.Paths]
V_union_single_dec [lemma, in GraphBasics.Vertices]
V_union_single_single [definition, in GraphBasics.Vertices]
V_single_single_disjoint [definition, in GraphBasics.Vertices]
V_single_disjoint [definition, in GraphBasics.Vertices]
V_union_inversion2 [definition, in GraphBasics.Vertices]
V_union_inversion [definition, in GraphBasics.Vertices]
V_distributivity_union_inter [definition, in GraphBasics.Vertices]
V_distributivity_inter_union [definition, in GraphBasics.Vertices]
V_union_differ_inter [definition, in GraphBasics.Vertices]
V_differ_empty [definition, in GraphBasics.Vertices]
V_differ_E_E [definition, in GraphBasics.Vertices]
V_differ [definition, in GraphBasics.Vertices]
V_inter_absorb [definition, in GraphBasics.Vertices]
V_included_inter [definition, in GraphBasics.Vertices]
V_not_inter [definition, in GraphBasics.Vertices]
V_inter_assoc [definition, in GraphBasics.Vertices]
V_inter_commut [definition, in GraphBasics.Vertices]
V_inter_empty [definition, in GraphBasics.Vertices]
V_inter_neutral [definition, in GraphBasics.Vertices]
V_inter_eq [definition, in GraphBasics.Vertices]
V_in_inter [definition, in GraphBasics.Vertices]
V_inter [definition, in GraphBasics.Vertices]
V_union_absorb [definition, in GraphBasics.Vertices]
V_included_union [definition, in GraphBasics.Vertices]
V_union_dec [definition, in GraphBasics.Vertices]
V_not_union [definition, in GraphBasics.Vertices]
V_union_assoc [definition, in GraphBasics.Vertices]
V_union_commut [definition, in GraphBasics.Vertices]
V_union_neutral [definition, in GraphBasics.Vertices]
V_union_eq [definition, in GraphBasics.Vertices]
V_in_right [definition, in GraphBasics.Vertices]
V_in_left [definition, in GraphBasics.Vertices]
V_union [definition, in GraphBasics.Vertices]
V_enumerable_sum [definition, in GraphBasics.Vertices]
V_enumerable [definition, in GraphBasics.Vertices]
V_included_single [definition, in GraphBasics.Vertices]
V_included [definition, in GraphBasics.Vertices]
V_single_equal_single [definition, in GraphBasics.Vertices]
V_single_equal [definition, in GraphBasics.Vertices]
V_in_single [definition, in GraphBasics.Vertices]
V_single [definition, in GraphBasics.Vertices]
V_empty_nothing [definition, in GraphBasics.Vertices]
V_empty [definition, in GraphBasics.Vertices]
V_set_diff_commut [definition, in GraphBasics.Vertices]
V_set_eq_commut [definition, in GraphBasics.Vertices]
V_eq_set [definition, in GraphBasics.Vertices]
V_set_diff [definition, in GraphBasics.Vertices]
V_set_eq [definition, in GraphBasics.Vertices]
V_set [definition, in GraphBasics.Vertices]
V_sum [definition, in GraphBasics.Vertices]
V_canon [definition, in GraphBasics.Vertices]
V_in_dec [definition, in GraphBasics.Vertices]
V_nil [definition, in GraphBasics.Vertices]
V_list [definition, in GraphBasics.Vertices]
V_eq_dec [lemma, in GraphBasics.Vertices]
V_included_union' [lemma, in GraphBasics.Connected]
W
Walk [inductive, in GraphBasics.Paths]Walk_reverse [lemma, in GraphBasics.Paths]
Walk_append [lemma, in GraphBasics.Paths]
Walk_subgraph [lemma, in GraphBasics.Paths]
Walk_eq [lemma, in GraphBasics.Paths]
Walk_to_path [lemma, in GraphBasics.Paths]
W_step [constructor, in GraphBasics.Paths]
W_null [constructor, in GraphBasics.Paths]
Variable Index
A
APPEND_WALKS.a [in GraphBasics.Paths]APPEND_WALKS.v [in GraphBasics.Paths]
D
DIRECTED_PATHES.a [in GraphBasics.Dipaths]DIRECTED_PATHES.v [in GraphBasics.Dipaths]
E
ENUMERATION.f [in GraphBasics.Enumerated]ENUMERATION.U [in GraphBasics.Enumerated]
ENUMERATION.U_separable [in GraphBasics.Enumerated]
EXTRACTED.a [in GraphBasics.Paths]
EXTRACTED.v [in GraphBasics.Paths]
N
NEIGHBOR.a [in GraphBasics.Degrees]NEIGHBOR.v [in GraphBasics.Degrees]
P
PATH_AND_DEGREE.g [in GraphBasics.Paths]PATH_AND_DEGREE.a [in GraphBasics.Paths]
PATH_AND_DEGREE.v [in GraphBasics.Paths]
PATH.a [in GraphBasics.Paths]
PATH.v [in GraphBasics.Paths]
R
REVERSE_WALK.g [in GraphBasics.Paths]REVERSE_WALK.a [in GraphBasics.Paths]
REVERSE_WALK.v [in GraphBasics.Paths]
U
U_SETS.U [in GraphBasics.Sets]Library Index
A
AcyclicArcs
C
ConnectedD
DegreesDigraphs
Dipaths
E
EdgesEnumerated
G
GraphsP
PathsS
SetsT
TreesV
VerticesLemma Index
A
Acyclic_no_cycle [in GraphBasics.Acyclic]Acyclic_Isa_Graph [in GraphBasics.Acyclic]
Acyclic_connected_isa_tree [in GraphBasics.Trees]
AC_edge_degree_one [in GraphBasics.Acyclic]
AC_edge_pendant [in GraphBasics.Acyclic]
AC_vertex_degree_zero [in GraphBasics.Acyclic]
AC_vertex_isolated [in GraphBasics.Acyclic]
AC_ina_inv2 [in GraphBasics.Acyclic]
AC_ina_inv1 [in GraphBasics.Acyclic]
A_union_single_inter [in GraphBasics.Graphs]
A_union_edge_edge [in GraphBasics.Edges]
A_in_union_edge [in GraphBasics.Edges]
A_not_in_union [in GraphBasics.Arcs]
A_eq_dec [in GraphBasics.Arcs]
A_included_union' [in GraphBasics.Connected]
C
cdr_app [in GraphBasics.Paths]Connected_path [in GraphBasics.Connected]
Connected_walk [in GraphBasics.Connected]
Connected_Isa_Graph [in GraphBasics.Connected]
Connected_not_empty [in GraphBasics.Connected]
Cycle_degree_one_nil [in GraphBasics.Paths]
Cycle_consx_degree_two [in GraphBasics.Paths]
Cycle_degree_two [in GraphBasics.Paths]
C_minus_pendant [in GraphBasics.Connected]
C_pendant_isolated [in GraphBasics.Connected]
C_minus_isolated_right [in GraphBasics.Connected]
C_minus_isolated_left [in GraphBasics.Connected]
C_minus_isolated [in GraphBasics.Connected]
C_ina_inv2 [in GraphBasics.Connected]
C_ina_inv1 [in GraphBasics.Connected]
C_a_dec [in GraphBasics.Connected]
C_v_dec [in GraphBasics.Connected]
D
Degree_not_pendant [in GraphBasics.Degrees]Degree_not_isolated [in GraphBasics.Degrees]
Degree_pendant [in GraphBasics.Degrees]
Degree_isolated [in GraphBasics.Degrees]
Degree_neighborhood [in GraphBasics.Degrees]
Differ_empty [in GraphBasics.Sets]
Differ_E_E [in GraphBasics.Sets]
Distributivity_union_inter [in GraphBasics.Sets]
Distributivity_inter_union [in GraphBasics.Sets]
D_path_isa_trail [in GraphBasics.Dipaths]
D_trail_isa_walk [in GraphBasics.Dipaths]
D_union [in GraphBasics.Digraphs]
D_a_dec [in GraphBasics.Digraphs]
D_v_dec [in GraphBasics.Digraphs]
E
Empty_nothing [in GraphBasics.Sets]E_eq_not_in' [in GraphBasics.Edges]
E_eq_not_in [in GraphBasics.Edges]
E_set_disjoint [in GraphBasics.Edges]
E_inter_empty [in GraphBasics.Edges]
E_union_absorb [in GraphBasics.Edges]
E_inclusion [in GraphBasics.Edges]
E_add_edge [in GraphBasics.Edges]
E_eq_dec [in GraphBasics.Edges]
E_not_set_eq24 [in GraphBasics.Edges]
E_not_set_eq14 [in GraphBasics.Edges]
E_not_set_eq123 [in GraphBasics.Edges]
E_set_eq_dec [in GraphBasics.Edges]
E_set_diff_eq [in GraphBasics.Edges]
E_set_eq_diff [in GraphBasics.Edges]
E_set_diff4 [in GraphBasics.Edges]
E_set_diff3 [in GraphBasics.Edges]
E_set_diff2 [in GraphBasics.Edges]
E_set_diff1 [in GraphBasics.Edges]
E_set_eq [in GraphBasics.Edges]
E_not_eq_traversal_pendant [in GraphBasics.Connected]
E_pendant_quasi_isolated [in GraphBasics.Connected]
G
graph_isa_digraph [in GraphBasics.Graphs]G_minus_edge [in GraphBasics.Graphs]
G_minus_vertex [in GraphBasics.Graphs]
G_empty_empty [in GraphBasics.Graphs]
G_union [in GraphBasics.Graphs]
G_ina_inv2 [in GraphBasics.Graphs]
G_ina_inv1 [in GraphBasics.Graphs]
G_non_directed [in GraphBasics.Graphs]
G_a_dec [in GraphBasics.Graphs]
G_v_dec [in GraphBasics.Graphs]
G_ends_in [in GraphBasics.Paths]
I
Included_inter [in GraphBasics.Sets]Included_union [in GraphBasics.Sets]
Included_single [in GraphBasics.Sets]
Inter_absorb [in GraphBasics.Sets]
Inter_assoc [in GraphBasics.Sets]
Inter_commut [in GraphBasics.Sets]
Inter_empty [in GraphBasics.Sets]
Inter_neutral [in GraphBasics.Sets]
Inter_eq [in GraphBasics.Sets]
In_degree_neighborhood [in GraphBasics.Degrees]
In_and_out_neighbor [in GraphBasics.Degrees]
N
neighbor_out_neighbor [in GraphBasics.Degrees]neighbor_in_neighbor [in GraphBasics.Degrees]
Not_inter [in GraphBasics.Sets]
Not_union [in GraphBasics.Sets]
O
one_le_one [in GraphBasics.Acyclic]Out_degree_neighborhood [in GraphBasics.Degrees]
P
Path_supergraph_cons_arc [in GraphBasics.Paths]Path_supergraph_arc [in GraphBasics.Paths]
Path_supergraph_cons_vertex [in GraphBasics.Paths]
Path_supergraph_vertex [in GraphBasics.Paths]
Path_subgraph [in GraphBasics.Paths]
Path_eq [in GraphBasics.Paths]
Path_degree_zero_nil [in GraphBasics.Paths]
Path_last_step [in GraphBasics.Paths]
Path_degree_two [in GraphBasics.Paths]
Path_consx_degree_one [in GraphBasics.Paths]
Path_degree_one [in GraphBasics.Paths]
Path_isa_trail [in GraphBasics.Paths]
P_when_cycle [in GraphBasics.Paths]
P_extract [in GraphBasics.Paths]
P_backstep [in GraphBasics.Paths]
P_inxyel_inyvl [in GraphBasics.Paths]
P_inxyel_inxvl [in GraphBasics.Paths]
P_inel_ina [in GraphBasics.Paths]
P_invl_inv [in GraphBasics.Paths]
P_endy_inv [in GraphBasics.Paths]
P_endx_inv [in GraphBasics.Paths]
P_iny_vl [in GraphBasics.Paths]
S
Single_single_disjoint [in GraphBasics.Sets]Single_disjoint [in GraphBasics.Sets]
Single_equal_single [in GraphBasics.Sets]
Single_equal [in GraphBasics.Sets]
T
Trail_subgraph [in GraphBasics.Paths]Trail_eq [in GraphBasics.Paths]
Trail_isa_walk [in GraphBasics.Paths]
Tree_isa_acyclic [in GraphBasics.Trees]
Tree_isa_connected [in GraphBasics.Trees]
Tree_isa_graph [in GraphBasics.Trees]
U
Union_single_single [in GraphBasics.Sets]Union_inversion2 [in GraphBasics.Sets]
Union_inversion [in GraphBasics.Sets]
Union_differ_inter [in GraphBasics.Sets]
Union_absorb [in GraphBasics.Sets]
Union_dec [in GraphBasics.Sets]
Union_assoc [in GraphBasics.Sets]
Union_commut [in GraphBasics.Sets]
Union_neutral [in GraphBasics.Sets]
Union_eq [in GraphBasics.Sets]
U_enumerable_sum [in GraphBasics.Enumerated]
U_in_dec [in GraphBasics.Enumerated]
U_set_diff [in GraphBasics.Sets]
U_set_diff_commut [in GraphBasics.Sets]
U_set_eq_commut [in GraphBasics.Sets]
U_eq_set [in GraphBasics.Sets]
V
V_union_single_inter [in GraphBasics.Graphs]V_union_single_dec [in GraphBasics.Vertices]
V_eq_dec [in GraphBasics.Vertices]
V_included_union' [in GraphBasics.Connected]
W
Walk_reverse [in GraphBasics.Paths]Walk_append [in GraphBasics.Paths]
Walk_subgraph [in GraphBasics.Paths]
Walk_eq [in GraphBasics.Paths]
Walk_to_path [in GraphBasics.Paths]
Constructor Index
A
AC_eq [in GraphBasics.Acyclic]AC_leaf [in GraphBasics.Acyclic]
AC_vertex [in GraphBasics.Acyclic]
AC_empty [in GraphBasics.Acyclic]
A_ends [in GraphBasics.Arcs]
C
C_eq [in GraphBasics.Connected]C_edge [in GraphBasics.Connected]
C_leaf [in GraphBasics.Connected]
C_isolated [in GraphBasics.Connected]
D
DP_step [in GraphBasics.Dipaths]DP_null [in GraphBasics.Dipaths]
DT_step [in GraphBasics.Dipaths]
DT_null [in GraphBasics.Dipaths]
DW_step [in GraphBasics.Dipaths]
DW_null [in GraphBasics.Dipaths]
D_eq [in GraphBasics.Digraphs]
D_arc [in GraphBasics.Digraphs]
D_vertex [in GraphBasics.Digraphs]
D_empty [in GraphBasics.Digraphs]
E
E_rev [in GraphBasics.Edges]E_refl [in GraphBasics.Edges]
E_ends [in GraphBasics.Edges]
E_left [in GraphBasics.Edges]
E_right [in GraphBasics.Edges]
G
G_eq [in GraphBasics.Graphs]G_edge [in GraphBasics.Graphs]
G_vertex [in GraphBasics.Graphs]
G_empty [in GraphBasics.Graphs]
I
index [in GraphBasics.Vertices]In_differ [in GraphBasics.Sets]
In_inter [in GraphBasics.Sets]
In_right [in GraphBasics.Sets]
In_left [in GraphBasics.Sets]
In_single [in GraphBasics.Sets]
In_full [in GraphBasics.Sets]
P
P_step [in GraphBasics.Paths]P_null [in GraphBasics.Paths]
T
T_eq [in GraphBasics.Trees]T_leaf [in GraphBasics.Trees]
T_root [in GraphBasics.Trees]
T_step [in GraphBasics.Paths]
T_null [in GraphBasics.Paths]
U
U_canon_cons [in GraphBasics.Enumerated]U_canon_nil [in GraphBasics.Enumerated]
W
W_step [in GraphBasics.Paths]W_null [in GraphBasics.Paths]
Axiom Index
U
U_set_eq [in GraphBasics.Sets]Inductive Index
A
Acyclic [in GraphBasics.Acyclic]Arc [in GraphBasics.Arcs]
C
Connected [in GraphBasics.Connected]D
Differ [in GraphBasics.Sets]Digraph [in GraphBasics.Digraphs]
D_path [in GraphBasics.Dipaths]
D_trail [in GraphBasics.Dipaths]
D_walk [in GraphBasics.Dipaths]
E
Edge [in GraphBasics.Edges]Empty [in GraphBasics.Sets]
E_eq [in GraphBasics.Edges]
E_set [in GraphBasics.Edges]
F
Full [in GraphBasics.Sets]G
Graph [in GraphBasics.Graphs]I
Inter [in GraphBasics.Sets]P
Path [in GraphBasics.Paths]S
Single [in GraphBasics.Sets]T
Trail [in GraphBasics.Paths]Tree [in GraphBasics.Trees]
U
Union [in GraphBasics.Sets]U_canon [in GraphBasics.Enumerated]
V
Vertex [in GraphBasics.Vertices]W
Walk [in GraphBasics.Paths]Section Index
A
ACYCLIC [in GraphBasics.Acyclic]ACYCLIC_AND_DEGREES [in GraphBasics.Acyclic]
APPEND_WALKS [in GraphBasics.Paths]
ARC [in GraphBasics.Arcs]
C
CONNECTED [in GraphBasics.Connected]CONNECTED_AND_ACYCLIC [in GraphBasics.Trees]
CONNECTED_BY_EDGES [in GraphBasics.Connected]
D
DEGREE [in GraphBasics.Degrees]DIGRAPH [in GraphBasics.Digraphs]
DIRECTED_PATHES [in GraphBasics.Dipaths]
E
EDGE [in GraphBasics.Edges]ENUMERATION [in GraphBasics.Enumerated]
EXTRACTED [in GraphBasics.Paths]
E_PROPERTIES [in GraphBasics.Edges]
G
GRAPH [in GraphBasics.Graphs]GRAPH_TO_DIGRAPH [in GraphBasics.Graphs]
I
INVERSION_GRAPH [in GraphBasics.Graphs]INVERSION_CONNECTED [in GraphBasics.Connected]
L
LIST_OF_EDGES [in GraphBasics.Edges]N
NEIGHBOR [in GraphBasics.Degrees]P
PATH [in GraphBasics.Paths]PATH_IN_A_SUBGRAPH [in GraphBasics.Paths]
PATH_EQ [in GraphBasics.Paths]
PATH_AND_DEGREE [in GraphBasics.Paths]
R
REMARKABLE_DEGREE [in GraphBasics.Degrees]REVERSE_WALK [in GraphBasics.Paths]
T
TREE [in GraphBasics.Trees]U
UNION_GRAPHS [in GraphBasics.Graphs]UNION_DIGRAPHS [in GraphBasics.Digraphs]
U_SETS.MIXED_PROPERTIES [in GraphBasics.Sets]
U_SETS.DIFFERENCE [in GraphBasics.Sets]
U_SETS.INTERSECTION [in GraphBasics.Sets]
U_SETS.UNION [in GraphBasics.Sets]
U_SETS.INCLUSION [in GraphBasics.Sets]
U_SETS [in GraphBasics.Sets]
V
VERTEX [in GraphBasics.Vertices]Definition Index
A
A_out_neighborhood [in GraphBasics.Arcs]A_in_neighborhood [in GraphBasics.Arcs]
A_single_single_disjoint [in GraphBasics.Arcs]
A_single_disjoint [in GraphBasics.Arcs]
A_union_inversion2 [in GraphBasics.Arcs]
A_union_inversion [in GraphBasics.Arcs]
A_distributivity_union_inter [in GraphBasics.Arcs]
A_distributivity_inter_union [in GraphBasics.Arcs]
A_union_differ_inter [in GraphBasics.Arcs]
A_differ_empty [in GraphBasics.Arcs]
A_differ_E_E [in GraphBasics.Arcs]
A_differ [in GraphBasics.Arcs]
A_inter_absorb [in GraphBasics.Arcs]
A_included_inter [in GraphBasics.Arcs]
A_not_inter [in GraphBasics.Arcs]
A_inter_assoc [in GraphBasics.Arcs]
A_inter_commut [in GraphBasics.Arcs]
A_inter_neutral [in GraphBasics.Arcs]
A_inter_empty [in GraphBasics.Arcs]
A_inter_eq [in GraphBasics.Arcs]
A_in_inter [in GraphBasics.Arcs]
A_inter [in GraphBasics.Arcs]
A_union_absorb [in GraphBasics.Arcs]
A_included_union [in GraphBasics.Arcs]
A_union_dec [in GraphBasics.Arcs]
A_not_union [in GraphBasics.Arcs]
A_union_assoc [in GraphBasics.Arcs]
A_union_commut [in GraphBasics.Arcs]
A_union_neutral [in GraphBasics.Arcs]
A_union_eq [in GraphBasics.Arcs]
A_in_right [in GraphBasics.Arcs]
A_in_left [in GraphBasics.Arcs]
A_union [in GraphBasics.Arcs]
A_enumerable_sum [in GraphBasics.Arcs]
A_enumerable [in GraphBasics.Arcs]
A_included_single [in GraphBasics.Arcs]
A_included [in GraphBasics.Arcs]
A_single_equal_single [in GraphBasics.Arcs]
A_single_equal [in GraphBasics.Arcs]
A_in_single [in GraphBasics.Arcs]
A_single [in GraphBasics.Arcs]
A_empty_nothing [in GraphBasics.Arcs]
A_empty [in GraphBasics.Arcs]
A_set_diff_commut [in GraphBasics.Arcs]
A_set_eq_commut [in GraphBasics.Arcs]
A_eq_set [in GraphBasics.Arcs]
A_set_diff [in GraphBasics.Arcs]
A_set_eq [in GraphBasics.Arcs]
A_set [in GraphBasics.Arcs]
A_sum [in GraphBasics.Arcs]
A_canon [in GraphBasics.Arcs]
A_in_dec [in GraphBasics.Arcs]
A_nil [in GraphBasics.Arcs]
A_list [in GraphBasics.Arcs]
A_loop [in GraphBasics.Arcs]
A_head [in GraphBasics.Arcs]
A_tail [in GraphBasics.Arcs]
C
cdr [in GraphBasics.Paths]Closed_trail [in GraphBasics.Paths]
Closed_walk [in GraphBasics.Paths]
Cycle [in GraphBasics.Paths]
D
DA_list [in GraphBasics.Digraphs]degree [in GraphBasics.Degrees]
DV_list [in GraphBasics.Digraphs]
D_cycle [in GraphBasics.Dipaths]
D_closed_trail [in GraphBasics.Dipaths]
D_closed_walk [in GraphBasics.Dipaths]
D_size [in GraphBasics.Digraphs]
D_order [in GraphBasics.Digraphs]
E
E_in [in GraphBasics.Edges]E_nil [in GraphBasics.Edges]
E_list [in GraphBasics.Edges]
E_reverse [in GraphBasics.Paths]
G
GA_list [in GraphBasics.Graphs]GE_list [in GraphBasics.Graphs]
GV_list [in GraphBasics.Graphs]
G_size [in GraphBasics.Graphs]
G_order [in GraphBasics.Graphs]
I
Included [in GraphBasics.Sets]In_degree [in GraphBasics.Degrees]
In_neighborhood [in GraphBasics.Degrees]
In_neighbor [in GraphBasics.Degrees]
isolated [in GraphBasics.Degrees]
N
Neighbor [in GraphBasics.Degrees]neighborhood [in GraphBasics.Degrees]
O
Out_degree [in GraphBasics.Degrees]Out_neighborhood [in GraphBasics.Degrees]
Out_neighbor [in GraphBasics.Degrees]
P
pendant [in GraphBasics.Degrees]U
U_sum [in GraphBasics.Enumerated]U_enumerable [in GraphBasics.Enumerated]
U_list [in GraphBasics.Enumerated]
U_set [in GraphBasics.Sets]
V
V_extract [in GraphBasics.Paths]V_union_single_single [in GraphBasics.Vertices]
V_single_single_disjoint [in GraphBasics.Vertices]
V_single_disjoint [in GraphBasics.Vertices]
V_union_inversion2 [in GraphBasics.Vertices]
V_union_inversion [in GraphBasics.Vertices]
V_distributivity_union_inter [in GraphBasics.Vertices]
V_distributivity_inter_union [in GraphBasics.Vertices]
V_union_differ_inter [in GraphBasics.Vertices]
V_differ_empty [in GraphBasics.Vertices]
V_differ_E_E [in GraphBasics.Vertices]
V_differ [in GraphBasics.Vertices]
V_inter_absorb [in GraphBasics.Vertices]
V_included_inter [in GraphBasics.Vertices]
V_not_inter [in GraphBasics.Vertices]
V_inter_assoc [in GraphBasics.Vertices]
V_inter_commut [in GraphBasics.Vertices]
V_inter_empty [in GraphBasics.Vertices]
V_inter_neutral [in GraphBasics.Vertices]
V_inter_eq [in GraphBasics.Vertices]
V_in_inter [in GraphBasics.Vertices]
V_inter [in GraphBasics.Vertices]
V_union_absorb [in GraphBasics.Vertices]
V_included_union [in GraphBasics.Vertices]
V_union_dec [in GraphBasics.Vertices]
V_not_union [in GraphBasics.Vertices]
V_union_assoc [in GraphBasics.Vertices]
V_union_commut [in GraphBasics.Vertices]
V_union_neutral [in GraphBasics.Vertices]
V_union_eq [in GraphBasics.Vertices]
V_in_right [in GraphBasics.Vertices]
V_in_left [in GraphBasics.Vertices]
V_union [in GraphBasics.Vertices]
V_enumerable_sum [in GraphBasics.Vertices]
V_enumerable [in GraphBasics.Vertices]
V_included_single [in GraphBasics.Vertices]
V_included [in GraphBasics.Vertices]
V_single_equal_single [in GraphBasics.Vertices]
V_single_equal [in GraphBasics.Vertices]
V_in_single [in GraphBasics.Vertices]
V_single [in GraphBasics.Vertices]
V_empty_nothing [in GraphBasics.Vertices]
V_empty [in GraphBasics.Vertices]
V_set_diff_commut [in GraphBasics.Vertices]
V_set_eq_commut [in GraphBasics.Vertices]
V_eq_set [in GraphBasics.Vertices]
V_set_diff [in GraphBasics.Vertices]
V_set_eq [in GraphBasics.Vertices]
V_set [in GraphBasics.Vertices]
V_sum [in GraphBasics.Vertices]
V_canon [in GraphBasics.Vertices]
V_in_dec [in GraphBasics.Vertices]
V_nil [in GraphBasics.Vertices]
V_list [in GraphBasics.Vertices]
| 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 | (439 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 | (20 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 | (13 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 | (153 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 | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 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 | (36 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 | (147 entries) |